Theorems · Definition · category theory
CategoryTheory.Bicategory.leftUnitor
{B : Type u} →
[self : CategoryTheory.Bicategory B] →
{a b : B} → (f : a ⟶ b) → CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) f ≅ fThe left unitor: 𝟙 a ≫ f ≅ f
- Defined in
- Mathlib.CategoryTheory.Bicategory.Basic
- Cited by
- 309 results in Mathlib
- Foundations
- Depth 3 from the axioms, rests on 12 definitions · uses no axioms
- Assumes
- CategoryTheory.Bicategory
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homstatement · cited by 32,603
- CategoryTheory.CategoryStruct.compstatement · cited by 17,999
- CategoryTheory.CategoryStruct.idstatement · cited by 6,235
- CategoryTheory.Isostatement · cited by 3,963
- CategoryTheory.Bicategorystatement and proof · cited by 1,587
Cited by423
Results whose statement or proof uses this declaration.
- CategoryTheory.Bicategory.conjugateEquivproof · cited by 41
- CategoryTheory.Cat.leftUnitor_hom_appstatement · cited by 11
- CategoryTheory.Bicategory.id_whiskerLeftstatement · cited by 9
- CategoryTheory.Bicategory.mateEquiv_apply'proof · cited by 9
- CategoryTheory.Bicategory.eqToHomTransIsoproof · cited by 7
- CategoryTheory.Bicategory.leftUnitor_whiskerRightstatement and proof · cited by 7
- CategoryTheory.Bicategory.Adjunction.homEquiv₁proof · cited by 7
- CategoryTheory.Bicategory.trianglestatement · cited by 7
- CategoryTheory.Bicategory.whiskerLeft_rightUnitorproof · cited by 7
- CategoryTheory.Bicategory.Prod.sectLproof · cited by 7
- CategoryTheory.Lax.LaxTrans.idproof · cited by 6
- CategoryTheory.Bicategory.unitors_inv_equalstatement and proof · cited by 6
Showing the 200 most cited of 423.