Loogle!

Result

Found 1199 declarations mentioning CategoryTheory.Cat. Of these, only the first 200 are shown.

• CategoryTheory.Cat 📋 Mathlib.CategoryTheory.Category.Cat
  : Type (max (u + 1) u (v + 1))
• CategoryTheory.Cat.bicategory 📋 Mathlib.CategoryTheory.Category.Cat
  : CategoryTheory.Bicategory CategoryTheory.Cat
• CategoryTheory.Cat.category 📋 Mathlib.CategoryTheory.Category.Cat
  : CategoryTheory.LargeCategory CategoryTheory.Cat
• CategoryTheory.Cat.instInhabited 📋 Mathlib.CategoryTheory.Category.Cat
  : Inhabited CategoryTheory.Cat
• CategoryTheory.Cat.instQuiver 📋 Mathlib.CategoryTheory.Category.Cat
  : Quiver CategoryTheory.Cat
• CategoryTheory.Cat.Hom 📋 Mathlib.CategoryTheory.Category.Cat
  (C D : CategoryTheory.Cat) : Type (max u v)
• CategoryTheory.Cat.instCoeSortType 📋 Mathlib.CategoryTheory.Category.Cat
  : CoeSort CategoryTheory.Cat (Type u)
• CategoryTheory.Cat.bicategory.strict 📋 Mathlib.CategoryTheory.Category.Cat
  : CategoryTheory.Bicategory.Strict CategoryTheory.Cat
• CategoryTheory.Cat.of 📋 Mathlib.CategoryTheory.Category.Cat
  (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.Cat
• CategoryTheory.typeToCat 📋 Mathlib.CategoryTheory.Category.Cat
  : CategoryTheory.Functor (Type u) CategoryTheory.Cat
• CategoryTheory.Cat.objects 📋 Mathlib.CategoryTheory.Category.Cat
  : CategoryTheory.Functor CategoryTheory.Cat (Type u)
• CategoryTheory.Cat.str 📋 Mathlib.CategoryTheory.Category.Cat
  (C : CategoryTheory.Cat) : CategoryTheory.Category.{v, u} ↑C
• CategoryTheory.instFaithfulCatTypeToCat 📋 Mathlib.CategoryTheory.Category.Cat
  : CategoryTheory.typeToCat.Faithful
• CategoryTheory.instFullCatTypeToCat 📋 Mathlib.CategoryTheory.Category.Cat
  : CategoryTheory.typeToCat.Full
• CategoryTheory.Cat.Hom.instCategory 📋 Mathlib.CategoryTheory.Category.Cat
  {X Y : CategoryTheory.Cat} : CategoryTheory.Category.{max u v, max u v} (X ⟶ Y)
• CategoryTheory.Cat.Hom.instQuiver 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : CategoryTheory.Cat} : Quiver (C ⟶ D)
• CategoryTheory.Cat.instCategoryObjObjects 📋 Mathlib.CategoryTheory.Category.Cat
  (X : CategoryTheory.Cat) : CategoryTheory.Category.{v, u} (CategoryTheory.Cat.objects.obj X)
• CategoryTheory.Cat.coe_of 📋 Mathlib.CategoryTheory.Category.Cat
  (C : CategoryTheory.Cat) : CategoryTheory.Cat.of ↑C = C
• CategoryTheory.Cat.Hom₂ 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : CategoryTheory.Cat} (F G : C ⟶ D) : Type (max u v)
• CategoryTheory.typeToCat_obj 📋 Mathlib.CategoryTheory.Category.Cat
  (X : Type u) : CategoryTheory.typeToCat.obj X = CategoryTheory.Cat.of (CategoryTheory.Discrete X)
• CategoryTheory.Cat.Hom.ofFunctor 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : CategoryTheory.Cat} (toFunctor : CategoryTheory.Functor ↑C ↑D) : C.Hom D
• CategoryTheory.Cat.Hom.toFunctor 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : CategoryTheory.Cat} (self : C.Hom D) : CategoryTheory.Functor ↑C ↑D
• CategoryTheory.Cat.equivOfIso 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : CategoryTheory.Cat} (γ : C ≅ D) : ↑C ≌ ↑D
• CategoryTheory.Cat.Hom.equivFunctor 📋 Mathlib.CategoryTheory.Category.Cat
  (C D : CategoryTheory.Cat) : (C ⟶ D) ≃ CategoryTheory.Functor ↑C ↑D
• CategoryTheory.Functor.toCatHom 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] (F : CategoryTheory.Functor C D) : CategoryTheory.Cat.of C ⟶ CategoryTheory.Cat.of D
• CategoryTheory.Functor.equivCatHom 📋 Mathlib.CategoryTheory.Category.Cat
  (C D : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] : CategoryTheory.Functor C D ≃ (CategoryTheory.Cat.of C ⟶ CategoryTheory.Cat.of D)
• CategoryTheory.Cat.id_eq_id 📋 Mathlib.CategoryTheory.Category.Cat
  (X : CategoryTheory.Cat) : (CategoryTheory.CategoryStruct.id X).toFunctor = CategoryTheory.Functor.id ↑X
• CategoryTheory.Cat.Hom.id_toFunctor 📋 Mathlib.CategoryTheory.Category.Cat
  {C : CategoryTheory.Cat} : (CategoryTheory.CategoryStruct.id C).toFunctor = CategoryTheory.Functor.id ↑C
• CategoryTheory.Cat.Hom.id_obj 📋 Mathlib.CategoryTheory.Category.Cat
  {C : CategoryTheory.Cat} (X : ↑C) : (CategoryTheory.CategoryStruct.id C).toFunctor.obj X = X
• CategoryTheory.Cat.Hom.ext 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : CategoryTheory.Cat} {x y : C.Hom D} (toFunctor : x.toFunctor = y.toFunctor) : x = y
• CategoryTheory.Cat.Hom.ext_iff 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : CategoryTheory.Cat} {x y : C.Hom D} : x = y ↔ x.toFunctor = y.toFunctor
• CategoryTheory.Cat.ext 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : CategoryTheory.Cat} {F G : C ⟶ D} (h : F.toFunctor = G.toFunctor) : F = G
• CategoryTheory.Cat.ext_iff 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : CategoryTheory.Cat} {F G : C ⟶ D} : F = G ↔ F.toFunctor = G.toFunctor
• CategoryTheory.Cat.Hom.toNatIso 📋 Mathlib.CategoryTheory.Category.Cat
  {X Y : CategoryTheory.Cat} {F G : X ⟶ Y} (e : F ≅ G) : F.toFunctor ≅ G.toFunctor
• CategoryTheory.Cat.Hom.isoMk 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] {F G : CategoryTheory.Functor C D} (e : F ≅ G) : F.toCatHom ≅ G.toCatHom
• CategoryTheory.Cat.comp_eq_comp 📋 Mathlib.CategoryTheory.Category.Cat
  {X Y Z : CategoryTheory.Cat} (F : X ⟶ Y) (G : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp F G).toFunctor = F.toFunctor.comp G.toFunctor
• CategoryTheory.Cat.Hom.comp_toFunctor 📋 Mathlib.CategoryTheory.Category.Cat
  {C D E : CategoryTheory.Cat} (F : C ⟶ D) (G : D ⟶ E) : (CategoryTheory.CategoryStruct.comp F G).toFunctor = F.toFunctor.comp G.toFunctor
• CategoryTheory.NatTrans.toCatHom₂ 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] {F G : CategoryTheory.Functor C D} (η : F ⟶ G) : F.toCatHom ⟶ G.toCatHom
• CategoryTheory.Cat.Hom.instIsIsoFunctorαCategoryToNatTransHomHom 📋 Mathlib.CategoryTheory.Category.Cat
  {X Y : CategoryTheory.Cat} {F G : X ⟶ Y} (e : F ≅ G) : CategoryTheory.IsIso e.hom.toNatTrans
• CategoryTheory.Cat.Hom.instIsIsoFunctorαCategoryToNatTransInvHom 📋 Mathlib.CategoryTheory.Category.Cat
  {X Y : CategoryTheory.Cat} {F G : X ⟶ Y} (e : F ≅ G) : CategoryTheory.IsIso e.inv.toNatTrans
• CategoryTheory.Cat.Hom₂.ofNatTrans 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : CategoryTheory.Cat} {F G : C ⟶ D} (toNatTrans : F.toFunctor ⟶ G.toFunctor) : CategoryTheory.Cat.Hom₂ F G
• CategoryTheory.Cat.Hom₂.toNatTrans 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : CategoryTheory.Cat} {F G : C ⟶ D} (self : CategoryTheory.Cat.Hom₂ F G) : F.toFunctor ⟶ G.toFunctor
• CategoryTheory.Cat.Hom.comp_obj 📋 Mathlib.CategoryTheory.Category.Cat
  {C D E : CategoryTheory.Cat} (F : C ⟶ D) (G : D ⟶ E) (X : ↑C) : (CategoryTheory.CategoryStruct.comp F G).toFunctor.obj X = G.toFunctor.obj (F.toFunctor.obj X)
• CategoryTheory.Cat.Hom.toNatIso_leftUnitor 📋 Mathlib.CategoryTheory.Category.Cat
  {B C : CategoryTheory.Cat} (F : B ⟶ C) : CategoryTheory.Cat.Hom.toNatIso (CategoryTheory.Bicategory.leftUnitor F) = F.toFunctor.leftUnitor
