Documentation Verification Report

Extension

📁 Source: Mathlib/CategoryTheory/Bicategory/Extension.lean

Statistics

Metric	Count
Definitions `LeftExtension`, `alongId`, `extension`, `homMk`, `instInhabitedId`, `mk`, `ofCompId`, `unit`, `whisker`, `whiskerHom`, `whiskerIdCancel`, `whiskerIso`, `whiskerOfCompIdIsoSelf`, `whiskering`, `LeftLift`, `alongId`, `homMk`, `instInhabitedId`, `mk`, `ofIdComp`, `unit`, `whisker`, `whiskerHom`, `whiskerIdCancel`, `whiskerIso`, `whiskerOfIdCompIsoSelf`, `whiskering`, `RightExtension`, `alongId`, `counit`, `extension`, `homMk`, `instInhabitedId`, `mk`, `RightLift`, `alongId`, `counit`, `homMk`, `instInhabitedId`, `mk`, `Extension`	41
Theorems `ofCompId_hom`, `ofCompId_left_as`, `ofCompId_right`, `w`, `w_assoc`, `whiskerHom_right`, `whiskerIdCancel_right`, `whiskerOfCompIdIsoSelf_hom_right`, `whiskerOfCompIdIsoSelf_inv_right`, `whisker_extension`, `whisker_unit`, `whiskering_map`, `whiskering_obj`, `ofIdComp_hom`, `ofIdComp_left_as`, `ofIdComp_right`, `w`, `w_assoc`, `whiskerHom_right`, `whiskerIdCancel_right`, `whiskerOfIdCompIsoSelf_hom_right`, `whiskerOfIdCompIsoSelf_inv_right`, `whisker_lift`, `whisker_unit`, `whiskering_map`, `whiskering_obj`, `w`, `w_assoc`, `w`, `w_assoc`	30
Total	71

CategoryTheory.Bicategory

Definitions

Name	Category	Theorems
`LeftExtension` 📖	CompOp	10 math math: `LeftExtension.whiskering_map`, `Lan.CommuteWith.lanCompIsoWhisker_hom_right`, `LeftExtension.IsKan.uniqueUpToIso_hom_right`, `Lan.CommuteWith.lanCompIsoWhisker_inv_right`, `instHasInitialLeftExtensionOfHasLeftKanExtension`, `LeftExtension.IsKan.uniqueUpToIso_inv_right`, `HasLeftKanExtension.hasInitial`, `LeftExtension.whiskerOfCompIdIsoSelf_hom_right`, `LeftExtension.whiskerOfCompIdIsoSelf_inv_right`, `LeftExtension.whiskering_obj`
`LeftLift` 📖	CompOp	10 math math: `LeftLift.whiskering_map`, `HasLeftKanLift.hasInitial`, `LeftLift.whiskerOfIdCompIsoSelf_hom_right`, `LeftLift.IsKan.uniqueUpToIso_hom_right`, `instHasInitialLeftLiftOfHasLeftKanLift`, `LanLift.CommuteWith.lanLiftCompIsoWhisker_inv_right`, `LeftLift.IsKan.uniqueUpToIso_inv_right`, `LeftLift.whiskering_obj`, `LeftLift.whiskerOfIdCompIsoSelf_inv_right`, `LanLift.CommuteWith.lanLiftCompIsoWhisker_hom_right`
`RightExtension` 📖	CompOp	—
`RightLift` 📖	CompOp	—

CategoryTheory.Bicategory.LeftExtension

Definitions

