Documentation Verification Report

Basic

📁 Source: Mathlib/CategoryTheory/Bicategory/Adjunction/Basic.lean

Statistics

Metric	Count
Definitions `comp`, `compCounit`, `compUnit`, `counit`, `id`, `instInhabitedId`, `ofIsLeftAdjoint`, `ofIsRightAdjoint`, `unit`, `counit`, `hom`, `id`, `instInhabited`, `inv`, `mkOfAdjointifyCounit`, `unit`, `IsLeftAdjoint`, `IsRightAdjoint`, `LeftAdjoint`, `adj`, `left`, `RightAdjoint`, `adj`, `right`, `adjointifyCounit`, `getLeftAdjoint`, `getRightAdjoint`, `leftAdjoint`, `leftZigzag`, `leftZigzagIso`, `rightAdjoint`, `rightZigzag`, `rightZigzagIso`, `«term_≌_»`, `«term_⊣_»`	35
Theorems `comp_counit`, `comp_left_triangle_aux`, `comp_right_triangle_aux`, `comp_unit`, `ext`, `ext_iff`, `left_triangle`, `right_triangle`, `left_triangle`, `left_triangle_hom`, `right_triangle`, `right_triangle_hom`, `mk`, `nonempty`, `mk`, `nonempty`, `adjointifyCounit_left_triangle`, `instIsIsoHomLeftZigzagHom`, `instIsIsoHomRightZigzagHom`, `leftZigzagIso_hom`, `leftZigzagIso_inv`, `leftZigzagIso_symm`, `rightZigzagIso_hom`, `rightZigzagIso_inv`, `rightZigzagIso_symm`, `rightZigzag_idempotent_of_left_triangle`, `right_triangle_of_left_triangle`	27
Total	62

CategoryTheory.Bicategory

Definitions