• CategoryTheory.NatTrans.toCatHom₂_id 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] (F : CategoryTheory.Functor C D) : CategoryTheory.NatTrans.toCatHom₂ (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id F.toCatHom
• CategoryTheory.Cat.Hom.id_map 📋 Mathlib.CategoryTheory.Category.Cat
  {C : CategoryTheory.Cat} {X Y : ↑C} (f : X ⟶ Y) : (CategoryTheory.CategoryStruct.id C).toFunctor.map f = f
• CategoryTheory.Cat.Hom.isoMk_toNatIso 📋 Mathlib.CategoryTheory.Category.Cat
  {X Y : CategoryTheory.Cat} {F G : X ⟶ Y} (e : F ≅ G) : CategoryTheory.Cat.Hom.isoMk (CategoryTheory.Cat.Hom.toNatIso e) = e
• CategoryTheory.typeToCat_map 📋 Mathlib.CategoryTheory.Category.Cat
  {X✝ Y✝ : Type u} (f : X✝ ⟶ Y✝) : CategoryTheory.typeToCat.map f = (CategoryTheory.Discrete.functor (CategoryTheory.Discrete.mk ∘ ⇑(CategoryTheory.ConcreteCategory.hom f))).toCatHom
• CategoryTheory.Functor.equivCatHom_apply 📋 Mathlib.CategoryTheory.Category.Cat
  (C D : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] (F : CategoryTheory.Functor C D) : (CategoryTheory.Functor.equivCatHom C D) F = F.toCatHom
• CategoryTheory.Cat.Hom₂.ext 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : CategoryTheory.Cat} {F G : C ⟶ D} {η₁ η₂ : F ⟶ G} (h : η₁.toNatTrans = η₂.toNatTrans) : η₁ = η₂
• CategoryTheory.Cat.Hom.isoMk_hom 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] {F G : CategoryTheory.Functor C D} (e : F ≅ G) : (CategoryTheory.Cat.Hom.isoMk e).hom = CategoryTheory.NatTrans.toCatHom₂ e.hom
• CategoryTheory.Cat.Hom.isoMk_inv 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] {F G : CategoryTheory.Functor C D} (e : F ≅ G) : (CategoryTheory.Cat.Hom.isoMk e).inv = CategoryTheory.NatTrans.toCatHom₂ e.inv
• CategoryTheory.Cat.Hom₂.ext_iff 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : CategoryTheory.Cat} {F G : C ⟶ D} {η₁ η₂ : F ⟶ G} : η₁ = η₂ ↔ η₁.toNatTrans = η₂.toNatTrans
• CategoryTheory.Cat.Hom.toNatTrans_id 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : CategoryTheory.Cat} (F : C ⟶ D) : (CategoryTheory.CategoryStruct.id F).toNatTrans = CategoryTheory.CategoryStruct.id F.toFunctor
• CategoryTheory.Cat.Hom₂.id_app 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : CategoryTheory.Cat} (F : C ⟶ D) (X : ↑C) : (CategoryTheory.CategoryStruct.id F).toNatTrans.app X = CategoryTheory.CategoryStruct.id (F.toFunctor.obj X)
• CategoryTheory.Cat.Hom.toNatIso_hom 📋 Mathlib.CategoryTheory.Category.Cat
  {X Y : CategoryTheory.Cat} {F G : X ⟶ Y} (e : F ≅ G) : (CategoryTheory.Cat.Hom.toNatIso e).hom = e.hom.toNatTrans
• CategoryTheory.Cat.Hom.toNatIso_inv 📋 Mathlib.CategoryTheory.Category.Cat
  {X Y : CategoryTheory.Cat} {F G : X ⟶ Y} (e : F ≅ G) : (CategoryTheory.Cat.Hom.toNatIso e).inv = e.inv.toNatTrans
• CategoryTheory.Cat.Hom.equivFunctor_apply 📋 Mathlib.CategoryTheory.Category.Cat
  (C D : CategoryTheory.Cat) (a✝ : CategoryTheory.Cat.of ↑C ⟶ CategoryTheory.Cat.of ↑D) : (CategoryTheory.Cat.Hom.equivFunctor C D) a✝ = a✝.toFunctor
• CategoryTheory.Functor.equivCatHom_symm_apply 📋 Mathlib.CategoryTheory.Category.Cat
  (C D : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] (self : (CategoryTheory.Cat.of C).Hom (CategoryTheory.Cat.of D)) : (CategoryTheory.Functor.equivCatHom C D).symm self = self.toFunctor
• CategoryTheory.Cat.Hom.equivFunctor_symm_apply 📋 Mathlib.CategoryTheory.Category.Cat
  (C D : CategoryTheory.Cat) (a✝ : CategoryTheory.Functor ↑C ↑D) : (CategoryTheory.Cat.Hom.equivFunctor C D).symm a✝ = a✝.toCatHom
• CategoryTheory.Cat.whiskerLeft_toNatTrans 📋 Mathlib.CategoryTheory.Category.Cat
  {C D E : CategoryTheory.Cat} (F : C ⟶ D) {G H : D ⟶ E} (η : G ⟶ H) : (CategoryTheory.Bicategory.whiskerLeft F η).toNatTrans = F.toFunctor.whiskerLeft η.toNatTrans
• CategoryTheory.Cat.whiskerRight_toNatTrans 📋 Mathlib.CategoryTheory.Category.Cat
  {C D E : CategoryTheory.Cat} {F G : C ⟶ D} (H : D ⟶ E) (η : F ⟶ G) : (CategoryTheory.Bicategory.whiskerRight η H).toNatTrans = CategoryTheory.Functor.whiskerRight η.toNatTrans H.toFunctor
• CategoryTheory.Cat.Hom.toNatIso_associator 📋 Mathlib.CategoryTheory.Category.Cat
  {B C D E : CategoryTheory.Cat} (F : B ⟶ C) (G : C ⟶ D) (H : D ⟶ E) : CategoryTheory.Cat.Hom.toNatIso (CategoryTheory.Bicategory.associator F G H) = F.toFunctor.associator G.toFunctor H.toFunctor
• CategoryTheory.Cat.Hom.toNatTrans_comp 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : CategoryTheory.Cat} {F G H : C ⟶ D} (η₁ : F ⟶ G) (η₂ : G ⟶ H) : (CategoryTheory.CategoryStruct.comp η₁ η₂).toNatTrans = CategoryTheory.CategoryStruct.comp η₁.toNatTrans η₂.toNatTrans
• CategoryTheory.NatTrans.toCatHom₂_comp 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] {F G H : CategoryTheory.Functor C D} (η₁ : F ⟶ G) (η₂ : G ⟶ H) : CategoryTheory.NatTrans.toCatHom₂ (CategoryTheory.CategoryStruct.comp η₁ η₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.toCatHom₂ η₁) (CategoryTheory.NatTrans.toCatHom₂ η₂)
• CategoryTheory.Cat.Hom.comp_map 📋 Mathlib.CategoryTheory.Category.Cat
  {C D E : CategoryTheory.Cat} (F : C ⟶ D) (G : D ⟶ E) {X Y : ↑C} (f : X ⟶ Y) : (CategoryTheory.CategoryStruct.comp F G).toFunctor.map f = G.toFunctor.map (F.toFunctor.map f)
• CategoryTheory.Cat.Hom.hom_inv_id_toNatTrans 📋 Mathlib.CategoryTheory.Category.Cat
  {X Y : CategoryTheory.Cat} {F G : X ⟶ Y} (e : F ≅ G) : CategoryTheory.CategoryStruct.comp e.hom.toNatTrans e.inv.toNatTrans = CategoryTheory.CategoryStruct.id F.toFunctor
• CategoryTheory.Cat.Hom.inv_hom_id_toNatTrans 📋 Mathlib.CategoryTheory.Category.Cat
  {X Y : CategoryTheory.Cat} {F G : X ⟶ Y} (e : F ≅ G) : CategoryTheory.CategoryStruct.comp e.inv.toNatTrans e.hom.toNatTrans = CategoryTheory.CategoryStruct.id G.toFunctor
• CategoryTheory.Cat.leftUnitor_hom_toNatTrans 📋 Mathlib.CategoryTheory.Category.Cat
  {B C : CategoryTheory.Cat} (F : B ⟶ C) : (CategoryTheory.Bicategory.leftUnitor F).hom.toNatTrans = F.toFunctor.leftUnitor.hom
• CategoryTheory.Cat.leftUnitor_inv_toNatTrans 📋 Mathlib.CategoryTheory.Category.Cat
  {B C : CategoryTheory.Cat} (F : B ⟶ C) : (CategoryTheory.Bicategory.leftUnitor F).inv.toNatTrans = F.toFunctor.leftUnitor.inv
• CategoryTheory.Cat.rightUnitor_hom_toNatTrans 📋 Mathlib.CategoryTheory.Category.Cat
  {B C : CategoryTheory.Cat} (F : B ⟶ C) : (CategoryTheory.Bicategory.rightUnitor F).hom.toNatTrans = F.toFunctor.rightUnitor.hom
• CategoryTheory.Cat.rightUnitor_inv_toNatTrans 📋 Mathlib.CategoryTheory.Category.Cat
  {B C : CategoryTheory.Cat} (F : B ⟶ C) : (CategoryTheory.Bicategory.rightUnitor F).inv.toNatTrans = F.toFunctor.rightUnitor.inv
• CategoryTheory.Cat.whiskerLeft_app 📋 Mathlib.CategoryTheory.Category.Cat
  {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)
• CategoryTheory.Cat.leftUnitor_hom_app 📋 Mathlib.CategoryTheory.Category.Cat
  {B C : CategoryTheory.Cat} (F : B ⟶ C) (X : ↑B) : (CategoryTheory.Bicategory.leftUnitor F).hom.toNatTrans.app X = CategoryTheory.eqToHom ⋯
• CategoryTheory.Cat.leftUnitor_inv_app 📋 Mathlib.CategoryTheory.Category.Cat
  {B C : CategoryTheory.Cat} (F : B ⟶ C) (X : ↑B) : (CategoryTheory.Bicategory.leftUnitor F).inv.toNatTrans.app X = CategoryTheory.eqToHom ⋯
