Documentation Verification Report

HasKan

📁 Source: Mathlib/CategoryTheory/Bicategory/Kan/HasKan.lean

Statistics

Metric	Count
Definitions `HasAbsLeftKanExtension`, `HasAbsLeftKanLift`, `HasLeftKanExtension`, `HasLeftKanLift`, `CommuteWith`, `isKan`, `isKanWhisker`, `lanCompIso`, `lanCompIsoWhisker`, `CommuteWith`, `isKan`, `isKanWhisker`, `lanLiftCompIso`, `lanLiftCompIsoWhisker`, `lan`, `lanDesc`, `lanIsKan`, `lanLeftExtension`, `lanLift`, `lanLiftDesc`, `lanLiftIsKan`, `lanLiftLeftLift`, `lanLiftUnit`, `lanUnit`, `«term_⁺_»`, `«term_₊_»`	26
Theorems `commute`, `toHasLeftKanExtension`, `commute`, `toHasLeftKanLift`, `hasInitial`, `hasInitial`, `commute`, `instHasLeftKanExtensionComp`, `lanCompIsoWhisker_hom_right`, `lanCompIsoWhisker_inv_right`, `lanCompIso_hom`, `lanCompIso_inv`, `of_isKan_whisker`, `of_lan_comp_iso`, `existsUnique`, `commute`, `instHasLeftKanLiftComp`, `lanLiftCompIsoWhisker_hom_right`, `lanLiftCompIsoWhisker_inv_right`, `lanLiftCompIso_hom`, `lanLiftCompIso_inv`, `of_isKan_whisker`, `of_lanLift_comp_iso`, `existsUnique`, `hasAbsLeftKanExtension`, `hasLeftKanExtension`, `hasAbsLeftKanLift`, `hasLeftKanLift`, `instCommuteWith`, `instCommuteWith_1`, `instHasInitialLeftExtensionOfHasLeftKanExtension`, `instHasInitialLeftLiftOfHasLeftKanLift`, `lanIsKan_desc`, `lanLeftExtension_extension`, `lanLeftExtension_unit`, `lanLiftIsKan_desc`, `lanLiftLeftLift_lift`, `lanLiftLeftLift_unit`, `lanLiftUnit_desc`, `lanLiftUnit_desc_assoc`, `lanUnit_desc`, `lanUnit_desc_assoc`	42
Total	68

CategoryTheory.Bicategory

Definitions

