Theorems · Theorem · category theory
CategoryTheory.Cat.whiskerLeft_app
∀ {C D E : CategoryTheory.Cat} (F : C ⟶ D) {G H : D ⟶ E} (η : G ⟶ H) (X : ↑C),
(CategoryTheory.Bicategory.whiskerLeft F η).toNatTrans.app X = η.toNatTrans.app (F.toFunctor.obj X)- Defined in
- Mathlib.CategoryTheory.Category.Cat
- Cited by
- 51 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.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement · cited by 32,673
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.Functor.objstatement and proof · cited by 19,642
- CategoryTheory.CategoryStruct.compstatement · cited by 17,999
- CategoryTheory.NatTrans.appstatement and proof · cited by 7,406
- CategoryTheory.Catstatement and proof · cited by 884
- CategoryTheory.Bundled.αstatement and proof · cited by 736
- CategoryTheory.Cat.Hom.toFunctorstatement and proof · cited by 531
- CategoryTheory.Bicategory.whiskerLeftstatement · cited by 524
- CategoryTheory.Cat.Hom₂.toNatTransstatement and proof · cited by 277
Cited by51
Results whose statement or proof uses this declaration.
- CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom_appproof · cited by 2
- CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv_appproof · cited by 2
- CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom_appproof · cited by 1
- CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv_appproof · cited by 1
- CategoryTheory.Pseudofunctor.map₂_associator_appproof · cited by 1
- CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_hom_appproof · cited by 1
- CategoryTheory.Pseudofunctor.map₂_right_unitor_appproof · cited by 1
- CategoryTheory.Pseudofunctor.map₂_whisker_left_appproof · cited by 1
- CategoryTheory.LaxFunctor.mapComp_assoc_left_appproof · cited by 1
- CategoryTheory.LaxFunctor.mapComp_assoc_right_appproof · cited by 1
- CategoryTheory.LaxFunctor.mapComp_naturality_right_appproof · cited by 1