• CategoryTheory.Cat.rightUnitor_hom_app 📋 Mathlib.CategoryTheory.Category.Cat
  {B C : CategoryTheory.Cat} (F : B ⟶ C) (X : ↑B) : (CategoryTheory.Bicategory.rightUnitor F).hom.toNatTrans.app X = CategoryTheory.eqToHom ⋯
• CategoryTheory.Cat.rightUnitor_inv_app 📋 Mathlib.CategoryTheory.Category.Cat
  {B C : CategoryTheory.Cat} (F : B ⟶ C) (X : ↑B) : (CategoryTheory.Bicategory.rightUnitor F).inv.toNatTrans.app X = CategoryTheory.eqToHom ⋯
• CategoryTheory.Cat.Hom.hom_inv_id_toNatTrans_app 📋 Mathlib.CategoryTheory.Category.Cat
  {X Y : CategoryTheory.Cat} {F G : X ⟶ Y} (e : F ≅ G) (A : ↑X) : CategoryTheory.CategoryStruct.comp (e.hom.toNatTrans.app A) (e.inv.toNatTrans.app A) = CategoryTheory.CategoryStruct.id (F.toFunctor.obj A)
• CategoryTheory.Cat.Hom.inv_hom_id_toNatTrans_app 📋 Mathlib.CategoryTheory.Category.Cat
  {X Y : CategoryTheory.Cat} {F G : X ⟶ Y} (e : F ≅ G) (A : ↑X) : CategoryTheory.CategoryStruct.comp (e.inv.toNatTrans.app A) (e.hom.toNatTrans.app A) = CategoryTheory.CategoryStruct.id (G.toFunctor.obj A)
• CategoryTheory.Cat.whiskerRight_app 📋 Mathlib.CategoryTheory.Category.Cat
  {C D E : CategoryTheory.Cat} {F G : C ⟶ D} (H : D ⟶ E) (η : F ⟶ G) (X : ↑C) : (CategoryTheory.Bicategory.whiskerRight η H).toNatTrans.app X = H.toFunctor.map (η.toNatTrans.app X)
• CategoryTheory.Cat.Hom₂.comp_app 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : CategoryTheory.Cat} {F G H : C ⟶ D} (α : F ⟶ G) (β : G ⟶ H) (X : ↑C) : (CategoryTheory.CategoryStruct.comp α β).toNatTrans.app X = CategoryTheory.CategoryStruct.comp (α.toNatTrans.app X) (β.toNatTrans.app X)
• CategoryTheory.Cat.Hom₂.eqToHom_toNatTrans 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : CategoryTheory.Cat} {F G : C ⟶ D} (h : F = G) : (CategoryTheory.eqToHom h).toNatTrans = CategoryTheory.eqToHom ⋯
• CategoryTheory.Cat.Hom.hom_inv_id_toNatTrans_app_assoc 📋 Mathlib.CategoryTheory.Category.Cat
  {X Y : CategoryTheory.Cat} {F G : X ⟶ Y} (e : F ≅ G) (A : ↑X) {Z : ↑Y} (h : F.toFunctor.obj A ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.hom.toNatTrans.app A) (CategoryTheory.CategoryStruct.comp (e.inv.toNatTrans.app A) h) = h
• CategoryTheory.Cat.Hom.inv_hom_id_toNatTrans_app_assoc 📋 Mathlib.CategoryTheory.Category.Cat
  {X Y : CategoryTheory.Cat} {F G : X ⟶ Y} (e : F ≅ G) (A : ↑X) {Z : ↑Y} (h : G.toFunctor.obj A ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.inv.toNatTrans.app A) (CategoryTheory.CategoryStruct.comp (e.hom.toNatTrans.app A) h) = h
• CategoryTheory.Cat.Hom.hom_inv_id_toNatTrans_assoc 📋 Mathlib.CategoryTheory.Category.Cat
  {X Y : CategoryTheory.Cat} {F G : X ⟶ Y} (e : F ≅ G) {Z : CategoryTheory.Functor ↑X ↑Y} (h : F.toFunctor ⟶ Z) : CategoryTheory.CategoryStruct.comp e.hom.toNatTrans (CategoryTheory.CategoryStruct.comp e.inv.toNatTrans h) = h
• CategoryTheory.Cat.Hom.inv_hom_id_toNatTrans_assoc 📋 Mathlib.CategoryTheory.Category.Cat
  {X Y : CategoryTheory.Cat} {F G : X ⟶ Y} (e : F ≅ G) {Z : CategoryTheory.Functor ↑X ↑Y} (h : G.toFunctor ⟶ Z) : CategoryTheory.CategoryStruct.comp e.inv.toNatTrans (CategoryTheory.CategoryStruct.comp e.hom.toNatTrans h) = h
• CategoryTheory.Cat.eqToHom_app 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : CategoryTheory.Cat} (F G : C ⟶ D) (h : F = G) (X : ↑C) : (CategoryTheory.eqToHom h).toNatTrans.app X = CategoryTheory.eqToHom ⋯
• CategoryTheory.Cat.Hom₂.comp_app_assoc 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : CategoryTheory.Cat} {F G H : C ⟶ D} (α : F ⟶ G) (β : G ⟶ H) (X : ↑C) {Z : ↑D} (h : H.toFunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp α β).toNatTrans.app X) h = CategoryTheory.CategoryStruct.comp (α.toNatTrans.app X) (CategoryTheory.CategoryStruct.comp (β.toNatTrans.app X) h)
• CategoryTheory.Cat.associator_hom_app 📋 Mathlib.CategoryTheory.Category.Cat
  {B C D E : CategoryTheory.Cat} (F : B ⟶ C) (G : C ⟶ D) (H : D ⟶ E) (X : ↑B) : (CategoryTheory.Bicategory.associator F G H).hom.toNatTrans.app X = CategoryTheory.eqToHom ⋯
• CategoryTheory.Cat.associator_inv_app 📋 Mathlib.CategoryTheory.Category.Cat
  {B C D E : CategoryTheory.Cat} (F : B ⟶ C) (G : C ⟶ D) (H : D ⟶ E) (X : ↑B) : (CategoryTheory.Bicategory.associator F G H).inv.toNatTrans.app X = CategoryTheory.eqToHom ⋯
• CategoryTheory.Cat.associator_hom_toNatTrans 📋 Mathlib.CategoryTheory.Category.Cat
  {B C D E : CategoryTheory.Cat} (F : B ⟶ C) (G : C ⟶ D) (H : D ⟶ E) : (CategoryTheory.Bicategory.associator F G H).hom.toNatTrans = (F.toFunctor.associator G.toFunctor H.toFunctor).hom
• CategoryTheory.Cat.associator_inv_toNatTrans 📋 Mathlib.CategoryTheory.Category.Cat
  {B C D E : CategoryTheory.Cat} (F : B ⟶ C) (G : C ⟶ D) (H : D ⟶ E) : (CategoryTheory.Bicategory.associator F G H).inv.toNatTrans = (F.toFunctor.associator G.toFunctor H.toFunctor).inv
• CategoryTheory.Cat.Hom.toNatIso_rightUnitor 📋 Mathlib.CategoryTheory.Category.Cat
  {B C : CategoryTheory.Cat} (F : B ⟶ C) : CategoryTheory.Cat.Hom.toNatIso (CategoryTheory.Bicategory.rightUnitor F) = CategoryTheory.eqToIso ⋯ ≪≫ F.toFunctor.rightUnitor ≪≫ CategoryTheory.eqToIso ⋯
• CategoryTheory.Cat.isoOfEquiv 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : CategoryTheory.Cat} (e : ↑C ≌ ↑D) (h₁ : ∀ (X : ↑C), e.inverse.obj (e.functor.obj X) = X) (h₂ : ∀ (Y : ↑D), e.functor.obj (e.inverse.obj Y) = Y) (h₃ : ∀ (X : ↑C), e.unitIso.hom.app X = CategoryTheory.eqToHom ⋯ := by cat_disch) (h₄ : ∀ (Y : ↑D), e.counitIso.hom.app Y = CategoryTheory.eqToHom ⋯ := by cat_disch) : C ≅ D
• CategoryTheory.Cat.isoOfEquiv_hom 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : CategoryTheory.Cat} (e : ↑C ≌ ↑D) (h₁ : ∀ (X : ↑C), e.inverse.obj (e.functor.obj X) = X) (h₂ : ∀ (Y : ↑D), e.functor.obj (e.inverse.obj Y) = Y) (h₃ : ∀ (X : ↑C), e.unitIso.hom.app X = CategoryTheory.eqToHom ⋯ := by cat_disch) (h₄ : ∀ (Y : ↑D), e.counitIso.hom.app Y = CategoryTheory.eqToHom ⋯ := by cat_disch) : (CategoryTheory.Cat.isoOfEquiv e h₁ h₂ h₃ h₄).hom = e.functor.toCatHom
• CategoryTheory.Cat.isoOfEquiv_inv 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : CategoryTheory.Cat} (e : ↑C ≌ ↑D) (h₁ : ∀ (X : ↑C), e.inverse.obj (e.functor.obj X) = X) (h₂ : ∀ (Y : ↑D), e.functor.obj (e.inverse.obj Y) = Y) (h₃ : ∀ (X : ↑C), e.unitIso.hom.app X = CategoryTheory.eqToHom ⋯ := by cat_disch) (h₄ : ∀ (Y : ↑D), e.counitIso.hom.app Y = CategoryTheory.eqToHom ⋯ := by cat_disch) : (CategoryTheory.Cat.isoOfEquiv e h₁ h₂ h₃ h₄).inv = e.inverse.toCatHom
• CategoryTheory.isomorphismClasses 📋 Mathlib.CategoryTheory.IsomorphismClasses
  : CategoryTheory.Functor CategoryTheory.Cat (Type u)