Name	Category	Theorems
`IsLeftAdjoint` 📖	CompData	2 math math: `isLeftAdjoint_TFAE`, `IsLeftAdjoint.mk`
`IsRightAdjoint` 📖	CompData	2 math math: `IsRightAdjoint.mk`, `isRightAdjoint_TFAE`
`LeftAdjoint` 📖	CompData	1 math math: `IsRightAdjoint.nonempty`
`RightAdjoint` 📖	CompData	1 math math: `IsLeftAdjoint.nonempty`
`adjointifyCounit` 📖	CompOp	1 math math: `adjointifyCounit_left_triangle`
`getLeftAdjoint` 📖	CompOp	—
`getRightAdjoint` 📖	CompOp	—
`leftAdjoint` 📖	CompOp	—
`leftZigzag` 📖	CompOp	6 math math: `leftZigzagIso_hom`, `instIsIsoHomLeftZigzagHom`, `Adjunction.left_triangle`, `rightZigzagIso_inv`, `Adjunction.comp_left_triangle_aux`, `Equivalence.left_triangle_hom`
`leftZigzagIso` 📖	CompOp	6 math math: `leftZigzagIso_symm`, `leftZigzagIso_hom`, `Equivalence.left_triangle`, `adjointifyCounit_left_triangle`, `rightZigzagIso_symm`, `leftZigzagIso_inv`
`rightAdjoint` 📖	CompOp	—
`rightZigzag` 📖	CompOp	8 math math: `right_triangle_of_left_triangle`, `rightZigzag_idempotent_of_left_triangle`, `instIsIsoHomRightZigzagHom`, `leftZigzagIso_inv`, `Adjunction.comp_right_triangle_aux`, `Adjunction.right_triangle`, `Equivalence.right_triangle_hom`, `rightZigzagIso_hom`
`rightZigzagIso` 📖	CompOp	5 math math: `leftZigzagIso_symm`, `Equivalence.right_triangle`, `rightZigzagIso_symm`, `rightZigzagIso_inv`, `rightZigzagIso_hom`
`«term_≌_»` 📖	CompOp	—
`«term_⊣_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjointifyCounit_left_triangle` 📖	mathematical	—	`leftZigzagIso` `adjointifyCounit` `CategoryTheory.Iso.trans` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `toCategoryStruct` `homCategory` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CategoryStruct.id` `leftUnitor` `CategoryTheory.Iso.symm` `rightUnitor`	—	`CategoryTheory.Iso.ext` `Mathlib.Tactic.BicategoryLike.mk_eq` `Mathlib.Tactic.Bicategory.eval_bicategoricalComp` `Mathlib.Tactic.Bicategory.eval_whiskerRight` `Mathlib.Tactic.Bicategory.eval_of` `Mathlib.Tactic.Bicategory.evalWhiskerRight_cons_of_of` `Mathlib.Tactic.Bicategory.evalWhiskerRight_nil` `Mathlib.Tactic.Bicategory.evalWhiskerRightAux_of` `Mathlib.Tactic.Bicategory.evalComp_cons` `Mathlib.Tactic.Bicategory.evalComp_nil_nil` `Mathlib.Tactic.Bicategory.evalComp_nil_cons` `Mathlib.Tactic.Bicategory.eval_whiskerLeft` `Mathlib.Tactic.Bicategory.eval_comp` `Mathlib.Tactic.Bicategory.evalWhiskerLeft_of_cons` `Mathlib.Tactic.Bicategory.evalWhiskerLeft_nil` `Mathlib.Tactic.Bicategory.evalWhiskerRight_comp` `Mathlib.Tactic.Bicategory.evalWhiskerRight_id` `Mathlib.Tactic.Bicategory.evalWhiskerLeft_comp` `Mathlib.Tactic.BicategoryLike.mk_eq_of_cons` `Mathlib.Tactic.Bicategory.mk_eq_of_naturality` `Mathlib.Tactic.Bicategory.naturality_comp` `Mathlib.Tactic.Bicategory.naturality_whiskerRight` `Mathlib.Tactic.Bicategory.naturality_id` `Mathlib.Tactic.Bicategory.naturality_leftUnitor` `Mathlib.Tactic.Bicategory.naturality_inv` `Mathlib.Tactic.Bicategory.naturality_rightUnitor` `Mathlib.Tactic.Bicategory.naturality_associator` `Mathlib.Tactic.Bicategory.naturality_whiskerLeft` `whisker_exchange` `Mathlib.Tactic.Bicategory.evalWhiskerLeft_id` `Mathlib.Tactic.Bicategory.evalWhiskerRight_cons_whisker` `CategoryTheory.Iso.inv_hom_id`
`instIsIsoHomLeftZigzagHom` 📖	mathematical	—	`CategoryTheory.IsIso` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `toCategoryStruct` `homCategory` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CategoryStruct.id` `leftZigzag` `CategoryTheory.Iso.hom`	—	`CategoryTheory.Iso.isIso_hom`
`instIsIsoHomRightZigzagHom` 📖	mathematical	—	`CategoryTheory.IsIso` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `toCategoryStruct` `homCategory` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CategoryStruct.id` `rightZigzag` `CategoryTheory.Iso.hom`	—	`CategoryTheory.Iso.isIso_hom`
`leftZigzagIso_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `toCategoryStruct` `homCategory` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CategoryStruct.id` `leftZigzagIso` `leftZigzag`	—	—
`leftZigzagIso_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `toCategoryStruct` `homCategory` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CategoryStruct.id` `leftZigzagIso` `rightZigzag`	—	`CategoryTheory.Iso.trans_assoc` `whiskerRight_comp` `id_whiskerRight` `CategoryTheory.Category.id_comp` `CategoryTheory.Iso.inv_hom_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.assoc`
`leftZigzagIso_symm` 📖	mathematical	—	`CategoryTheory.Iso.symm` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `toCategoryStruct` `homCategory` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CategoryStruct.id` `leftZigzagIso` `rightZigzagIso`	—	`CategoryTheory.Iso.ext` `leftZigzagIso_inv`
`rightZigzagIso_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `toCategoryStruct` `homCategory` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CategoryStruct.id` `rightZigzagIso` `rightZigzag`	—	—
`rightZigzagIso_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `toCategoryStruct` `homCategory` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CategoryStruct.id` `rightZigzagIso` `leftZigzag`	—	`CategoryTheory.Iso.trans_assoc` `whiskerRight_comp` `id_whiskerRight` `CategoryTheory.Category.id_comp` `CategoryTheory.Iso.inv_hom_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.assoc`
`rightZigzagIso_symm` 📖	mathematical	—	`CategoryTheory.Iso.symm` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `toCategoryStruct` `homCategory` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CategoryStruct.id` `rightZigzagIso` `leftZigzagIso`	—	`CategoryTheory.Iso.ext` `rightZigzagIso_inv`
`rightZigzag_idempotent_of_left_triangle` 📖	mathematical	`leftZigzag` `CategoryTheory.CategoryStruct.comp` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `toCategoryStruct` `CategoryTheory.Category.toCategoryStruct` `homCategory` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Iso.hom` `leftUnitor` `CategoryTheory.Iso.inv` `rightUnitor`	`CategoryTheory.bicategoricalComp` `CategoryTheory.BicategoricalCoherence.left` `CategoryTheory.BicategoricalCoherence.right'` `CategoryTheory.BicategoricalCoherence.refl` `rightZigzag`	—	`Mathlib.Tactic.BicategoryLike.mk_eq` `Mathlib.Tactic.Bicategory.eval_bicategoricalComp` `Mathlib.Tactic.Bicategory.eval_whiskerLeft` `Mathlib.Tactic.Bicategory.eval_of` `Mathlib.Tactic.Bicategory.evalWhiskerLeft_of_cons` `Mathlib.Tactic.Bicategory.evalWhiskerLeft_nil` `Mathlib.Tactic.Bicategory.eval_whiskerRight` `Mathlib.Tactic.Bicategory.evalWhiskerRight_cons_of_of` `Mathlib.Tactic.Bicategory.evalWhiskerRight_nil` `Mathlib.Tactic.Bicategory.evalWhiskerRightAux_of` `Mathlib.Tactic.Bicategory.evalComp_cons` `Mathlib.Tactic.Bicategory.evalComp_nil_nil` `Mathlib.Tactic.Bicategory.evalComp_nil_cons` `Mathlib.Tactic.Bicategory.eval_comp` `Mathlib.Tactic.Bicategory.evalWhiskerRight_id` `Mathlib.Tactic.Bicategory.evalWhiskerLeft_comp` `Mathlib.Tactic.Bicategory.evalWhiskerLeft_id` `Mathlib.Tactic.BicategoryLike.mk_eq_of_cons` `Mathlib.Tactic.Bicategory.mk_eq_of_naturality` `Mathlib.Tactic.Bicategory.naturality_whiskerLeft` `Mathlib.Tactic.Bicategory.naturality_id` `Mathlib.Tactic.Bicategory.naturality_comp` `Mathlib.Tactic.Bicategory.naturality_whiskerRight` `Mathlib.Tactic.Bicategory.naturality_inv` `Mathlib.Tactic.Bicategory.naturality_associator` `Mathlib.Tactic.Bicategory.naturality_rightUnitor` `Mathlib.Tactic.Bicategory.naturality_leftUnitor` `whisker_exchange` `Mathlib.Tactic.Bicategory.evalWhiskerRight_comp` `leftZigzag.eq_1` `Mathlib.Tactic.Bicategory.evalWhiskerRight_cons_whisker`
`right_triangle_of_left_triangle` 📖	mathematical	`leftZigzag` `CategoryTheory.Iso.hom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `toCategoryStruct` `homCategory` `CategoryTheory.CategoryStruct.id` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `leftUnitor` `CategoryTheory.Iso.inv` `rightUnitor`	`rightZigzag`	—	`CategoryTheory.cancel_epi` `CategoryTheory.epi_comp` `CategoryTheory.IsIso.epi_of_iso` `instIsIsoHomRightZigzagHom` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.Iso.isIso_inv` `Mathlib.Tactic.BicategoryLike.mk_eq` `Mathlib.Tactic.Bicategory.eval_comp` `Mathlib.Tactic.Bicategory.eval_bicategoricalComp` `Mathlib.Tactic.Bicategory.eval_whiskerLeft` `Mathlib.Tactic.Bicategory.eval_of` `Mathlib.Tactic.Bicategory.evalWhiskerLeft_of_cons` `Mathlib.Tactic.Bicategory.evalWhiskerLeft_nil` `Mathlib.Tactic.Bicategory.eval_whiskerRight` `Mathlib.Tactic.Bicategory.evalWhiskerRight_cons_of_of` `Mathlib.Tactic.Bicategory.evalWhiskerRight_nil` `Mathlib.Tactic.Bicategory.evalWhiskerRightAux_of` `Mathlib.Tactic.Bicategory.evalComp_cons` `Mathlib.Tactic.Bicategory.evalComp_nil_nil` `Mathlib.Tactic.Bicategory.evalComp_nil_cons` `Mathlib.Tactic.BicategoryLike.mk_eq_of_cons` `Mathlib.Tactic.Bicategory.mk_eq_of_naturality` `Mathlib.Tactic.Bicategory.naturality_whiskerLeft` `Mathlib.Tactic.Bicategory.naturality_id` `Mathlib.Tactic.Bicategory.naturality_comp` `Mathlib.Tactic.Bicategory.naturality_whiskerRight` `Mathlib.Tactic.Bicategory.naturality_inv` `Mathlib.Tactic.Bicategory.naturality_associator` `Mathlib.Tactic.Bicategory.naturality_leftUnitor` `Mathlib.Tactic.Bicategory.naturality_rightUnitor` `rightZigzag_idempotent_of_left_triangle` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.inv_hom_id_assoc` `CategoryTheory.Iso.hom_inv_id` `CategoryTheory.Category.comp_id`

CategoryTheory.Bicategory.Adjunction

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	16 math math: `CategoryTheory.Bicategory.iterated_mateEquiv_conjugateEquiv`, `CategoryTheory.Bicategory.conjugateEquiv_whiskerRight`, `CategoryTheory.Bicategory.mateEquiv_comp_id_right`, `CategoryTheory.Adjunction.toCat_comp_toCat`, `CategoryTheory.Bicategory.mateEquiv_id_comp_right`, `comp_counit`, `CategoryTheory.Bicategory.conjugateEquiv_id_comp_right_apply`, `CategoryTheory.Bicategory.conjugateEquiv_comp_id_right_apply`, `ofCat_comp`, `CategoryTheory.Bicategory.mateEquiv_hcomp`, `CategoryTheory.Bicategory.iterated_mateEquiv_conjugateEquiv_symm`, `CategoryTheory.Bicategory.mateEquiv_square`, `CategoryTheory.Bicategory.conjugateEquiv_associator_hom`, `CategoryTheory.Bicategory.Adj.comp_adj`, `comp_unit`, `CategoryTheory.Bicategory.conjugateEquiv_whiskerLeft`
`compCounit` 📖	CompOp	3 math math: `comp_counit`, `comp_left_triangle_aux`, `comp_right_triangle_aux`
`compUnit` 📖	CompOp	3 math math: `comp_left_triangle_aux`, `comp_right_triangle_aux`, `comp_unit`
`counit` 📖	CompOp	13 math math: `homEquiv₂_symm_apply`, `CategoryTheory.Adjunction.ofCat_counit`, `homEquiv₁_apply`, `comp_counit`, `CategoryTheory.Bicategory.mateEquiv_symm_apply'`, `CategoryTheory.Adjunction.toCat_counit_toNatTrans`, `left_triangle`, `CategoryTheory.Bicategory.conjugateEquiv_apply'`, `CategoryTheory.Bicategory.conjugateEquiv_adjunction_id`, `CategoryTheory.Bicategory.conjugateEquiv_symm_apply'`, `ext_iff`, `right_triangle`, `CategoryTheory.Bicategory.mateEquiv_apply'`
`id` 📖	CompOp	8 math math: `CategoryTheory.Bicategory.mateEquiv_comp_id_right`, `CategoryTheory.Bicategory.conjugateEquiv_adjunction_id_symm`, `CategoryTheory.Bicategory.mateEquiv_id_comp_right`, `CategoryTheory.Bicategory.conjugateEquiv_id_comp_right_apply`, `CategoryTheory.Bicategory.conjugateEquiv_comp_id_right_apply`, `ofCat_id`, `CategoryTheory.Bicategory.Adj.id_adj`, `CategoryTheory.Bicategory.conjugateEquiv_adjunction_id`
`instInhabitedId` 📖	CompOp	—
`ofIsLeftAdjoint` 📖	CompOp	—
`ofIsRightAdjoint` 📖	CompOp	—
`unit` 📖	CompOp	13 math math: `CategoryTheory.Bicategory.conjugateEquiv_adjunction_id_symm`, `CategoryTheory.Bicategory.mateEquiv_symm_apply'`, `homEquiv₂_apply`, `left_triangle`, `CategoryTheory.Bicategory.conjugateEquiv_apply'`, `CategoryTheory.Adjunction.toCat_unit_toNatTrans`, `CategoryTheory.Adjunction.ofCat_unit`, `homEquiv₁_symm_apply`, `comp_unit`, `CategoryTheory.Bicategory.conjugateEquiv_symm_apply'`, `ext_iff`, `right_triangle`, `CategoryTheory.Bicategory.mateEquiv_apply'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_counit` 📖	mathematical	—	`counit` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bicategory.toCategoryStruct` `comp` `compCounit`	—	—
`comp_left_triangle_aux` 📖	mathematical	—	`CategoryTheory.Bicategory.leftZigzag` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bicategory.toCategoryStruct` `compUnit` `compCounit` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Iso.hom` `CategoryTheory.Bicategory.leftUnitor` `CategoryTheory.Iso.inv` `CategoryTheory.Bicategory.rightUnitor`	—	`Mathlib.Tactic.BicategoryLike.mk_eq` `Mathlib.Tactic.Bicategory.eval_bicategoricalComp` `Mathlib.Tactic.Bicategory.eval_whiskerRight` `Mathlib.Tactic.Bicategory.eval_of` `Mathlib.Tactic.Bicategory.eval_whiskerLeft` `Mathlib.Tactic.Bicategory.evalWhiskerRight_cons_of_of` `Mathlib.Tactic.Bicategory.evalWhiskerRight_nil` `Mathlib.Tactic.Bicategory.evalWhiskerRightAux_of` `Mathlib.Tactic.Bicategory.evalComp_cons` `Mathlib.Tactic.Bicategory.evalComp_nil_nil` `Mathlib.Tactic.Bicategory.evalComp_nil_cons` `Mathlib.Tactic.Bicategory.evalWhiskerLeft_of_cons` `Mathlib.Tactic.Bicategory.evalWhiskerLeft_nil` `Mathlib.Tactic.Bicategory.evalWhiskerRight_comp` `Mathlib.Tactic.Bicategory.evalWhiskerRight_cons_whisker` `Mathlib.Tactic.Bicategory.evalWhiskerLeft_comp` `Mathlib.Tactic.Bicategory.eval_comp` `Mathlib.Tactic.BicategoryLike.mk_eq_of_cons` `Mathlib.Tactic.Bicategory.mk_eq_of_naturality` `Mathlib.Tactic.Bicategory.naturality_comp` `Mathlib.Tactic.Bicategory.naturality_inv` `Mathlib.Tactic.Bicategory.naturality_associator` `Mathlib.Tactic.Bicategory.naturality_whiskerRight` `Mathlib.Tactic.Bicategory.naturality_id` `Mathlib.Tactic.Bicategory.naturality_leftUnitor` `Mathlib.Tactic.Bicategory.naturality_whiskerLeft` `CategoryTheory.Bicategory.whisker_exchange` `Mathlib.Tactic.Bicategory.evalWhiskerLeft_id` `Mathlib.Tactic.Bicategory.evalWhiskerRight_id` `Mathlib.Tactic.Bicategory.naturality_rightUnitor` `left_triangle`
`comp_right_triangle_aux` 📖	mathematical	—	`CategoryTheory.Bicategory.rightZigzag` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bicategory.toCategoryStruct` `compUnit` `compCounit` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Iso.hom` `CategoryTheory.Bicategory.rightUnitor` `CategoryTheory.Iso.inv` `CategoryTheory.Bicategory.leftUnitor`	—	`Mathlib.Tactic.BicategoryLike.mk_eq` `Mathlib.Tactic.Bicategory.eval_bicategoricalComp` `Mathlib.Tactic.Bicategory.eval_whiskerLeft` `Mathlib.Tactic.Bicategory.eval_of` `Mathlib.Tactic.Bicategory.eval_whiskerRight` `Mathlib.Tactic.Bicategory.evalWhiskerRight_cons_of_of` `Mathlib.Tactic.Bicategory.evalWhiskerRight_nil` `Mathlib.Tactic.Bicategory.evalWhiskerRightAux_of` `Mathlib.Tactic.Bicategory.evalComp_cons` `Mathlib.Tactic.Bicategory.evalComp_nil_nil` `Mathlib.Tactic.Bicategory.evalComp_nil_cons` `Mathlib.Tactic.Bicategory.evalWhiskerLeft_of_cons` `Mathlib.Tactic.Bicategory.evalWhiskerLeft_nil` `Mathlib.Tactic.Bicategory.evalWhiskerLeft_comp` `Mathlib.Tactic.Bicategory.evalWhiskerRight_cons_whisker` `Mathlib.Tactic.Bicategory.evalWhiskerRight_comp` `Mathlib.Tactic.Bicategory.eval_comp` `Mathlib.Tactic.BicategoryLike.mk_eq_of_cons` `Mathlib.Tactic.Bicategory.mk_eq_of_naturality` `Mathlib.Tactic.Bicategory.naturality_comp` `Mathlib.Tactic.Bicategory.naturality_associator` `Mathlib.Tactic.Bicategory.naturality_whiskerLeft` `Mathlib.Tactic.Bicategory.naturality_id` `Mathlib.Tactic.Bicategory.naturality_whiskerRight` `Mathlib.Tactic.Bicategory.naturality_inv` `Mathlib.Tactic.Bicategory.naturality_leftUnitor` `CategoryTheory.Bicategory.whisker_exchange` `Mathlib.Tactic.Bicategory.evalWhiskerRight_id` `Mathlib.Tactic.Bicategory.evalWhiskerLeft_id` `Mathlib.Tactic.Bicategory.naturality_rightUnitor` `right_triangle`
`comp_unit` 📖	mathematical	—	`unit` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bicategory.toCategoryStruct` `comp` `compUnit`	—	—
`ext` 📖	—	`unit` `counit`	—	—	—
`ext_iff` 📖	mathematical	—	`unit` `counit`	—	`ext`
`left_triangle` 📖	mathematical	—	`CategoryTheory.Bicategory.leftZigzag` `unit` `counit` `CategoryTheory.CategoryStruct.comp` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Iso.hom` `CategoryTheory.Bicategory.leftUnitor` `CategoryTheory.Iso.inv` `CategoryTheory.Bicategory.rightUnitor`	—	—
`right_triangle` 📖	mathematical	—	`CategoryTheory.Bicategory.rightZigzag` `unit` `counit` `CategoryTheory.CategoryStruct.comp` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Iso.hom` `CategoryTheory.Bicategory.rightUnitor` `CategoryTheory.Iso.inv` `CategoryTheory.Bicategory.leftUnitor`	—	—

CategoryTheory.Bicategory.Equivalence

Definitions

Name	Category	Theorems
`counit` 📖	CompOp	4 math math: `right_triangle`, `left_triangle`, `right_triangle_hom`, `left_triangle_hom`
`hom` 📖	CompOp	4 math math: `right_triangle`, `left_triangle`, `right_triangle_hom`, `left_triangle_hom`
`id` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`inv` 📖	CompOp	4 math math: `right_triangle`, `left_triangle`, `right_triangle_hom`, `left_triangle_hom`
`mkOfAdjointifyCounit` 📖	CompOp	—
`unit` 📖	CompOp	4 math math: `right_triangle`, `left_triangle`, `right_triangle_hom`, `left_triangle_hom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`left_triangle` 📖	mathematical	—	`CategoryTheory.Bicategory.leftZigzagIso` `hom` `inv` `unit` `counit` `CategoryTheory.Iso.trans` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Bicategory.leftUnitor` `CategoryTheory.Iso.symm` `CategoryTheory.Bicategory.rightUnitor`	—	—
`left_triangle_hom` 📖	mathematical	—	`CategoryTheory.Bicategory.leftZigzag` `hom` `inv` `CategoryTheory.Iso.hom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.CategoryStruct.id` `CategoryTheory.CategoryStruct.comp` `unit` `counit` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.leftUnitor` `CategoryTheory.Iso.inv` `CategoryTheory.Bicategory.rightUnitor`	—	`left_triangle`
`right_triangle` 📖	mathematical	—	`CategoryTheory.Bicategory.rightZigzagIso` `hom` `inv` `unit` `counit` `CategoryTheory.Iso.trans` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Bicategory.rightUnitor` `CategoryTheory.Iso.symm` `CategoryTheory.Bicategory.leftUnitor`	—	`CategoryTheory.Iso.ext` `CategoryTheory.Bicategory.right_triangle_of_left_triangle` `left_triangle_hom`
`right_triangle_hom` 📖	mathematical	—	`CategoryTheory.Bicategory.rightZigzag` `hom` `inv` `CategoryTheory.Iso.hom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.CategoryStruct.id` `CategoryTheory.CategoryStruct.comp` `unit` `counit` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.rightUnitor` `CategoryTheory.Iso.inv` `CategoryTheory.Bicategory.leftUnitor`	—	`right_triangle`

CategoryTheory.Bicategory.IsLeftAdjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mk` 📖	mathematical	—	`CategoryTheory.Bicategory.IsLeftAdjoint`	—	—
`nonempty` 📖	mathematical	—	`CategoryTheory.Bicategory.RightAdjoint`	—	—

CategoryTheory.Bicategory.IsRightAdjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mk` 📖	mathematical	—	`CategoryTheory.Bicategory.IsRightAdjoint`	—	—
`nonempty` 📖	mathematical	—	`CategoryTheory.Bicategory.LeftAdjoint`	—	—

CategoryTheory.Bicategory.LeftAdjoint

Definitions

Name	Category	Theorems
`adj` 📖	CompOp	—
`left` 📖	CompOp	—

CategoryTheory.Bicategory.RightAdjoint

Definitions

Name	Category	Theorems
`adj` 📖	CompOp	—
`right` 📖	CompOp	—

---

← Back to Index