Theorems · Definition · category theory
CategoryTheory.Bicategory.lanUnit
{B : Type u} →
[inst : CategoryTheory.Bicategory B] →
{a b c : B} →
(f : a ⟶ b) →
(g : a ⟶ c) →
[inst_1 : CategoryTheory.Bicategory.HasLeftKanExtension f g] →
g ⟶ CategoryTheory.CategoryStruct.comp f (CategoryTheory.Bicategory.lan f g)The unit for the left Kan extension f⁺ g.
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 30 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.CategoryStruct.compstatement · cited by 17,999
- CategoryTheory.Bicategorystatement and proof · cited by 1,587
- CategoryTheory.Bicategory.HasLeftKanExtensionstatement and proof · cited by 19
- CategoryTheory.Bicategory.LeftExtension.unitproof · cited by 12
- CategoryTheory.Bicategory.lanLeftExtensionproof · cited by 10
- CategoryTheory.Bicategory.lanstatement · cited by 8
Cited by5
Results whose statement or proof uses this declaration.
- CategoryTheory.Bicategory.lanUnit_descstatement · cited by 1
- CategoryTheory.Bicategory.lanLeftExtension_unitstatement · cited by 0
- CategoryTheory.Bicategory.Lan.CommuteWith.of_lan_comp_isostatement and proof · cited by 0
- CategoryTheory.Bicategory.Lan.existsUniquestatement · cited by 0
- CategoryTheory.Bicategory.lanUnit_desc_assocstatement and proof · cited by 0