• CategoryTheory.Over.mapFunctor 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  (T : Type u₁) [CategoryTheory.Category.{v₁, u₁} T] : CategoryTheory.Functor T CategoryTheory.Cat
• CategoryTheory.Under.mapFunctor 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  (T : Type u₁) [CategoryTheory.Category.{v₁, u₁} T] : CategoryTheory.Functor Tᵒᵖ CategoryTheory.Cat
• CategoryTheory.Over.mapFunctor_obj 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  (T : Type u₁) [CategoryTheory.Category.{v₁, u₁} T] (X : T) : (CategoryTheory.Over.mapFunctor T).obj X = CategoryTheory.Cat.of (CategoryTheory.Over X)
• CategoryTheory.Under.mapFunctor_obj 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  (T : Type u₁) [CategoryTheory.Category.{v₁, u₁} T] (X : Tᵒᵖ) : (CategoryTheory.Under.mapFunctor T).obj X = CategoryTheory.Cat.of (CategoryTheory.Under (Opposite.unop X))
• CategoryTheory.Over.mapFunctor_map 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  (T : Type u₁) [CategoryTheory.Category.{v₁, u₁} T] {X✝ Y✝ : T} (f : X✝ ⟶ Y✝) : (CategoryTheory.Over.mapFunctor T).map f = (CategoryTheory.Over.map f).toCatHom
• CategoryTheory.Under.mapFunctor_map 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  (T : Type u₁) [CategoryTheory.Category.{v₁, u₁} T] {X✝ Y✝ : Tᵒᵖ} (f : X✝ ⟶ Y✝) : (CategoryTheory.Under.mapFunctor T).map f = (CategoryTheory.Under.map f.unop).toCatHom
• preordToCat 📋 Mathlib.Order.Category.Preord
  : CategoryTheory.Functor Preord CategoryTheory.Cat
• instFaithfulPreordCatPreordToCat 📋 Mathlib.Order.Category.Preord
  : preordToCat.Faithful
• instFullPreordCatPreordToCat 📋 Mathlib.Order.Category.Preord
  : preordToCat.Full
• preordToCat_obj 📋 Mathlib.Order.Category.Preord
  (X : Preord) : preordToCat.obj X = CategoryTheory.Cat.of ↑X
• preordToCat_map 📋 Mathlib.Order.Category.Preord
  {X✝ Y✝ : Preord} (f : X✝ ⟶ Y✝) : preordToCat.map f = ⋯.functor.toCatHom
• Mathlib.Tactic.CategoryTheory.ToApp.toNatTrans_congr 📋 Mathlib.Tactic.CategoryTheory.ToApp
  {C D : CategoryTheory.Cat} {F G : C ⟶ D} {η θ : F ⟶ G} (h : η = θ) : η.toNatTrans = θ.toNatTrans
• CategoryTheory.OplaxFunctor.map₂_rightUnitor_app 📋 Mathlib.CategoryTheory.Bicategory.Functor.Oplax
  {B : Type u_1} [CategoryTheory.Bicategory B] (self : CategoryTheory.OplaxFunctor B CategoryTheory.Cat) {a b : B} (f : a ⟶ b) (X : ↑(self.obj a)) : (self.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom).toNatTrans.app X = CategoryTheory.CategoryStruct.comp ((self.mapComp f (CategoryTheory.CategoryStruct.id b)).toNatTrans.app X) ((self.mapId b).toNatTrans.app ((self.map f).toFunctor.obj X))
• CategoryTheory.OplaxFunctor.map₂_leftUnitor_app 📋 Mathlib.CategoryTheory.Bicategory.Functor.Oplax
  {B : Type u_1} [CategoryTheory.Bicategory B] (self : CategoryTheory.OplaxFunctor B CategoryTheory.Cat) {a b : B} (f : a ⟶ b) (X : ↑(self.obj a)) : (self.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom).toNatTrans.app X = CategoryTheory.CategoryStruct.comp ((self.mapComp (CategoryTheory.CategoryStruct.id a) f).toNatTrans.app X) ((self.map f).toFunctor.map ((self.mapId a).toNatTrans.app X))
• CategoryTheory.OplaxFunctor.map₂_rightUnitor_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Functor.Oplax
  {B : Type u_1} [CategoryTheory.Bicategory B] (self : CategoryTheory.OplaxFunctor B CategoryTheory.Cat) {a b : B} (f : a ⟶ b) (X : ↑(self.obj a)) {Z : ↑(self.obj b)} (h : (self.map f).toFunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((self.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom).toNatTrans.app X) h = CategoryTheory.CategoryStruct.comp ((self.mapComp f (CategoryTheory.CategoryStruct.id b)).toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((self.mapId b).toNatTrans.app ((self.map f).toFunctor.obj X)) h)
• CategoryTheory.OplaxFunctor.map₂_leftUnitor_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Functor.Oplax
  {B : Type u_1} [CategoryTheory.Bicategory B] (self : CategoryTheory.OplaxFunctor B CategoryTheory.Cat) {a b : B} (f : a ⟶ b) (X : ↑(self.obj a)) {Z : ↑(self.obj b)} (h : (self.map f).toFunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((self.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom).toNatTrans.app X) h = CategoryTheory.CategoryStruct.comp ((self.mapComp (CategoryTheory.CategoryStruct.id a) f).toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((self.map f).toFunctor.map ((self.mapId a).toNatTrans.app X)) h)
• CategoryTheory.OplaxFunctor.mapComp_naturality_right_app 📋 Mathlib.CategoryTheory.Bicategory.Functor.Oplax
  {B : Type u_1} [CategoryTheory.Bicategory B] (self : CategoryTheory.OplaxFunctor B CategoryTheory.Cat) {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (X : ↑(self.obj a)) : CategoryTheory.CategoryStruct.comp ((self.map₂ (CategoryTheory.Bicategory.whiskerLeft f η)).toNatTrans.app X) ((self.mapComp f g').toNatTrans.app X) = CategoryTheory.CategoryStruct.comp ((self.mapComp f g).toNatTrans.app X) ((self.map₂ η).toNatTrans.app ((self.map f).toFunctor.obj X))
• CategoryTheory.OplaxFunctor.mapComp_naturality_left_app 📋 Mathlib.CategoryTheory.Bicategory.Functor.Oplax
  {B : Type u_1} [CategoryTheory.Bicategory B] (self : CategoryTheory.OplaxFunctor B CategoryTheory.Cat) {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (X : ↑(self.obj a)) : CategoryTheory.CategoryStruct.comp ((self.map₂ (CategoryTheory.Bicategory.whiskerRight η g)).toNatTrans.app X) ((self.mapComp f' g).toNatTrans.app X) = CategoryTheory.CategoryStruct.comp ((self.mapComp f g).toNatTrans.app X) ((self.map g).toFunctor.map ((self.map₂ η).toNatTrans.app X))
• CategoryTheory.OplaxFunctor.mapComp_naturality_right_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Functor.Oplax
  {B : Type u_1} [CategoryTheory.Bicategory B] (self : CategoryTheory.OplaxFunctor B CategoryTheory.Cat) {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (X : ↑(self.obj a)) {Z : ↑(self.obj c)} (h : (self.map g').toFunctor.obj ((self.map f).toFunctor.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((self.map₂ (CategoryTheory.Bicategory.whiskerLeft f η)).toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((self.mapComp f g').toNatTrans.app X) h) = CategoryTheory.CategoryStruct.comp ((self.mapComp f g).toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((self.map₂ η).toNatTrans.app ((self.map f).toFunctor.obj X)) h)
• CategoryTheory.OplaxFunctor.mapComp_naturality_left_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Functor.Oplax
  {B : Type u_1} [CategoryTheory.Bicategory B] (self : CategoryTheory.OplaxFunctor B CategoryTheory.Cat) {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (X : ↑(self.obj a)) {Z : ↑(self.obj c)} (h : (self.map g).toFunctor.obj ((self.map f').toFunctor.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((self.map₂ (CategoryTheory.Bicategory.whiskerRight η g)).toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((self.mapComp f' g).toNatTrans.app X) h) = CategoryTheory.CategoryStruct.comp ((self.mapComp f g).toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((self.map g).toFunctor.map ((self.map₂ η).toNatTrans.app X)) h)
• CategoryTheory.OplaxFunctor.mapComp_assoc_left_app 📋 Mathlib.CategoryTheory.Bicategory.Functor.Oplax
  {B : Type u_1} [CategoryTheory.Bicategory B] (F : CategoryTheory.OplaxFunctor B CategoryTheory.Cat) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(F.obj a)) : CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).toNatTrans.app X) ((F.map h).toFunctor.map ((F.mapComp f g).toNatTrans.app X)) = CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.associator f g h).hom).toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).toNatTrans.app X) ((F.mapComp g h).toNatTrans.app ((F.map f).toFunctor.obj X)))
• CategoryTheory.OplaxFunctor.mapComp_assoc_right_app 📋 Mathlib.CategoryTheory.Bicategory.Functor.Oplax
  {B : Type u_1} [CategoryTheory.Bicategory B] (F : CategoryTheory.OplaxFunctor B CategoryTheory.Cat) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(F.obj a)) : CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).toNatTrans.app X) ((F.mapComp g h).toNatTrans.app ((F.map f).toFunctor.obj X)) = CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.associator f g h).inv).toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).toNatTrans.app X) ((F.map h).toFunctor.map ((F.mapComp f g).toNatTrans.app X)))