Name	Category	Theorems
`alongId` 📖	CompOp	—
`extension` 📖	CompOp	15 math math: `w_assoc`, `CategoryTheory.Bicategory.Lan.existsUnique`, `ofCompId_right`, `whiskerIdCancel_right`, `IsKan.fac_assoc`, `ofCompId_hom`, `CategoryTheory.Bicategory.lanUnit_desc`, `whisker_unit`, `whiskerOfCompIdIsoSelf_hom_right`, `CategoryTheory.Bicategory.lanLeftExtension_extension`, `whisker_extension`, `CategoryTheory.Bicategory.lanUnit_desc_assoc`, `whiskerOfCompIdIsoSelf_inv_right`, `IsKan.fac`, `w`
`homMk` 📖	CompOp	1 math math: `whiskering_map`
`instInhabitedId` 📖	CompOp	—
`mk` 📖	CompOp	—
`ofCompId` 📖	CompOp	6 math math: `ofCompId_right`, `ofCompId_left_as`, `whiskerIdCancel_right`, `ofCompId_hom`, `whiskerOfCompIdIsoSelf_hom_right`, `whiskerOfCompIdIsoSelf_inv_right`
`unit` 📖	CompOp	10 math math: `w_assoc`, `CategoryTheory.Bicategory.Lan.existsUnique`, `IsKan.fac_assoc`, `ofCompId_hom`, `CategoryTheory.Bicategory.lanUnit_desc`, `whisker_unit`, `CategoryTheory.Bicategory.lanUnit_desc_assoc`, `IsKan.fac`, `CategoryTheory.Bicategory.lanLeftExtension_unit`, `w`
`whisker` 📖	CompOp	13 math math: `whiskering_map`, `CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIso_inv`, `CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIsoWhisker_hom_right`, `whiskerIdCancel_right`, `CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIsoWhisker_inv_right`, `CategoryTheory.Bicategory.Lan.CommuteWith.commute`, `CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIso_hom`, `whisker_unit`, `whiskerOfCompIdIsoSelf_hom_right`, `whisker_extension`, `whiskerHom_right`, `whiskerOfCompIdIsoSelf_inv_right`, `whiskering_obj`
`whiskerHom` 📖	CompOp	1 math math: `whiskerHom_right`
`whiskerIdCancel` 📖	CompOp	1 math math: `whiskerIdCancel_right`
`whiskerIso` 📖	CompOp	—
`whiskerOfCompIdIsoSelf` 📖	CompOp	2 math math: `whiskerOfCompIdIsoSelf_hom_right`, `whiskerOfCompIdIsoSelf_inv_right`
`whiskering` 📖	CompOp	2 math math: `whiskering_map`, `whiskering_obj`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofCompId_hom` 📖	mathematical	—	`CategoryTheory.Comma.hom` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Bicategory.precomp` `ofCompId` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.CategoryStruct.id` `extension` `CategoryTheory.Iso.inv` `CategoryTheory.Bicategory.rightUnitor` `unit`	—	—
`ofCompId_left_as` 📖	mathematical	—	`CategoryTheory.Discrete.as` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Bicategory.precomp` `ofCompId`	—	—
`ofCompId_right` 📖	mathematical	—	`CategoryTheory.Comma.right` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Bicategory.precomp` `ofCompId` `extension` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CategoryStruct.id`	—	—
`w` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `extension` `CategoryTheory.Comma.right` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Bicategory.precomp` `unit` `CategoryTheory.Bicategory.whiskerLeft` `CategoryTheory.CommaMorphism.right`	—	`CategoryTheory.StructuredArrow.w`
`w_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `extension` `unit` `CategoryTheory.Comma.right` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Bicategory.precomp` `CategoryTheory.Bicategory.whiskerLeft` `CategoryTheory.CommaMorphism.right`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `w`
`whiskerHom_right` 📖	mathematical	—	`CategoryTheory.CommaMorphism.right` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bicategory.precomp` `whisker` `whiskerHom` `CategoryTheory.Bicategory.whiskerRight` `CategoryTheory.Comma.right`	—	—
`whiskerIdCancel_right` 📖	mathematical	—	`CategoryTheory.CommaMorphism.right` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Bicategory.precomp` `ofCompId` `whiskerIdCancel` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `extension` `CategoryTheory.CategoryStruct.id` `whisker` `CategoryTheory.Iso.hom` `CategoryTheory.Bicategory.rightUnitor`	—	—
`whiskerOfCompIdIsoSelf_hom_right` 📖	mathematical	—	`CategoryTheory.CommaMorphism.right` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Bicategory.precomp` `ofCompId` `whisker` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Iso.hom` `CategoryTheory.Bicategory.LeftExtension` `CategoryTheory.instCategoryStructuredArrow` `whiskerOfCompIdIsoSelf` `CategoryTheory.CategoryStruct.comp` `extension` `CategoryTheory.Comma.right` `CategoryTheory.Bicategory.rightUnitor`	—	—
`whiskerOfCompIdIsoSelf_inv_right` 📖	mathematical	—	`CategoryTheory.CommaMorphism.right` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Bicategory.precomp` `ofCompId` `whisker` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Iso.inv` `CategoryTheory.Bicategory.LeftExtension` `CategoryTheory.instCategoryStructuredArrow` `whiskerOfCompIdIsoSelf` `CategoryTheory.CategoryStruct.comp` `extension` `CategoryTheory.Comma.right` `CategoryTheory.Bicategory.rightUnitor`	—	—
`whisker_extension` 📖	mathematical	—	`extension` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bicategory.toCategoryStruct` `whisker`	—	—
`whisker_unit` 📖	mathematical	—	`unit` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bicategory.toCategoryStruct` `whisker` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `extension` `CategoryTheory.Bicategory.whiskerRight` `CategoryTheory.Iso.hom` `CategoryTheory.Bicategory.associator`	—	—
`whiskering_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.Bicategory.LeftExtension` `CategoryTheory.instCategoryStructuredArrow` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Bicategory.precomp` `CategoryTheory.CategoryStruct.comp` `whiskering` `homMk` `whisker` `CategoryTheory.Bicategory.whiskerRight` `CategoryTheory.Comma.right` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.CommaMorphism.right`	—	—
`whiskering_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.Bicategory.LeftExtension` `CategoryTheory.instCategoryStructuredArrow` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Bicategory.precomp` `CategoryTheory.CategoryStruct.comp` `whiskering` `whisker`	—	—