Name	Category	Theorems
`HasAbsLeftKanExtension` 📖	CompData	2 math math: `isLeftAdjoint_TFAE`, `LeftExtension.IsAbsKan.hasAbsLeftKanExtension`
`HasAbsLeftKanLift` 📖	CompData	2 math math: `LeftLift.IsAbsKan.hasAbsLeftKanLift`, `isRightAdjoint_TFAE`
`HasLeftKanExtension` 📖	CompData	4 math math: `isLeftAdjoint_TFAE`, `LeftExtension.IsKan.hasLeftKanExtension`, `Lan.CommuteWith.instHasLeftKanExtensionComp`, `HasAbsLeftKanExtension.toHasLeftKanExtension`
`HasLeftKanLift` 📖	CompData	4 math math: `LanLift.CommuteWith.instHasLeftKanLiftComp`, `HasAbsLeftKanLift.toHasLeftKanLift`, `isRightAdjoint_TFAE`, `LeftLift.IsKan.hasLeftKanLift`
`lan` 📖	CompOp	6 math math: `Lan.existsUnique`, `Lan.CommuteWith.lanCompIso_inv`, `Lan.CommuteWith.lanCompIso_hom`, `lanUnit_desc`, `lanLeftExtension_extension`, `lanUnit_desc_assoc`
`lanDesc` 📖	CompOp	5 math math: `Lan.CommuteWith.lanCompIsoWhisker_hom_right`, `lanIsKan_desc`, `Lan.CommuteWith.lanCompIso_hom`, `lanUnit_desc`, `lanUnit_desc_assoc`
`lanIsKan` 📖	CompOp	1 math math: `lanIsKan_desc`
`lanLeftExtension` 📖	CompOp	8 math math: `Lan.CommuteWith.lanCompIso_inv`, `Lan.CommuteWith.lanCompIsoWhisker_hom_right`, `Lan.CommuteWith.lanCompIsoWhisker_inv_right`, `Lan.CommuteWith.commute`, `lanIsKan_desc`, `Lan.CommuteWith.lanCompIso_hom`, `lanLeftExtension_extension`, `lanLeftExtension_unit`
`lanLift` 📖	CompOp	6 math math: `LanLift.CommuteWith.lanLiftCompIso_hom`, `lanLiftUnit_desc_assoc`, `LanLift.existsUnique`, `lanLiftLeftLift_lift`, `lanLiftUnit_desc`, `LanLift.CommuteWith.lanLiftCompIso_inv`
`lanLiftDesc` 📖	CompOp	5 math math: `LanLift.CommuteWith.lanLiftCompIso_hom`, `lanLiftUnit_desc_assoc`, `lanLiftIsKan_desc`, `lanLiftUnit_desc`, `LanLift.CommuteWith.lanLiftCompIsoWhisker_hom_right`
`lanLiftIsKan` 📖	CompOp	1 math math: `lanLiftIsKan_desc`
`lanLiftLeftLift` 📖	CompOp	8 math math: `LanLift.CommuteWith.lanLiftCompIso_hom`, `lanLiftLeftLift_unit`, `lanLiftIsKan_desc`, `lanLiftLeftLift_lift`, `LanLift.CommuteWith.commute`, `LanLift.CommuteWith.lanLiftCompIsoWhisker_inv_right`, `LanLift.CommuteWith.lanLiftCompIso_inv`, `LanLift.CommuteWith.lanLiftCompIsoWhisker_hom_right`
`lanLiftUnit` 📖	CompOp	4 math math: `lanLiftUnit_desc_assoc`, `LanLift.existsUnique`, `lanLiftLeftLift_unit`, `lanLiftUnit_desc`
`lanUnit` 📖	CompOp	4 math math: `Lan.existsUnique`, `lanUnit_desc`, `lanUnit_desc_assoc`, `lanLeftExtension_unit`
`«term_⁺_»` 📖	CompOp	—
`«term_₊_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instCommuteWith` 📖	mathematical	—	`Lan.CommuteWith` `HasAbsLeftKanExtension.toHasLeftKanExtension`	—	`HasAbsLeftKanExtension.commute`
`instCommuteWith_1` 📖	mathematical	—	`LanLift.CommuteWith` `HasAbsLeftKanLift.toHasLeftKanLift`	—	`HasAbsLeftKanLift.commute`
`instHasInitialLeftExtensionOfHasLeftKanExtension` 📖	mathematical	—	`CategoryTheory.Limits.HasInitial` `LeftExtension` `CategoryTheory.instCategoryStructuredArrow` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `toCategoryStruct` `homCategory` `precomp`	—	`HasLeftKanExtension.hasInitial`
`instHasInitialLeftLiftOfHasLeftKanLift` 📖	mathematical	—	`CategoryTheory.Limits.HasInitial` `LeftLift` `CategoryTheory.instCategoryStructuredArrow` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `toCategoryStruct` `homCategory` `postcomp`	—	`HasLeftKanLift.hasInitial`
`lanIsKan_desc` 📖	mathematical	—	`LeftExtension.IsKan.desc` `lanLeftExtension` `lanIsKan` `lanDesc`	—	—
`lanLeftExtension_extension` 📖	mathematical	—	`LeftExtension.extension` `lanLeftExtension` `lan`	—	—
`lanLeftExtension_unit` 📖	mathematical	—	`LeftExtension.unit` `lanLeftExtension` `lanUnit`	—	—
`lanLiftIsKan_desc` 📖	mathematical	—	`LeftLift.IsKan.desc` `lanLiftLeftLift` `lanLiftIsKan` `lanLiftDesc`	—	—
`lanLiftLeftLift_lift` 📖	mathematical	—	`LeftLift.lift` `lanLiftLeftLift` `lanLift`	—	—
`lanLiftLeftLift_unit` 📖	mathematical	—	`LeftLift.unit` `lanLiftLeftLift` `lanLiftUnit`	—	—
`lanLiftUnit_desc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `toCategoryStruct` `CategoryTheory.Category.toCategoryStruct` `homCategory` `lanLift` `LeftLift.lift` `lanLiftUnit` `whiskerRight` `lanLiftDesc` `LeftLift.unit`	—	`LeftLift.IsKan.fac`
`lanLiftUnit_desc_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `toCategoryStruct` `CategoryTheory.Category.toCategoryStruct` `homCategory` `lanLift` `lanLiftUnit` `LeftLift.lift` `whiskerRight` `lanLiftDesc` `LeftLift.unit`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `lanLiftUnit_desc`
`lanUnit_desc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `toCategoryStruct` `CategoryTheory.Category.toCategoryStruct` `homCategory` `lan` `LeftExtension.extension` `lanUnit` `whiskerLeft` `lanDesc` `LeftExtension.unit`	—	`LeftExtension.IsKan.fac`
`lanUnit_desc_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `toCategoryStruct` `CategoryTheory.Category.toCategoryStruct` `homCategory` `lan` `lanUnit` `LeftExtension.extension` `whiskerLeft` `lanDesc` `LeftExtension.unit`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `lanUnit_desc`