• CategoryTheory.OplaxFunctor.map₂_associator_app 📋 Mathlib.CategoryTheory.Bicategory.Functor.Oplax
  {B : Type u_1} [CategoryTheory.Bicategory B] (self : CategoryTheory.OplaxFunctor B CategoryTheory.Cat) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(self.obj a)) : CategoryTheory.CategoryStruct.comp ((self.map₂ (CategoryTheory.Bicategory.associator f g h).hom).toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((self.mapComp f (CategoryTheory.CategoryStruct.comp g h)).toNatTrans.app X) ((self.mapComp g h).toNatTrans.app ((self.map f).toFunctor.obj X))) = CategoryTheory.CategoryStruct.comp ((self.mapComp (CategoryTheory.CategoryStruct.comp f g) h).toNatTrans.app X) ((self.map h).toFunctor.map ((self.mapComp f g).toNatTrans.app X))
• CategoryTheory.OplaxFunctor.mapComp_assoc_left_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Functor.Oplax
  {B : Type u_1} [CategoryTheory.Bicategory B] (F : CategoryTheory.OplaxFunctor B CategoryTheory.Cat) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(F.obj a)) {Z : ↑(F.obj d)} (h✝ : (F.map h).toFunctor.obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj X)) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((F.map h).toFunctor.map ((F.mapComp f g).toNatTrans.app X)) h✝) = CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.associator f g h).hom).toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((F.mapComp g h).toNatTrans.app ((F.map f).toFunctor.obj X)) h✝))
• CategoryTheory.OplaxFunctor.mapComp_assoc_right_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Functor.Oplax
  {B : Type u_1} [CategoryTheory.Bicategory B] (F : CategoryTheory.OplaxFunctor B CategoryTheory.Cat) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(F.obj a)) {Z : ↑(F.obj d)} (h✝ : (F.map h).toFunctor.obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj X)) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((F.mapComp g h).toNatTrans.app ((F.map f).toFunctor.obj X)) h✝) = CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.associator f g h).inv).toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((F.map h).toFunctor.map ((F.mapComp f g).toNatTrans.app X)) h✝))
• CategoryTheory.OplaxFunctor.map₂_associator_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Functor.Oplax
  {B : Type u_1} [CategoryTheory.Bicategory B] (self : CategoryTheory.OplaxFunctor B CategoryTheory.Cat) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(self.obj a)) {Z : ↑(self.obj d)} (h✝ : (self.map h).toFunctor.obj ((self.map g).toFunctor.obj ((self.map f).toFunctor.obj X)) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((self.map₂ (CategoryTheory.Bicategory.associator f g h).hom).toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((self.mapComp f (CategoryTheory.CategoryStruct.comp g h)).toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((self.mapComp g h).toNatTrans.app ((self.map f).toFunctor.obj X)) h✝)) = CategoryTheory.CategoryStruct.comp ((self.mapComp (CategoryTheory.CategoryStruct.comp f g) h).toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((self.map h).toFunctor.map ((self.mapComp f g).toNatTrans.app X)) h✝)
• CategoryTheory.LaxFunctor.map₂_rightUnitor_app 📋 Mathlib.CategoryTheory.Bicategory.Functor.Lax
  {B : Type u_1} [CategoryTheory.Bicategory B] (self : CategoryTheory.LaxFunctor B CategoryTheory.Cat) {a b : B} (f : a ⟶ b) (X : ↑(self.obj a)) : (self.map₂ (CategoryTheory.Bicategory.rightUnitor f).inv).toNatTrans.app X = CategoryTheory.CategoryStruct.comp ((self.mapId b).toNatTrans.app ((self.map f).toFunctor.obj X)) ((self.mapComp f (CategoryTheory.CategoryStruct.id b)).toNatTrans.app X)
• CategoryTheory.LaxFunctor.map₂_leftUnitor_app 📋 Mathlib.CategoryTheory.Bicategory.Functor.Lax
  {B : Type u_1} [CategoryTheory.Bicategory B] (self : CategoryTheory.LaxFunctor B CategoryTheory.Cat) {a b : B} (f : a ⟶ b) (X : ↑(self.obj a)) : (self.map₂ (CategoryTheory.Bicategory.leftUnitor f).inv).toNatTrans.app X = CategoryTheory.CategoryStruct.comp ((self.map f).toFunctor.map ((self.mapId a).toNatTrans.app X)) ((self.mapComp (CategoryTheory.CategoryStruct.id a) f).toNatTrans.app X)
• CategoryTheory.LaxFunctor.map₂_rightUnitor_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Functor.Lax
  {B : Type u_1} [CategoryTheory.Bicategory B] (self : CategoryTheory.LaxFunctor B CategoryTheory.Cat) {a b : B} (f : a ⟶ b) (X : ↑(self.obj a)) {Z : ↑(self.obj b)} (h : (self.map (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id b))).toFunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((self.map₂ (CategoryTheory.Bicategory.rightUnitor f).inv).toNatTrans.app X) h = CategoryTheory.CategoryStruct.comp ((self.mapId b).toNatTrans.app ((self.map f).toFunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((self.mapComp f (CategoryTheory.CategoryStruct.id b)).toNatTrans.app X) h)
• CategoryTheory.LaxFunctor.map₂_leftUnitor_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Functor.Lax
  {B : Type u_1} [CategoryTheory.Bicategory B] (self : CategoryTheory.LaxFunctor B CategoryTheory.Cat) {a b : B} (f : a ⟶ b) (X : ↑(self.obj a)) {Z : ↑(self.obj b)} (h : (self.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) f)).toFunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((self.map₂ (CategoryTheory.Bicategory.leftUnitor f).inv).toNatTrans.app X) h = CategoryTheory.CategoryStruct.comp ((self.map f).toFunctor.map ((self.mapId a).toNatTrans.app X)) (CategoryTheory.CategoryStruct.comp ((self.mapComp (CategoryTheory.CategoryStruct.id a) f).toNatTrans.app X) h)
• CategoryTheory.LaxFunctor.map₂_rightUnitor_hom_app 📋 Mathlib.CategoryTheory.Bicategory.Functor.Lax
  {B : Type u_1} [CategoryTheory.Bicategory B] (F : CategoryTheory.LaxFunctor B CategoryTheory.Cat) {a b : B} (f : a ⟶ b) (X : ↑(F.obj a)) : CategoryTheory.CategoryStruct.id ((CategoryTheory.CategoryStruct.id (F.obj b)).toFunctor.obj ((F.map f).toFunctor.obj X)) = CategoryTheory.CategoryStruct.comp ((F.mapId b).toNatTrans.app ((F.map f).toFunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.id b)).toNatTrans.app X) ((F.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom).toNatTrans.app X))
• CategoryTheory.LaxFunctor.map₂_rightUnitor_hom_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Functor.Lax
  {B : Type u_1} [CategoryTheory.Bicategory B] (F : CategoryTheory.LaxFunctor B CategoryTheory.Cat) {a b : B} (f : a ⟶ b) (X : ↑(F.obj a)) {Z : ↑(F.obj b)} (h : (CategoryTheory.CategoryStruct.id (F.obj b)).toFunctor.obj ((F.map f).toFunctor.obj X) ⟶ Z) : h = CategoryTheory.CategoryStruct.comp ((F.mapId b).toNatTrans.app ((F.map f).toFunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.id b)).toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom).toNatTrans.app X) h))
• CategoryTheory.LaxFunctor.mapComp_naturality_right_app 📋 Mathlib.CategoryTheory.Bicategory.Functor.Lax
  {B : Type u_1} [CategoryTheory.Bicategory B] (self : CategoryTheory.LaxFunctor B CategoryTheory.Cat) {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (X : ↑(self.obj a)) : CategoryTheory.CategoryStruct.comp ((self.mapComp f g).toNatTrans.app X) ((self.map₂ (CategoryTheory.Bicategory.whiskerLeft f η)).toNatTrans.app X) = CategoryTheory.CategoryStruct.comp ((self.map₂ η).toNatTrans.app ((self.map f).toFunctor.obj X)) ((self.mapComp f g').toNatTrans.app X)
• CategoryTheory.LaxFunctor.map₂_leftUnitor_hom_app 📋 Mathlib.CategoryTheory.Bicategory.Functor.Lax
  {B : Type u_1} [CategoryTheory.Bicategory B] (F : CategoryTheory.LaxFunctor B CategoryTheory.Cat) {a b : B} (f : a ⟶ b) (X : ↑(F.obj a)) : CategoryTheory.CategoryStruct.id ((F.map f).toFunctor.obj ((CategoryTheory.CategoryStruct.id (F.obj a)).toFunctor.obj X)) = CategoryTheory.CategoryStruct.comp ((F.map f).toFunctor.map ((F.mapId a).toNatTrans.app X)) (CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.id a) f).toNatTrans.app X) ((F.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom).toNatTrans.app X))
• CategoryTheory.LaxFunctor.map₂_leftUnitor_hom_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Functor.Lax
  {B : Type u_1} [CategoryTheory.Bicategory B] (F : CategoryTheory.LaxFunctor B CategoryTheory.Cat) {a b : B} (f : a ⟶ b) (X : ↑(F.obj a)) {Z : ↑(F.obj b)} (h : (F.map f).toFunctor.obj ((CategoryTheory.CategoryStruct.id (F.obj a)).toFunctor.obj X) ⟶ Z) : h = CategoryTheory.CategoryStruct.comp ((F.map f).toFunctor.map ((F.mapId a).toNatTrans.app X)) (CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.id a) f).toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom).toNatTrans.app X) h))
