Structures · Category theory
CategoryTheory.Bicategory.HasLeftKanExtension
The existence of a left Kan extension of g along f.
- Shape
- 2 explicit arguments · adds hasInitial
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by27
- CategoryTheory.Bicategory.lanLeftExtension
- CategoryTheory.Bicategory.lan
- CategoryTheory.Bicategory.lanIsKan
- CategoryTheory.Bicategory.lanDesc
- CategoryTheory.Bicategory.lanUnit
- CategoryTheory.Bicategory.Lan.CommuteWith.isKan
- CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIso
- CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIsoWhisker
- CategoryTheory.Bicategory.lanUnit_desc
- CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIsoWhisker_inv_right
- CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIso_hom
- CategoryTheory.Bicategory.Lan.CommuteWith.isKan.congr_simp
- CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIsoWhisker_hom_right
- CategoryTheory.Bicategory.Lan.CommuteWith.of_isKan_whisker
- CategoryTheory.Bicategory.lanIsKan_desc
- CategoryTheory.Bicategory.lanUnit_desc_assoc
- CategoryTheory.Bicategory.Lan.existsUnique
- CategoryTheory.Bicategory.LeftExtension.instCommuteWithOfIsLeftAdjoint
- CategoryTheory.Bicategory.Lan.CommuteWith.isKanWhisker
- CategoryTheory.Bicategory.Lan.CommuteWith.of_lan_comp_iso
- CategoryTheory.Bicategory.lanLeftExtension_unit
- CategoryTheory.Bicategory.lanLeftExtension_extension
- CategoryTheory.Bicategory.Lan.CommuteWith.instHasLeftKanExtensionComp
- CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIso_inv
- CategoryTheory.Bicategory.HasLeftKanExtension.hasInitial
- CategoryTheory.Bicategory.lan.congr_simp
- CategoryTheory.Bicategory.instHasInitialLeftExtensionOfHasLeftKanExtension
Ancestors0
No ancestors.