CategoryTheory.Bicategory.HasAbsLeftKanExtension

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commute` 📖	mathematical	—	`CategoryTheory.Bicategory.Lan.CommuteWith` `toHasLeftKanExtension`	—	—
`toHasLeftKanExtension` 📖	mathematical	—	`CategoryTheory.Bicategory.HasLeftKanExtension`	—	—

CategoryTheory.Bicategory.HasAbsLeftKanLift

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commute` 📖	mathematical	—	`CategoryTheory.Bicategory.LanLift.CommuteWith` `toHasLeftKanLift`	—	—
`toHasLeftKanLift` 📖	mathematical	—	`CategoryTheory.Bicategory.HasLeftKanLift`	—	—

CategoryTheory.Bicategory.HasLeftKanExtension

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasInitial` 📖	mathematical	—	`CategoryTheory.Limits.HasInitial` `CategoryTheory.Bicategory.LeftExtension` `CategoryTheory.instCategoryStructuredArrow` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Bicategory.precomp`	—	—

CategoryTheory.Bicategory.HasLeftKanLift

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasInitial` 📖	mathematical	—	`CategoryTheory.Limits.HasInitial` `CategoryTheory.Bicategory.LeftLift` `CategoryTheory.instCategoryStructuredArrow` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Bicategory.postcomp`	—	—

CategoryTheory.Bicategory.Lan

Definitions

Name	Category	Theorems
`CommuteWith` 📖	CompData	6 math math: `CommuteWith.of_isKan_whisker`, `CategoryTheory.Bicategory.isLeftAdjoint_TFAE`, `CategoryTheory.Bicategory.HasAbsLeftKanExtension.commute`, `CategoryTheory.Bicategory.instCommuteWith`, `CategoryTheory.Bicategory.LeftExtension.instCommuteWithOfIsLeftAdjoint`, `CommuteWith.of_lan_comp_iso`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`existsUnique` 📖	mathematical	—	`ExistsUnique` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Bicategory.lan` `CategoryTheory.Bicategory.LeftExtension.extension` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bicategory.lanUnit` `CategoryTheory.Bicategory.whiskerLeft` `CategoryTheory.Bicategory.LeftExtension.unit`	—	`CategoryTheory.StructuredArrow.IsUniversal.existsUnique`

CategoryTheory.Bicategory.Lan.CommuteWith

Definitions