• CategoryTheory.LaxFunctor.mapComp_naturality_left_app 📋 Mathlib.CategoryTheory.Bicategory.Functor.Lax
  {B : Type u_1} [CategoryTheory.Bicategory B] (self : CategoryTheory.LaxFunctor B CategoryTheory.Cat) {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (X : ↑(self.obj a)) : CategoryTheory.CategoryStruct.comp ((self.mapComp f g).toNatTrans.app X) ((self.map₂ (CategoryTheory.Bicategory.whiskerRight η g)).toNatTrans.app X) = CategoryTheory.CategoryStruct.comp ((self.map g).toFunctor.map ((self.map₂ η).toNatTrans.app X)) ((self.mapComp f' g).toNatTrans.app X)
• CategoryTheory.LaxFunctor.mapComp_naturality_right_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Functor.Lax
  {B : Type u_1} [CategoryTheory.Bicategory B] (self : CategoryTheory.LaxFunctor B CategoryTheory.Cat) {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (X : ↑(self.obj a)) {Z : ↑(self.obj c)} (h : (self.map (CategoryTheory.CategoryStruct.comp f g')).toFunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((self.mapComp f g).toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((self.map₂ (CategoryTheory.Bicategory.whiskerLeft f η)).toNatTrans.app X) h) = CategoryTheory.CategoryStruct.comp ((self.map₂ η).toNatTrans.app ((self.map f).toFunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((self.mapComp f g').toNatTrans.app X) h)
• CategoryTheory.LaxFunctor.mapComp_naturality_left_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Functor.Lax
  {B : Type u_1} [CategoryTheory.Bicategory B] (self : CategoryTheory.LaxFunctor B CategoryTheory.Cat) {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (X : ↑(self.obj a)) {Z : ↑(self.obj c)} (h : (self.map (CategoryTheory.CategoryStruct.comp f' g)).toFunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((self.mapComp f g).toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((self.map₂ (CategoryTheory.Bicategory.whiskerRight η g)).toNatTrans.app X) h) = CategoryTheory.CategoryStruct.comp ((self.map g).toFunctor.map ((self.map₂ η).toNatTrans.app X)) (CategoryTheory.CategoryStruct.comp ((self.mapComp f' g).toNatTrans.app X) h)
• CategoryTheory.LaxFunctor.mapComp_assoc_left_app 📋 Mathlib.CategoryTheory.Bicategory.Functor.Lax
  {B : Type u_1} [CategoryTheory.Bicategory B] (F : CategoryTheory.LaxFunctor B CategoryTheory.Cat) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(F.obj a)) : CategoryTheory.CategoryStruct.comp ((F.map h).toFunctor.map ((F.mapComp f g).toNatTrans.app X)) ((F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).toNatTrans.app X) = CategoryTheory.CategoryStruct.comp ((F.mapComp g h).toNatTrans.app ((F.map f).toFunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).toNatTrans.app X) ((F.map₂ (CategoryTheory.Bicategory.associator f g h).inv).toNatTrans.app X))
• CategoryTheory.LaxFunctor.mapComp_assoc_right_app 📋 Mathlib.CategoryTheory.Bicategory.Functor.Lax
  {B : Type u_1} [CategoryTheory.Bicategory B] (F : CategoryTheory.LaxFunctor B CategoryTheory.Cat) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(F.obj a)) : CategoryTheory.CategoryStruct.comp ((F.mapComp g h).toNatTrans.app ((F.map f).toFunctor.obj X)) ((F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).toNatTrans.app X) = CategoryTheory.CategoryStruct.comp ((F.map h).toFunctor.map ((F.mapComp f g).toNatTrans.app X)) (CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).toNatTrans.app X) ((F.map₂ (CategoryTheory.Bicategory.associator f g h).hom).toNatTrans.app X))
• CategoryTheory.LaxFunctor.map₂_associator_app 📋 Mathlib.CategoryTheory.Bicategory.Functor.Lax
  {B : Type u_1} [CategoryTheory.Bicategory B] (self : CategoryTheory.LaxFunctor B CategoryTheory.Cat) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(self.obj a)) : CategoryTheory.CategoryStruct.comp ((self.map h).toFunctor.map ((self.mapComp f g).toNatTrans.app X)) (CategoryTheory.CategoryStruct.comp ((self.mapComp (CategoryTheory.CategoryStruct.comp f g) h).toNatTrans.app X) ((self.map₂ (CategoryTheory.Bicategory.associator f g h).hom).toNatTrans.app X)) = CategoryTheory.CategoryStruct.comp ((self.mapComp g h).toNatTrans.app ((self.map f).toFunctor.obj X)) ((self.mapComp f (CategoryTheory.CategoryStruct.comp g h)).toNatTrans.app X)
• CategoryTheory.LaxFunctor.mapComp_assoc_left_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Functor.Lax
  {B : Type u_1} [CategoryTheory.Bicategory B] (F : CategoryTheory.LaxFunctor B CategoryTheory.Cat) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(F.obj a)) {Z : ↑(F.obj d)} (h✝ : (F.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h)).toFunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.map h).toFunctor.map ((F.mapComp f g).toNatTrans.app X)) (CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).toNatTrans.app X) h✝) = CategoryTheory.CategoryStruct.comp ((F.mapComp g h).toNatTrans.app ((F.map f).toFunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.associator f g h).inv).toNatTrans.app X) h✝))
• CategoryTheory.LaxFunctor.mapComp_assoc_right_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Functor.Lax
  {B : Type u_1} [CategoryTheory.Bicategory B] (F : CategoryTheory.LaxFunctor B CategoryTheory.Cat) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(F.obj a)) {Z : ↑(F.obj d)} (h✝ : (F.map (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h))).toFunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.mapComp g h).toNatTrans.app ((F.map f).toFunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).toNatTrans.app X) h✝) = CategoryTheory.CategoryStruct.comp ((F.map h).toFunctor.map ((F.mapComp f g).toNatTrans.app X)) (CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.associator f g h).hom).toNatTrans.app X) h✝))