CategoryTheory.Bicategory.LeftLift

Definitions

Name	Category	Theorems
`alongId` 📖	CompOp	—
`homMk` 📖	CompOp	1 math math: `whiskering_map`
`instInhabitedId` 📖	CompOp	—
`mk` 📖	CompOp	—
`ofIdComp` 📖	CompOp	6 math math: `ofIdComp_right`, `ofIdComp_hom`, `whiskerOfIdCompIsoSelf_hom_right`, `whiskerIdCancel_right`, `ofIdComp_left_as`, `whiskerOfIdCompIsoSelf_inv_right`
`unit` 📖	CompOp	10 math math: `w_assoc`, `CategoryTheory.Bicategory.lanLiftUnit_desc_assoc`, `IsKan.fac_assoc`, `CategoryTheory.Bicategory.LanLift.existsUnique`, `CategoryTheory.Bicategory.lanLiftLeftLift_unit`, `whisker_unit`, `IsKan.fac`, `ofIdComp_hom`, `CategoryTheory.Bicategory.lanLiftUnit_desc`, `w`
`whisker` 📖	CompOp	13 math math: `whiskering_map`, `CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIso_hom`, `whisker_unit`, `whiskerHom_right`, `whisker_lift`, `whiskerOfIdCompIsoSelf_hom_right`, `whiskerIdCancel_right`, `CategoryTheory.Bicategory.LanLift.CommuteWith.commute`, `CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIsoWhisker_inv_right`, `whiskering_obj`, `whiskerOfIdCompIsoSelf_inv_right`, `CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIso_inv`, `CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIsoWhisker_hom_right`
`whiskerHom` 📖	CompOp	1 math math: `whiskerHom_right`
`whiskerIdCancel` 📖	CompOp	1 math math: `whiskerIdCancel_right`
`whiskerIso` 📖	CompOp	—
`whiskerOfIdCompIsoSelf` 📖	CompOp	2 math math: `whiskerOfIdCompIsoSelf_hom_right`, `whiskerOfIdCompIsoSelf_inv_right`
`whiskering` 📖	CompOp	2 math math: `whiskering_map`, `whiskering_obj`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofIdComp_hom` 📖	mathematical	—	`CategoryTheory.Comma.hom` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Bicategory.postcomp` `ofIdComp` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.CategoryStruct.id` `lift` `CategoryTheory.Iso.inv` `CategoryTheory.Bicategory.leftUnitor` `unit`	—	—
`ofIdComp_left_as` 📖	mathematical	—	`CategoryTheory.Discrete.as` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Bicategory.postcomp` `ofIdComp`	—	—
`ofIdComp_right` 📖	mathematical	—	`CategoryTheory.Comma.right` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Bicategory.postcomp` `ofIdComp` `lift` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CategoryStruct.id`	—	—
`w` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `lift` `CategoryTheory.Comma.right` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Bicategory.postcomp` `unit` `CategoryTheory.Bicategory.whiskerRight` `CategoryTheory.CommaMorphism.right`	—	`CategoryTheory.StructuredArrow.w`
`w_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `lift` `unit` `CategoryTheory.Comma.right` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Bicategory.postcomp` `CategoryTheory.Bicategory.whiskerRight` `CategoryTheory.CommaMorphism.right`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `w`
`whiskerHom_right` 📖	mathematical	—	`CategoryTheory.CommaMorphism.right` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bicategory.postcomp` `whisker` `whiskerHom` `CategoryTheory.Bicategory.whiskerLeft` `lift`	—	—
`whiskerIdCancel_right` 📖	mathematical	—	`CategoryTheory.CommaMorphism.right` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Bicategory.postcomp` `ofIdComp` `whiskerIdCancel` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `lift` `CategoryTheory.CategoryStruct.id` `whisker` `CategoryTheory.Iso.hom` `CategoryTheory.Bicategory.leftUnitor`	—	—
`whiskerOfIdCompIsoSelf_hom_right` 📖	mathematical	—	`CategoryTheory.CommaMorphism.right` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Bicategory.postcomp` `ofIdComp` `whisker` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Iso.hom` `CategoryTheory.Bicategory.LeftLift` `CategoryTheory.instCategoryStructuredArrow` `whiskerOfIdCompIsoSelf` `CategoryTheory.CategoryStruct.comp` `lift` `CategoryTheory.Comma.right` `CategoryTheory.Bicategory.leftUnitor`	—	—
`whiskerOfIdCompIsoSelf_inv_right` 📖	mathematical	—	`CategoryTheory.CommaMorphism.right` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Bicategory.postcomp` `ofIdComp` `whisker` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Iso.inv` `CategoryTheory.Bicategory.LeftLift` `CategoryTheory.instCategoryStructuredArrow` `whiskerOfIdCompIsoSelf` `CategoryTheory.CategoryStruct.comp` `lift` `CategoryTheory.Comma.right` `CategoryTheory.Bicategory.leftUnitor`	—	—
`whisker_lift` 📖	mathematical	—	`lift` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bicategory.toCategoryStruct` `whisker`	—	—
`whisker_unit` 📖	mathematical	—	`unit` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bicategory.toCategoryStruct` `whisker` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `lift` `CategoryTheory.Bicategory.whiskerLeft` `CategoryTheory.Iso.inv` `CategoryTheory.Bicategory.associator`	—	—
`whiskering_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.Bicategory.LeftLift` `CategoryTheory.instCategoryStructuredArrow` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Bicategory.postcomp` `CategoryTheory.CategoryStruct.comp` `whiskering` `homMk` `whisker` `CategoryTheory.Bicategory.whiskerLeft` `lift` `CategoryTheory.CommaMorphism.right` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit`	—	—
`whiskering_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.Bicategory.LeftLift` `CategoryTheory.instCategoryStructuredArrow` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Bicategory.postcomp` `CategoryTheory.CategoryStruct.comp` `whiskering` `whisker`	—	—