Name	Category	Theorems
`isKan` 📖	CompOp	2 math math: `lanCompIso_inv`, `lanCompIsoWhisker_inv_right`
`isKanWhisker` 📖	CompOp	—
`lanCompIso` 📖	CompOp	2 math math: `lanCompIso_inv`, `lanCompIso_hom`
`lanCompIsoWhisker` 📖	CompOp	2 math math: `lanCompIsoWhisker_hom_right`, `lanCompIsoWhisker_inv_right`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commute` 📖	mathematical	—	`CategoryTheory.Bicategory.LeftExtension.IsKan` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.LeftExtension.whisker` `CategoryTheory.Bicategory.lanLeftExtension`	—	—
`instHasLeftKanExtensionComp` 📖	mathematical	—	`CategoryTheory.Bicategory.HasLeftKanExtension` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bicategory.toCategoryStruct`	—	`CategoryTheory.Bicategory.LeftExtension.IsKan.hasLeftKanExtension`
`lanCompIsoWhisker_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.CategoryStruct.comp` `CategoryTheory.Bicategory.precomp` `CategoryTheory.Bicategory.lanLeftExtension` `instHasLeftKanExtensionComp` `CategoryTheory.Bicategory.LeftExtension.whisker` `CategoryTheory.Iso.hom` `CategoryTheory.Bicategory.LeftExtension` `CategoryTheory.instCategoryStructuredArrow` `lanCompIsoWhisker` `CategoryTheory.Bicategory.lanDesc`	—	`instHasLeftKanExtensionComp`
`lanCompIsoWhisker_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.CategoryStruct.comp` `CategoryTheory.Bicategory.precomp` `CategoryTheory.Bicategory.LeftExtension.whisker` `CategoryTheory.Bicategory.lanLeftExtension` `instHasLeftKanExtensionComp` `CategoryTheory.Iso.inv` `CategoryTheory.Bicategory.LeftExtension` `CategoryTheory.instCategoryStructuredArrow` `lanCompIsoWhisker` `CategoryTheory.Bicategory.LeftExtension.IsKan.desc` `isKan`	—	`instHasLeftKanExtensionComp`
`lanCompIso_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Bicategory.lan` `CategoryTheory.CategoryStruct.comp` `instHasLeftKanExtensionComp` `lanCompIso` `CategoryTheory.Bicategory.lanDesc` `CategoryTheory.Bicategory.LeftExtension.whisker` `CategoryTheory.Bicategory.lanLeftExtension`	—	`instHasLeftKanExtensionComp`
`lanCompIso_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Bicategory.lan` `CategoryTheory.CategoryStruct.comp` `instHasLeftKanExtensionComp` `lanCompIso` `CategoryTheory.Bicategory.LeftExtension.IsKan.desc` `CategoryTheory.Bicategory.LeftExtension.whisker` `CategoryTheory.Bicategory.lanLeftExtension` `isKan`	—	`instHasLeftKanExtensionComp`
`of_isKan_whisker` 📖	mathematical	—	`CategoryTheory.Bicategory.Lan.CommuteWith`	—	—
`of_lan_comp_iso` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Bicategory.lan` `CategoryTheory.Bicategory.lanUnit` `CategoryTheory.Bicategory.whiskerLeft` `CategoryTheory.Iso.hom` `CategoryTheory.Bicategory.whiskerRight` `CategoryTheory.Bicategory.associator`	`CategoryTheory.Bicategory.Lan.CommuteWith`	—	—

CategoryTheory.Bicategory.LanLift

Definitions

Name	Category	Theorems
`CommuteWith` 📖	CompData	5 math math: `CategoryTheory.Bicategory.HasAbsLeftKanLift.commute`, `CommuteWith.of_lanLift_comp_iso`, `CategoryTheory.Bicategory.instCommuteWith_1`, `CategoryTheory.Bicategory.isRightAdjoint_TFAE`, `CommuteWith.of_isKan_whisker`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`existsUnique` 📖	mathematical	—	`ExistsUnique` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Bicategory.lanLift` `CategoryTheory.Bicategory.LeftLift.lift` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bicategory.lanLiftUnit` `CategoryTheory.Bicategory.whiskerRight` `CategoryTheory.Bicategory.LeftLift.unit`	—	`CategoryTheory.StructuredArrow.IsUniversal.existsUnique`

CategoryTheory.Bicategory.LanLift.CommuteWith

Definitions