• CategoryTheory.LaxFunctor.map₂_associator_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Functor.Lax
  {B : Type u_1} [CategoryTheory.Bicategory B] (self : CategoryTheory.LaxFunctor B CategoryTheory.Cat) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(self.obj a)) {Z : ↑(self.obj d)} (h✝ : (self.map (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h))).toFunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((self.map h).toFunctor.map ((self.mapComp f g).toNatTrans.app X)) (CategoryTheory.CategoryStruct.comp ((self.mapComp (CategoryTheory.CategoryStruct.comp f g) h).toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((self.map₂ (CategoryTheory.Bicategory.associator f g h).hom).toNatTrans.app X) h✝)) = CategoryTheory.CategoryStruct.comp ((self.mapComp g h).toNatTrans.app ((self.map f).toFunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((self.mapComp f (CategoryTheory.CategoryStruct.comp g h)).toNatTrans.app X) h✝)
• CategoryTheory.Pseudofunctor.map₂_right_unitor_app 📋 Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] (self : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b : B} (f : a ⟶ b) (X : ↑(self.obj a)) : (self.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom).toNatTrans.app X = CategoryTheory.CategoryStruct.comp ((self.mapComp f (CategoryTheory.CategoryStruct.id b)).hom.toNatTrans.app X) ((self.mapId b).hom.toNatTrans.app ((self.map f).toFunctor.obj X))
• CategoryTheory.Pseudofunctor.mapComp_id_right_hom_app 📋 Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b : B} (f : a ⟶ b) (X : ↑(F.obj a)) : (F.mapComp f (CategoryTheory.CategoryStruct.id b)).hom.toNatTrans.app X = CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom).toNatTrans.app X) ((F.mapId b).inv.toNatTrans.app ((F.map f).toFunctor.obj X))
• CategoryTheory.Pseudofunctor.whiskerLeft_mapId_inv_app 📋 Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b : B} (f : a ⟶ b) (X : ↑(F.obj a)) : (F.mapId b).inv.toNatTrans.app ((F.map f).toFunctor.obj X) = CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.rightUnitor f).inv).toNatTrans.app X) ((F.mapComp f (CategoryTheory.CategoryStruct.id b)).hom.toNatTrans.app X)
• CategoryTheory.Pseudofunctor.mapComp_id_right_inv_app 📋 Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b : B} (f : a ⟶ b) (X : ↑(F.obj a)) : (F.mapComp f (CategoryTheory.CategoryStruct.id b)).inv.toNatTrans.app X = CategoryTheory.CategoryStruct.comp ((F.mapId b).hom.toNatTrans.app ((F.map f).toFunctor.obj X)) ((F.map₂ (CategoryTheory.Bicategory.rightUnitor f).inv).toNatTrans.app X)
• CategoryTheory.Pseudofunctor.map₂_left_unitor_app 📋 Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] (self : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b : B} (f : a ⟶ b) (X : ↑(self.obj a)) : (self.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom).toNatTrans.app X = CategoryTheory.CategoryStruct.comp ((self.mapComp (CategoryTheory.CategoryStruct.id a) f).hom.toNatTrans.app X) ((self.map f).toFunctor.map ((self.mapId a).hom.toNatTrans.app X))
• CategoryTheory.Pseudofunctor.whiskerLeft_mapId_hom_app 📋 Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b : B} (f : a ⟶ b) (X : ↑(F.obj a)) : (F.mapId b).hom.toNatTrans.app ((F.map f).toFunctor.obj X) = CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.id b)).inv.toNatTrans.app X) ((F.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom).toNatTrans.app X)
• CategoryTheory.Pseudofunctor.mapComp_id_left_hom_app 📋 Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b : B} (f : a ⟶ b) (X : ↑(F.obj a)) : (F.mapComp (CategoryTheory.CategoryStruct.id a) f).hom.toNatTrans.app X = CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom).toNatTrans.app X) ((F.map f).toFunctor.map ((F.mapId a).inv.toNatTrans.app X))
• CategoryTheory.Pseudofunctor.whiskerRight_mapId_inv_app 📋 Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b : B} (f : a ⟶ b) (X : ↑(F.obj a)) : (F.map f).toFunctor.map ((F.mapId a).inv.toNatTrans.app X) = CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.leftUnitor f).inv).toNatTrans.app X) ((F.mapComp (CategoryTheory.CategoryStruct.id a) f).hom.toNatTrans.app X)
• CategoryTheory.Pseudofunctor.mapComp_id_left_inv_app 📋 Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b : B} (f : a ⟶ b) (X : ↑(F.obj a)) : (F.mapComp (CategoryTheory.CategoryStruct.id a) f).inv.toNatTrans.app X = CategoryTheory.CategoryStruct.comp ((F.map f).toFunctor.map ((F.mapId a).hom.toNatTrans.app X)) ((F.map₂ (CategoryTheory.Bicategory.leftUnitor f).inv).toNatTrans.app X)
• CategoryTheory.Pseudofunctor.whiskerRight_mapId_hom_app 📋 Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b : B} (f : a ⟶ b) (X : ↑(F.obj a)) : (F.map f).toFunctor.map ((F.mapId a).hom.toNatTrans.app X) = CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.id a) f).inv.toNatTrans.app X) ((F.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom).toNatTrans.app X)
• CategoryTheory.Pseudofunctor.map₂_right_unitor_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] (self : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b : B} (f : a ⟶ b) (X : ↑(self.obj a)) {Z : ↑(self.obj b)} (h : (self.map f).toFunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((self.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom).toNatTrans.app X) h = CategoryTheory.CategoryStruct.comp ((self.mapComp f (CategoryTheory.CategoryStruct.id b)).hom.toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((self.mapId b).hom.toNatTrans.app ((self.map f).toFunctor.obj X)) h)
• CategoryTheory.Pseudofunctor.mapComp_id_right_hom_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b : B} (f : a ⟶ b) (X : ↑(F.obj a)) {Z : ↑(F.obj b)} (h : (F.map (CategoryTheory.CategoryStruct.id b)).toFunctor.obj ((F.map f).toFunctor.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.id b)).hom.toNatTrans.app X) h = CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom).toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((F.mapId b).inv.toNatTrans.app ((F.map f).toFunctor.obj X)) h)
• CategoryTheory.Pseudofunctor.map₂_left_unitor_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] (self : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b : B} (f : a ⟶ b) (X : ↑(self.obj a)) {Z : ↑(self.obj b)} (h : (self.map f).toFunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((self.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom).toNatTrans.app X) h = CategoryTheory.CategoryStruct.comp ((self.mapComp (CategoryTheory.CategoryStruct.id a) f).hom.toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((self.map f).toFunctor.map ((self.mapId a).hom.toNatTrans.app X)) h)
• CategoryTheory.Pseudofunctor.mapComp_id_right_inv_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b : B} (f : a ⟶ b) (X : ↑(F.obj a)) {Z : ↑(F.obj b)} (h : (F.map (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id b))).toFunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.id b)).inv.toNatTrans.app X) h = CategoryTheory.CategoryStruct.comp ((F.mapId b).hom.toNatTrans.app ((F.map f).toFunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.rightUnitor f).inv).toNatTrans.app X) h)
• CategoryTheory.Pseudofunctor.mapComp_id_left_hom_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b : B} (f : a ⟶ b) (X : ↑(F.obj a)) {Z : ↑(F.obj b)} (h : (F.map f).toFunctor.obj ((F.map (CategoryTheory.CategoryStruct.id a)).toFunctor.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.id a) f).hom.toNatTrans.app X) h = CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom).toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((F.map f).toFunctor.map ((F.mapId a).inv.toNatTrans.app X)) h)
• CategoryTheory.Pseudofunctor.whiskerLeft_mapId_hom_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b : B} (f : a ⟶ b) (X : ↑(F.obj a)) {Z : ↑(F.obj b)} (h : (CategoryTheory.CategoryStruct.id (F.obj b)).toFunctor.obj ((F.map f).toFunctor.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.mapId b).hom.toNatTrans.app ((F.map f).toFunctor.obj X)) h = CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.id b)).inv.toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom).toNatTrans.app X) h)
• CategoryTheory.Pseudofunctor.whiskerLeft_mapId_inv_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b : B} (f : a ⟶ b) (X : ↑(F.obj a)) {Z : ↑(F.obj b)} (h : (F.map (CategoryTheory.CategoryStruct.id b)).toFunctor.obj ((F.map f).toFunctor.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.mapId b).inv.toNatTrans.app ((F.map f).toFunctor.obj X)) h = CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.rightUnitor f).inv).toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.id b)).hom.toNatTrans.app X) h)
• CategoryTheory.Pseudofunctor.map₂_whisker_left_app 📋 Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] (self : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h) (X : ↑(self.obj a)) : (self.map₂ (CategoryTheory.Bicategory.whiskerLeft f η)).toNatTrans.app X = CategoryTheory.CategoryStruct.comp ((self.mapComp f g).hom.toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((self.map₂ η).toNatTrans.app ((self.map f).toFunctor.obj X)) ((self.mapComp f h).inv.toNatTrans.app X))
• CategoryTheory.Pseudofunctor.mapComp_id_left_inv_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b : B} (f : a ⟶ b) (X : ↑(F.obj a)) {Z : ↑(F.obj b)} (h : (F.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) f)).toFunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.id a) f).inv.toNatTrans.app X) h = CategoryTheory.CategoryStruct.comp ((F.map f).toFunctor.map ((F.mapId a).hom.toNatTrans.app X)) (CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.leftUnitor f).inv).toNatTrans.app X) h)
• CategoryTheory.Pseudofunctor.whiskerRight_mapId_hom_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b : B} (f : a ⟶ b) (X : ↑(F.obj a)) {Z : ↑(F.obj b)} (h : (F.map f).toFunctor.obj ((CategoryTheory.CategoryStruct.id (F.obj a)).toFunctor.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.map f).toFunctor.map ((F.mapId a).hom.toNatTrans.app X)) h = CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.id a) f).inv.toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom).toNatTrans.app X) h)
• CategoryTheory.Pseudofunctor.whiskerRight_mapId_inv_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b : B} (f : a ⟶ b) (X : ↑(F.obj a)) {Z : ↑(F.obj b)} (h : (F.map f).toFunctor.obj ((F.map (CategoryTheory.CategoryStruct.id a)).toFunctor.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.map f).toFunctor.map ((F.mapId a).inv.toNatTrans.app X)) h = CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.leftUnitor f).inv).toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.id a) f).hom.toNatTrans.app X) h)
• CategoryTheory.Pseudofunctor.map₂_whisker_right_app 📋 Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] (self : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b c : B} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c) (X : ↑(self.obj a)) : (self.map₂ (CategoryTheory.Bicategory.whiskerRight η h)).toNatTrans.app X = CategoryTheory.CategoryStruct.comp ((self.mapComp f h).hom.toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((self.map h).toFunctor.map ((self.map₂ η).toNatTrans.app X)) ((self.mapComp g h).inv.toNatTrans.app X))
• CategoryTheory.Pseudofunctor.map₂_whisker_left_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] (self : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h) (X : ↑(self.obj a)) {Z : ↑(self.obj c)} (h✝ : (self.map (CategoryTheory.CategoryStruct.comp f h)).toFunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((self.map₂ (CategoryTheory.Bicategory.whiskerLeft f η)).toNatTrans.app X) h✝ = CategoryTheory.CategoryStruct.comp ((self.mapComp f g).hom.toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((self.map₂ η).toNatTrans.app ((self.map f).toFunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((self.mapComp f h).inv.toNatTrans.app X) h✝))
• CategoryTheory.Pseudofunctor.map₂_whisker_right_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] (self : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b c : B} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c) (X : ↑(self.obj a)) {Z : ↑(self.obj c)} (h✝ : (self.map (CategoryTheory.CategoryStruct.comp g h)).toFunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((self.map₂ (CategoryTheory.Bicategory.whiskerRight η h)).toNatTrans.app X) h✝ = CategoryTheory.CategoryStruct.comp ((self.mapComp f h).hom.toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((self.map h).toFunctor.map ((self.map₂ η).toNatTrans.app X)) (CategoryTheory.CategoryStruct.comp ((self.mapComp g h).inv.toNatTrans.app X) h✝))
• CategoryTheory.Pseudofunctor.map₂_associator_app 📋 Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] (self : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(self.obj a)) : (self.map₂ (CategoryTheory.Bicategory.associator f g h).hom).toNatTrans.app X = CategoryTheory.CategoryStruct.comp ((self.mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom.toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((self.map h).toFunctor.map ((self.mapComp f g).hom.toNatTrans.app X)) (CategoryTheory.CategoryStruct.comp ((self.mapComp g h).inv.toNatTrans.app ((self.map f).toFunctor.obj X)) ((self.mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv.toNatTrans.app X)))
• CategoryTheory.Pseudofunctor.mapComp_assoc_left_inv_app 📋 Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(F.obj a)) : CategoryTheory.CategoryStruct.comp ((F.map h).toFunctor.map ((F.mapComp f g).inv.toNatTrans.app X)) ((F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).inv.toNatTrans.app X) = CategoryTheory.CategoryStruct.comp ((F.mapComp g h).inv.toNatTrans.app ((F.map f).toFunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv.toNatTrans.app X) ((F.map₂ (CategoryTheory.Bicategory.associator f g h).inv).toNatTrans.app X))
• CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv_app 📋 Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(F.obj a)) : CategoryTheory.CategoryStruct.comp ((F.mapComp g h).inv.toNatTrans.app ((F.map f).toFunctor.obj X)) ((F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv.toNatTrans.app X) = CategoryTheory.CategoryStruct.comp ((F.map h).toFunctor.map ((F.mapComp f g).inv.toNatTrans.app X)) (CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).inv.toNatTrans.app X) ((F.map₂ (CategoryTheory.Bicategory.associator f g h).hom).toNatTrans.app X))
• CategoryTheory.Pseudofunctor.mapComp_assoc_left_hom_app 📋 Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(F.obj a)) : CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom.toNatTrans.app X) ((F.map h).toFunctor.map ((F.mapComp f g).hom.toNatTrans.app X)) = CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.associator f g h).hom).toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).hom.toNatTrans.app X) ((F.mapComp g h).hom.toNatTrans.app ((F.map f).toFunctor.obj X)))
• CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom_app 📋 Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(F.obj a)) : CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).hom.toNatTrans.app X) ((F.mapComp g h).hom.toNatTrans.app ((F.map f).toFunctor.obj X)) = CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.associator f g h).inv).toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom.toNatTrans.app X) ((F.map h).toFunctor.map ((F.mapComp f g).hom.toNatTrans.app X)))
• CategoryTheory.Pseudofunctor.map₂_associator_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] (self : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(self.obj a)) {Z : ↑(self.obj d)} (h✝ : (self.map (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h))).toFunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((self.map₂ (CategoryTheory.Bicategory.associator f g h).hom).toNatTrans.app X) h✝ = CategoryTheory.CategoryStruct.comp ((self.mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom.toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((self.map h).toFunctor.map ((self.mapComp f g).hom.toNatTrans.app X)) (CategoryTheory.CategoryStruct.comp ((self.mapComp g h).inv.toNatTrans.app ((self.map f).toFunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((self.mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv.toNatTrans.app X) h✝)))
• CategoryTheory.Pseudofunctor.mapComp_assoc_left_hom_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(F.obj a)) {Z : ↑(F.obj d)} (h✝ : (F.map h).toFunctor.obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj X)) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom.toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((F.map h).toFunctor.map ((F.mapComp f g).hom.toNatTrans.app X)) h✝) = CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.associator f g h).hom).toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).hom.toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((F.mapComp g h).hom.toNatTrans.app ((F.map f).toFunctor.obj X)) h✝))
• CategoryTheory.Pseudofunctor.mapComp_assoc_left_inv_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(F.obj a)) {Z : ↑(F.obj d)} (h✝ : (F.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h)).toFunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.map h).toFunctor.map ((F.mapComp f g).inv.toNatTrans.app X)) (CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).inv.toNatTrans.app X) h✝) = CategoryTheory.CategoryStruct.comp ((F.mapComp g h).inv.toNatTrans.app ((F.map f).toFunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv.toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.associator f g h).inv).toNatTrans.app X) h✝))
• CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(F.obj a)) {Z : ↑(F.obj d)} (h✝ : (F.map h).toFunctor.obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj X)) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).hom.toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((F.mapComp g h).hom.toNatTrans.app ((F.map f).toFunctor.obj X)) h✝) = CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.associator f g h).inv).toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom.toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((F.map h).toFunctor.map ((F.mapComp f g).hom.toNatTrans.app X)) h✝))
• CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv_app_assoc 📋 Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
  {B : Type u_1} [CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(F.obj a)) {Z : ↑(F.obj d)} (h✝ : (F.map (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h))).toFunctor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.mapComp g h).inv.toNatTrans.app ((F.map f).toFunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv.toNatTrans.app X) h✝) = CategoryTheory.CategoryStruct.comp ((F.map h).toFunctor.map ((F.mapComp f g).inv.toNatTrans.app X)) (CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).inv.toNatTrans.app X) (CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.associator f g h).hom).toNatTrans.app X) h✝))