CategoryTheory.Bicategory.RightExtension

Definitions

Name	Category	Theorems
`alongId` 📖	CompOp	—
`counit` 📖	CompOp	2 math math: `w_assoc`, `w`
`extension` 📖	CompOp	—
`homMk` 📖	CompOp	—
`instInhabitedId` 📖	CompOp	—
`mk` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`w` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Bicategory.precomp` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Bicategory.whiskerLeft` `CategoryTheory.CommaMorphism.left` `counit`	—	`CategoryTheory.CostructuredArrow.w`
`w_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Bicategory.precomp` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Bicategory.whiskerLeft` `CategoryTheory.CommaMorphism.left` `counit`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `w`

CategoryTheory.Bicategory.RightLift

Definitions

Name	Category	Theorems
`alongId` 📖	CompOp	—
`counit` 📖	CompOp	2 math math: `w_assoc`, `w`
`homMk` 📖	CompOp	—
`instInhabitedId` 📖	CompOp	—
`mk` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`w` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Bicategory.postcomp` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Bicategory.whiskerRight` `CategoryTheory.CommaMorphism.left` `counit`	—	`CategoryTheory.CostructuredArrow.w`
`w_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Bicategory.postcomp` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Bicategory.whiskerRight` `CategoryTheory.CommaMorphism.left` `counit`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `w`

CategoryTheory.Functor.WellOrderInductionData

Definitions

Name	Category	Theorems
`Extension` 📖	CompData	2 math math: `Extension.instSubsingletonOfWellFoundedLT`, `Extension.instNonempty`

---

← Back to Index