Name	Category	Theorems
`isKan` 📖	CompOp	2 math math: `lanLiftCompIsoWhisker_inv_right`, `lanLiftCompIso_inv`
`isKanWhisker` 📖	CompOp	—
`lanLiftCompIso` 📖	CompOp	2 math math: `lanLiftCompIso_hom`, `lanLiftCompIso_inv`
`lanLiftCompIsoWhisker` 📖	CompOp	2 math math: `lanLiftCompIsoWhisker_inv_right`, `lanLiftCompIsoWhisker_hom_right`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commute` 📖	mathematical	—	`CategoryTheory.Bicategory.LeftLift.IsKan` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.LeftLift.whisker` `CategoryTheory.Bicategory.lanLiftLeftLift`	—	—
`instHasLeftKanLiftComp` 📖	mathematical	—	`CategoryTheory.Bicategory.HasLeftKanLift` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Bicategory.toCategoryStruct`	—	`CategoryTheory.Bicategory.LeftLift.IsKan.hasLeftKanLift`
`lanLiftCompIsoWhisker_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.CategoryStruct.comp` `CategoryTheory.Bicategory.postcomp` `CategoryTheory.Bicategory.lanLiftLeftLift` `instHasLeftKanLiftComp` `CategoryTheory.Bicategory.LeftLift.whisker` `CategoryTheory.Iso.hom` `CategoryTheory.Bicategory.LeftLift` `CategoryTheory.instCategoryStructuredArrow` `lanLiftCompIsoWhisker` `CategoryTheory.Bicategory.lanLiftDesc`	—	`instHasLeftKanLiftComp`
`lanLiftCompIsoWhisker_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.CategoryStruct.comp` `CategoryTheory.Bicategory.postcomp` `CategoryTheory.Bicategory.LeftLift.whisker` `CategoryTheory.Bicategory.lanLiftLeftLift` `instHasLeftKanLiftComp` `CategoryTheory.Iso.inv` `CategoryTheory.Bicategory.LeftLift` `CategoryTheory.instCategoryStructuredArrow` `lanLiftCompIsoWhisker` `CategoryTheory.Bicategory.LeftLift.IsKan.desc` `isKan`	—	`instHasLeftKanLiftComp`
`lanLiftCompIso_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Bicategory.lanLift` `CategoryTheory.CategoryStruct.comp` `instHasLeftKanLiftComp` `lanLiftCompIso` `CategoryTheory.Bicategory.lanLiftDesc` `CategoryTheory.Bicategory.LeftLift.whisker` `CategoryTheory.Bicategory.lanLiftLeftLift`	—	`instHasLeftKanLiftComp`
`lanLiftCompIso_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Bicategory.lanLift` `CategoryTheory.CategoryStruct.comp` `instHasLeftKanLiftComp` `lanLiftCompIso` `CategoryTheory.Bicategory.LeftLift.IsKan.desc` `CategoryTheory.Bicategory.LeftLift.whisker` `CategoryTheory.Bicategory.lanLiftLeftLift` `isKan`	—	`instHasLeftKanLiftComp`
`of_isKan_whisker` 📖	mathematical	—	`CategoryTheory.Bicategory.LanLift.CommuteWith`	—	—
`of_lanLift_comp_iso` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Bicategory.toCategoryStruct` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Bicategory.homCategory` `CategoryTheory.Bicategory.lanLift` `CategoryTheory.Bicategory.lanLiftUnit` `CategoryTheory.Bicategory.whiskerRight` `CategoryTheory.Iso.hom` `CategoryTheory.Bicategory.whiskerLeft` `CategoryTheory.Iso.inv` `CategoryTheory.Bicategory.associator`	`CategoryTheory.Bicategory.LanLift.CommuteWith`	—	—

CategoryTheory.Bicategory.LeftExtension.IsAbsKan

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasAbsLeftKanExtension` 📖	mathematical	—	`CategoryTheory.Bicategory.HasAbsLeftKanExtension`	—	`CategoryTheory.Bicategory.LeftExtension.IsKan.hasLeftKanExtension`

CategoryTheory.Bicategory.LeftExtension.IsKan

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasLeftKanExtension` 📖	mathematical	—	`CategoryTheory.Bicategory.HasLeftKanExtension`	—	`CategoryTheory.Limits.IsInitial.hasInitial`

CategoryTheory.Bicategory.LeftLift.IsAbsKan

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasAbsLeftKanLift` 📖	mathematical	—	`CategoryTheory.Bicategory.HasAbsLeftKanLift`	—	`CategoryTheory.Bicategory.LeftLift.IsKan.hasLeftKanLift`

CategoryTheory.Bicategory.LeftLift.IsKan

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasLeftKanLift` 📖	mathematical	—	`CategoryTheory.Bicategory.HasLeftKanLift`	—	`CategoryTheory.Limits.IsInitial.hasInitial`

---

← Back to Index