• CategoryTheory.WithInitial.prelaxfunctor 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  : CategoryTheory.PrelaxFunctor CategoryTheory.Cat CategoryTheory.Cat
• CategoryTheory.WithInitial.pseudofunctor 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  : CategoryTheory.Pseudofunctor CategoryTheory.Cat CategoryTheory.Cat
• CategoryTheory.WithTerminal.prelaxfunctor 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  : CategoryTheory.PrelaxFunctor CategoryTheory.Cat CategoryTheory.Cat
• CategoryTheory.WithTerminal.pseudofunctor 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  : CategoryTheory.Pseudofunctor CategoryTheory.Cat CategoryTheory.Cat
• CategoryTheory.WithInitial.pseudofunctor_toPrelaxFunctor 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  : CategoryTheory.WithInitial.pseudofunctor.toPrelaxFunctor = CategoryTheory.WithInitial.prelaxfunctor
• CategoryTheory.WithTerminal.pseudofunctor_toPrelaxFunctor 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  : CategoryTheory.WithTerminal.pseudofunctor.toPrelaxFunctor = CategoryTheory.WithTerminal.prelaxfunctor
• CategoryTheory.WithInitial.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_obj 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  (C : CategoryTheory.Cat) : CategoryTheory.WithInitial.prelaxfunctor.obj C = CategoryTheory.Cat.of (CategoryTheory.WithInitial ↑C)
• CategoryTheory.WithTerminal.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_obj 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  (C : CategoryTheory.Cat) : CategoryTheory.WithTerminal.prelaxfunctor.obj C = CategoryTheory.Cat.of (CategoryTheory.WithTerminal ↑C)
• CategoryTheory.WithInitial.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_map 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {X✝ Y✝ : CategoryTheory.Cat} (F : X✝ ⟶ Y✝) : CategoryTheory.WithInitial.prelaxfunctor.map F = (CategoryTheory.WithInitial.map F.toFunctor).toCatHom
• CategoryTheory.WithTerminal.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_map 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {X✝ Y✝ : CategoryTheory.Cat} (F : X✝ ⟶ Y✝) : CategoryTheory.WithTerminal.prelaxfunctor.map F = (CategoryTheory.WithTerminal.map F.toFunctor).toCatHom
• CategoryTheory.WithInitial.prelaxfunctor_toPrelaxFunctorStruct_map₂ 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {a✝ b✝ : CategoryTheory.Cat} {f✝ g✝ : a✝ ⟶ b✝} (f : f✝ ⟶ g✝) : CategoryTheory.WithInitial.prelaxfunctor.map₂ f = CategoryTheory.NatTrans.toCatHom₂ (CategoryTheory.WithInitial.map₂ f.toNatTrans)
• CategoryTheory.WithTerminal.prelaxfunctor_toPrelaxFunctorStruct_map₂ 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {a✝ b✝ : CategoryTheory.Cat} {f✝ g✝ : a✝ ⟶ b✝} (f : f✝ ⟶ g✝) : CategoryTheory.WithTerminal.prelaxfunctor.map₂ f = CategoryTheory.NatTrans.toCatHom₂ (CategoryTheory.WithTerminal.map₂ f.toNatTrans)
• CategoryTheory.WithInitial.pseudofunctor_mapId 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  (C : CategoryTheory.Cat) : CategoryTheory.WithInitial.pseudofunctor.mapId C = CategoryTheory.Cat.Hom.isoMk (CategoryTheory.WithInitial.mapId ↑C)
• CategoryTheory.WithTerminal.pseudofunctor_mapId 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  (C : CategoryTheory.Cat) : CategoryTheory.WithTerminal.pseudofunctor.mapId C = CategoryTheory.Cat.Hom.isoMk (CategoryTheory.WithTerminal.mapId ↑C)
• CategoryTheory.WithInitial.pseudofunctor_mapComp 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {a✝ b✝ c✝ : CategoryTheory.Cat} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) : CategoryTheory.WithInitial.pseudofunctor.mapComp x✝ x✝¹ = CategoryTheory.Cat.Hom.isoMk (CategoryTheory.WithInitial.mapComp x✝.toFunctor x✝¹.toFunctor)
• CategoryTheory.WithTerminal.pseudofunctor_mapComp 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {a✝ b✝ c✝ : CategoryTheory.Cat} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) : CategoryTheory.WithTerminal.pseudofunctor.mapComp x✝ x✝¹ = CategoryTheory.Cat.Hom.isoMk (CategoryTheory.WithTerminal.mapComp x✝.toFunctor x✝¹.toFunctor)
• CategoryTheory.Cat.asSmallFunctor 📋 Mathlib.CategoryTheory.Category.Cat.AsSmall
  : CategoryTheory.Functor CategoryTheory.Cat CategoryTheory.Cat
• CategoryTheory.Cat.asSmallFunctor_obj 📋 Mathlib.CategoryTheory.Category.Cat.AsSmall
  (C : CategoryTheory.Cat) : CategoryTheory.Cat.asSmallFunctor.obj C = CategoryTheory.Cat.of (CategoryTheory.AsSmall ↑C)
• CategoryTheory.Cat.asSmallFunctor_map 📋 Mathlib.CategoryTheory.Category.Cat.AsSmall
  {X✝ Y✝ : CategoryTheory.Cat} (F : X✝ ⟶ Y✝) : CategoryTheory.Cat.asSmallFunctor.map F = (CategoryTheory.AsSmall.down.comp (F.toFunctor.comp CategoryTheory.AsSmall.up)).toCatHom
• CategoryTheory.Functor.elementsFunctor 📋 Mathlib.CategoryTheory.Elements
  {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor (CategoryTheory.Functor C (Type w)) CategoryTheory.Cat
• CategoryTheory.Functor.elementsFunctor_obj 📋 Mathlib.CategoryTheory.Elements
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) : CategoryTheory.Functor.elementsFunctor.obj F = CategoryTheory.Cat.of F.Elements
• CategoryTheory.Functor.elementsFunctor_map 📋 Mathlib.CategoryTheory.Elements
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : CategoryTheory.Functor C (Type w)} (n : X✝ ⟶ Y✝) : CategoryTheory.Functor.elementsFunctor.map n = (CategoryTheory.NatTrans.mapElements n).toCatHom
• CategoryTheory.Grothendieck 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat) : Type (max u u₂)
• CategoryTheory.Grothendieck.base 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (self : CategoryTheory.Grothendieck F) : C
• CategoryTheory.Grothendieck.instCategory 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} : CategoryTheory.Category.{max v₂ v, max u₂ u} (CategoryTheory.Grothendieck F)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c