Loogle!

Result

Found 4891 declarations mentioning CategoryTheory.CategoryStruct.id. Of these, only the first 200 are shown.

• CategoryTheory.CategoryStruct.id 📋 Mathlib.CategoryTheory.Category.Basic
  {obj : Type u} [self : CategoryTheory.CategoryStruct.{v, u} obj] (X : obj) : X ⟶ X
• CategoryTheory.instEpiId 📋 Mathlib.CategoryTheory.Category.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) : CategoryTheory.Epi (CategoryTheory.CategoryStruct.id X)
• CategoryTheory.instMonoId 📋 Mathlib.CategoryTheory.Category.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) : CategoryTheory.Mono (CategoryTheory.CategoryStruct.id X)
• CategoryTheory.Category.comp_id 📋 Mathlib.CategoryTheory.Category.Basic
  {obj : Type u} [self : CategoryTheory.Category.{v, u} obj] {X Y : obj} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id Y) = f
• CategoryTheory.Category.id_comp 📋 Mathlib.CategoryTheory.Category.Basic
  {obj : Type u} [self : CategoryTheory.Category.{v, u} obj] {X Y : obj} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X) f = f
• CategoryTheory.id_of_comp_left_id 📋 Mathlib.CategoryTheory.Category.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (f : X ⟶ X) (w : ∀ {Y : C} (g : X ⟶ Y), CategoryTheory.CategoryStruct.comp f g = g) : f = CategoryTheory.CategoryStruct.id X
• CategoryTheory.id_of_comp_right_id 📋 Mathlib.CategoryTheory.Category.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (f : X ⟶ X) (w : ∀ {Y : C} (g : Y ⟶ X), CategoryTheory.CategoryStruct.comp g f = g) : f = CategoryTheory.CategoryStruct.id X
• CategoryTheory.cancel_epi_id 📋 Mathlib.CategoryTheory.Category.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f] {h : Y ⟶ Y} : CategoryTheory.CategoryStruct.comp f h = f ↔ h = CategoryTheory.CategoryStruct.id Y
• CategoryTheory.cancel_mono_id 📋 Mathlib.CategoryTheory.Category.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : Y ⟶ X) [CategoryTheory.Mono f] {h : Y ⟶ Y} : CategoryTheory.CategoryStruct.comp h f = f ↔ h = CategoryTheory.CategoryStruct.id Y
• CategoryTheory.Category.mk' 📋 Mathlib.CategoryTheory.Category.Basic
  {obj : Type u} [CategoryTheory.CategoryStruct.{v, u} obj] (id_comp : ∀ {X Y : obj} (f : Y ⟶ X), CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id X) = f) (comp_id : ∀ {X Y : obj} (f : Y ⟶ X), CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id Y) f = f) (assoc : ∀ {W X Y Z : obj} (f : X ⟶ W) (g : Y ⟶ X) (h : Z ⟶ Y), CategoryTheory.CategoryStruct.comp h (CategoryTheory.CategoryStruct.comp g f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp h g) f) : CategoryTheory.Category.{v, u} obj
• CategoryTheory.Category.mk 📋 Mathlib.CategoryTheory.Category.Basic
  {obj : Type u} [toCategoryStruct : CategoryTheory.CategoryStruct.{v, u} obj] (id_comp : ∀ {X Y : obj} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X) f = f := by cat_disch) (comp_id : ∀ {X Y : obj} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id Y) = f := by cat_disch) (assoc : ∀ {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h) := by cat_disch) : CategoryTheory.Category.{v, u} obj
• CategoryTheory.Functor.map_id 📋 Mathlib.CategoryTheory.Functor.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (self : CategoryTheory.Functor C D) (X : C) : self.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (self.obj X)
• CategoryTheory.Functor.mk 📋 Mathlib.CategoryTheory.Functor.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (obj : C → D) (map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)) (map_id : ∀ (X : C), map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (obj X) := by cat_disch) (map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (map f) (map g) := by cat_disch) : CategoryTheory.Functor C D
• CategoryTheory.NatTrans.id_app' 📋 Mathlib.CategoryTheory.NatTrans
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C) : (CategoryTheory.NatTrans.id F).app X = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.IsIso.id 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) : CategoryTheory.IsIso (CategoryTheory.CategoryStruct.id X)
• CategoryTheory.Iso.refl_hom 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) : (CategoryTheory.Iso.refl X).hom = CategoryTheory.CategoryStruct.id X
• CategoryTheory.Iso.refl_inv 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) : (CategoryTheory.Iso.refl X).inv = CategoryTheory.CategoryStruct.id X
• CategoryTheory.IsIso.inv_id 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} : CategoryTheory.inv (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id X
• CategoryTheory.Iso.hom_inv_id 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (self : X ≅ Y) : CategoryTheory.CategoryStruct.comp self.hom self.inv = CategoryTheory.CategoryStruct.id X
• CategoryTheory.Iso.inv_hom_id 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (self : X ≅ Y) : CategoryTheory.CategoryStruct.comp self.inv self.hom = CategoryTheory.CategoryStruct.id Y
• CategoryTheory.IsIso.hom_inv_id 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [I : CategoryTheory.IsIso f] : CategoryTheory.CategoryStruct.comp f (CategoryTheory.inv f) = CategoryTheory.CategoryStruct.id X
• CategoryTheory.IsIso.inv_hom_id 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [I : CategoryTheory.IsIso f] : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv f) f = CategoryTheory.CategoryStruct.id Y
• CategoryTheory.isIso_of_comp_hom_eq_id 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (g : Y ⟶ X) [CategoryTheory.IsIso g] {f : X ⟶ Y} (h : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.id X) : CategoryTheory.IsIso f
• CategoryTheory.isIso_of_hom_comp_eq_id 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (g : X ⟶ Y) [CategoryTheory.IsIso g] {f : Y ⟶ X} (h : CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.id X) : CategoryTheory.IsIso f
• CategoryTheory.Iso.inv_ext 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ≅ Y} {g : Y ⟶ X} (hom_inv_id : CategoryTheory.CategoryStruct.comp f.hom g = CategoryTheory.CategoryStruct.id X) : f.inv = g
• CategoryTheory.Iso.inv_ext' 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ≅ Y} {g : Y ⟶ X} (hom_inv_id : CategoryTheory.CategoryStruct.comp f.hom g = CategoryTheory.CategoryStruct.id X) : g = f.inv
• CategoryTheory.Iso.comp_hom_eq_id 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) {f : Y ⟶ X} : CategoryTheory.CategoryStruct.comp f α.hom = CategoryTheory.CategoryStruct.id Y ↔ f = α.inv
• CategoryTheory.Iso.comp_inv_eq_id 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) {f : X ⟶ Y} : CategoryTheory.CategoryStruct.comp f α.inv = CategoryTheory.CategoryStruct.id X ↔ f = α.hom
• CategoryTheory.Iso.hom_comp_eq_id 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) {f : Y ⟶ X} : CategoryTheory.CategoryStruct.comp α.hom f = CategoryTheory.CategoryStruct.id X ↔ f = α.inv
• CategoryTheory.Iso.inv_comp_eq_id 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) {f : X ⟶ Y} : CategoryTheory.CategoryStruct.comp α.inv f = CategoryTheory.CategoryStruct.id Y ↔ f = α.hom
• CategoryTheory.IsIso.eq_inv_of_hom_inv_id 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.IsIso f] {g : Y ⟶ X} (hom_inv_id : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.id X) : g = CategoryTheory.inv f
• CategoryTheory.IsIso.eq_inv_of_inv_hom_id 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : Y ⟶ X} [CategoryTheory.IsIso f] {g : X ⟶ Y} (hom_inv_id : CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.id X) : g = CategoryTheory.inv f
• CategoryTheory.IsIso.inv_eq_of_hom_inv_id 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.IsIso f] {g : Y ⟶ X} (hom_inv_id : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.id X) : CategoryTheory.inv f = g
• CategoryTheory.IsIso.inv_eq_of_inv_hom_id 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : Y ⟶ X} [CategoryTheory.IsIso f] {g : X ⟶ Y} (hom_inv_id : CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.id X) : CategoryTheory.inv f = g
• CategoryTheory.comp_hom_eq_id 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (g : Y ⟶ X) [CategoryTheory.IsIso g] {f : X ⟶ Y} : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.id X ↔ f = CategoryTheory.inv g
• CategoryTheory.comp_inv_eq_id 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (g : Y ⟶ X) [CategoryTheory.IsIso g] {f : Y ⟶ X} : CategoryTheory.CategoryStruct.comp f (CategoryTheory.inv g) = CategoryTheory.CategoryStruct.id Y ↔ f = g
• CategoryTheory.hom_comp_eq_id 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (g : X ⟶ Y) [CategoryTheory.IsIso g] {f : Y ⟶ X} : CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.id X ↔ f = CategoryTheory.inv g
• CategoryTheory.inv_comp_eq_id 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (g : X ⟶ Y) [CategoryTheory.IsIso g] {f : X ⟶ Y} : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv g) f = CategoryTheory.CategoryStruct.id Y ↔ f = g
• CategoryTheory.Iso.mk 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (hom : X ⟶ Y) (inv : Y ⟶ X) (hom_inv_id : CategoryTheory.CategoryStruct.comp hom inv = CategoryTheory.CategoryStruct.id X := by cat_disch) (inv_hom_id : CategoryTheory.CategoryStruct.comp inv hom = CategoryTheory.CategoryStruct.id Y := by cat_disch) : X ≅ Y
• CategoryTheory.IsIso.mk 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (out : ∃ inv, CategoryTheory.CategoryStruct.comp f inv = CategoryTheory.CategoryStruct.id X ∧ CategoryTheory.CategoryStruct.comp inv f = CategoryTheory.CategoryStruct.id Y) : CategoryTheory.IsIso f
• CategoryTheory.IsIso.mk' 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : Y ⟶ X} (out : ∃ inv, CategoryTheory.CategoryStruct.comp inv f = CategoryTheory.CategoryStruct.id X ∧ CategoryTheory.CategoryStruct.comp f inv = CategoryTheory.CategoryStruct.id Y) : CategoryTheory.IsIso f
• CategoryTheory.IsIso.out 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {X Y : C} {f : X ⟶ Y} [self : CategoryTheory.IsIso f] : ∃ inv, CategoryTheory.CategoryStruct.comp f inv = CategoryTheory.CategoryStruct.id X ∧ CategoryTheory.CategoryStruct.comp inv f = CategoryTheory.CategoryStruct.id Y
• CategoryTheory.Iso.symm_mk 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (hom : X ⟶ Y) (inv : Y ⟶ X) (hom_inv_id : CategoryTheory.CategoryStruct.comp hom inv = CategoryTheory.CategoryStruct.id X) (inv_hom_id : CategoryTheory.CategoryStruct.comp inv hom = CategoryTheory.CategoryStruct.id Y) : { hom := hom, inv := inv, hom_inv_id := hom_inv_id, inv_hom_id := inv_hom_id }.symm = { hom := inv, inv := hom, hom_inv_id := inv_hom_id, inv_hom_id := hom_inv_id }
• CategoryTheory.Functor.map_hom_inv' 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X Y : C} (f : X ≅ Y) : CategoryTheory.CategoryStruct.comp (F.map f.hom) (F.map f.inv) = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.Functor.map_inv_hom' 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X Y : C} (f : X ≅ Y) : CategoryTheory.CategoryStruct.comp (F.map f.inv) (F.map f.hom) = CategoryTheory.CategoryStruct.id (F.obj Y)
• CategoryTheory.Iso.map_hom_inv_id 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {X Y : C} (e : X ≅ Y) (F : CategoryTheory.Functor C D) : CategoryTheory.CategoryStruct.comp (F.map e.hom) (F.map e.inv) = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.Iso.map_inv_hom_id 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {X Y : C} (e : X ≅ Y) (F : CategoryTheory.Functor C D) : CategoryTheory.CategoryStruct.comp (F.map e.inv) (F.map e.hom) = CategoryTheory.CategoryStruct.id (F.obj Y)
• CategoryTheory.Functor.map_hom_inv 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso f] : CategoryTheory.CategoryStruct.comp (F.map f) (F.map (CategoryTheory.inv f)) = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.Functor.map_inv_hom 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X Y : C} (f : Y ⟶ X) [CategoryTheory.IsIso f] : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.inv f)) (F.map f) = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.Iso.trans_mk 📋 Mathlib.CategoryTheory.Iso
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (hom : X ⟶ Y) (inv : Y ⟶ X) (hom_inv_id : CategoryTheory.CategoryStruct.comp hom inv = CategoryTheory.CategoryStruct.id X) (inv_hom_id : CategoryTheory.CategoryStruct.comp inv hom = CategoryTheory.CategoryStruct.id Y) (hom' : Y ⟶ Z) (inv' : Z ⟶ Y) (hom_inv_id' : CategoryTheory.CategoryStruct.comp hom' inv' = CategoryTheory.CategoryStruct.id Y) (inv_hom_id' : CategoryTheory.CategoryStruct.comp inv' hom' = CategoryTheory.CategoryStruct.id Z) (hom_inv_id'' : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp hom hom') (CategoryTheory.CategoryStruct.comp inv' inv) = CategoryTheory.CategoryStruct.id X) (inv_hom_id'' : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp inv' inv) (CategoryTheory.CategoryStruct.comp hom hom') = CategoryTheory.CategoryStruct.id Z) : { hom := hom, inv := inv, hom_inv_id := hom_inv_id, inv_hom_id := inv_hom_id } ≪≫ { hom := hom', inv := inv', hom_inv_id := hom_inv_id', inv_hom_id := inv_hom_id' } = { hom := CategoryTheory.CategoryStruct.comp hom hom', inv := CategoryTheory.CategoryStruct.comp inv' inv, hom_inv_id := hom_inv_id'', inv_hom_id := inv_hom_id'' }
• CategoryTheory.NatTrans.id_app 📋 Mathlib.CategoryTheory.Functor.Category
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C) : (CategoryTheory.CategoryStruct.id F).app X = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.Functor.leftUnitor_hom_app 📋 Mathlib.CategoryTheory.Functor.Category
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C) : F.leftUnitor.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.Functor.leftUnitor_inv_app 📋 Mathlib.CategoryTheory.Functor.Category
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C) : F.leftUnitor.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.Functor.rightUnitor_hom_app 📋 Mathlib.CategoryTheory.Functor.Category
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C) : F.rightUnitor.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.Functor.rightUnitor_inv_app 📋 Mathlib.CategoryTheory.Functor.Category
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C) : F.rightUnitor.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.NatTrans.id_hcomp_app 📋 Mathlib.CategoryTheory.Functor.Category
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor E C} (α : F ⟶ G) (X : E) : (CategoryTheory.CategoryStruct.id H ◫ α).app X = α.app (H.obj X)
• CategoryTheory.NatTrans.hcomp_id_app 📋 Mathlib.CategoryTheory.Functor.Category
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor D E} (α : F ⟶ G) (X : C) : (α ◫ CategoryTheory.CategoryStruct.id H).app X = H.map (α.app X)
• CategoryTheory.Functor.associator_hom_app 📋 Mathlib.CategoryTheory.Functor.Category
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {E' : Type u₄} [CategoryTheory.Category.{v₄, u₄} E'] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) (H : CategoryTheory.Functor E E') (x✝ : C) : (F.associator G H).hom.app x✝ = CategoryTheory.CategoryStruct.id (((F.comp G).comp H).obj x✝)
• CategoryTheory.Functor.associator_inv_app 📋 Mathlib.CategoryTheory.Functor.Category
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {E' : Type u₄} [CategoryTheory.Category.{v₄, u₄} E'] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) (H : CategoryTheory.Functor E E') (x✝ : C) : (F.associator G H).inv.app x✝ = CategoryTheory.CategoryStruct.id ((F.comp (G.comp H)).obj x✝)
• CategoryTheory.Iso.map_hom_inv_id_app 📋 Mathlib.CategoryTheory.Functor.Category
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {X Y : C} (e : X ≅ Y) (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (Z : D) : CategoryTheory.CategoryStruct.comp ((F.map e.hom).app Z) ((F.map e.inv).app Z) = CategoryTheory.CategoryStruct.id ((F.obj X).obj Z)
• CategoryTheory.Iso.map_inv_hom_id_app 📋 Mathlib.CategoryTheory.Functor.Category
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {X Y : C} (e : X ≅ Y) (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (Z : D) : CategoryTheory.CategoryStruct.comp ((F.map e.inv).app Z) ((F.map e.hom).app Z) = CategoryTheory.CategoryStruct.id ((F.obj Y).obj Z)
• CategoryTheory.Iso.hom_inv_id_app 📋 Mathlib.CategoryTheory.NatIso
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (α : F ≅ G) (X : C) : CategoryTheory.CategoryStruct.comp (α.hom.app X) (α.inv.app X) = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.Iso.inv_hom_id_app 📋 Mathlib.CategoryTheory.NatIso
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (α : F ≅ G) (X : C) : CategoryTheory.CategoryStruct.comp (α.inv.app X) (α.hom.app X) = CategoryTheory.CategoryStruct.id (G.obj X)
• CategoryTheory.Iso.hom_inv_id_app_app 📋 Mathlib.CategoryTheory.NatIso
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F G : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (e : F ≅ G) (X₁ : C) (X₂ : D) : CategoryTheory.CategoryStruct.comp ((e.hom.app X₁).app X₂) ((e.inv.app X₁).app X₂) = CategoryTheory.CategoryStruct.id ((F.obj X₁).obj X₂)
• CategoryTheory.Iso.inv_hom_id_app_app 📋 Mathlib.CategoryTheory.NatIso
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F G : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (e : F ≅ G) (X₁ : C) (X₂ : D) : CategoryTheory.CategoryStruct.comp ((e.inv.app X₁).app X₂) ((e.hom.app X₁).app X₂) = CategoryTheory.CategoryStruct.id ((G.obj X₁).obj X₂)
• CategoryTheory.Iso.hom_inv_id_app_app_app 📋 Mathlib.CategoryTheory.NatIso
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {E' : Type u₄} [CategoryTheory.Category.{v₄, u₄} E'] {F G : CategoryTheory.Functor C (CategoryTheory.Functor D (CategoryTheory.Functor E E'))} (e : F ≅ G) (X₁ : C) (X₂ : D) (X₃ : E) : CategoryTheory.CategoryStruct.comp (((e.hom.app X₁).app X₂).app X₃) (((e.inv.app X₁).app X₂).app X₃) = CategoryTheory.CategoryStruct.id (((F.obj X₁).obj X₂).obj X₃)
• CategoryTheory.Iso.inv_hom_id_app_app_app 📋 Mathlib.CategoryTheory.NatIso
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {E' : Type u₄} [CategoryTheory.Category.{v₄, u₄} E'] {F G : CategoryTheory.Functor C (CategoryTheory.Functor D (CategoryTheory.Functor E E'))} (e : F ≅ G) (X₁ : C) (X₂ : D) (X₃ : E) : CategoryTheory.CategoryStruct.comp (((e.inv.app X₁).app X₂).app X₃) (((e.hom.app X₁).app X₂).app X₃) = CategoryTheory.CategoryStruct.id (((G.obj X₁).obj X₂).obj X₃)
• CategoryTheory.Functor.FullyFaithful.preimage_id 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {X : C} : hF.preimage (CategoryTheory.CategoryStruct.id (F.obj X)) = CategoryTheory.CategoryStruct.id X
• CategoryTheory.Functor.preimage_id 📋 Mathlib.CategoryTheory.Functor.FullyFaithful
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {X : C} [F.Full] [F.Faithful] : F.preimage (CategoryTheory.CategoryStruct.id (F.obj X)) = CategoryTheory.CategoryStruct.id X
• CategoryTheory.InducedCategory.id_hom 📋 Mathlib.CategoryTheory.InducedCategory
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] {F : C → D} (X : CategoryTheory.InducedCategory D F) : (CategoryTheory.CategoryStruct.id X).hom = CategoryTheory.CategoryStruct.id (F X)
• CategoryTheory.ObjectProperty.FullSubcategory.id_hom 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) (X : P.FullSubcategory) : (CategoryTheory.CategoryStruct.id X).hom = CategoryTheory.CategoryStruct.id X.obj
• CategoryTheory.ObjectProperty.isoHom_inv_id_hom 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory} (e : X ≅ Y) : CategoryTheory.CategoryStruct.comp e.hom.hom e.inv.hom = CategoryTheory.CategoryStruct.id X.obj
• CategoryTheory.ObjectProperty.isoInv_hom_id_hom 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory} (e : X ≅ Y) : CategoryTheory.CategoryStruct.comp e.inv.hom e.hom.hom = CategoryTheory.CategoryStruct.id Y.obj
• CategoryTheory.hom_id 📋 Mathlib.CategoryTheory.ConcreteCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] {X : C} : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id
• CategoryTheory.ConcreteCategory.coe_id 📋 Mathlib.CategoryTheory.ConcreteCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] {X : C} : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id
• CategoryTheory.ConcreteCategory.id_apply 📋 Mathlib.CategoryTheory.ConcreteCategory.Basic
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {FC : outParam (C → C → Type u_1)} {CC : outParam (C → Type w)} {inst✝¹ : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))} [self : CategoryTheory.ConcreteCategory C FC] {X : C} (x : CC X) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x
• CategoryTheory.id_apply 📋 Mathlib.CategoryTheory.ConcreteCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] {X : C} (x : CategoryTheory.ToType X) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x
• CategoryTheory.ConcreteCategory.mk 📋 Mathlib.CategoryTheory.ConcreteCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : outParam (C → C → Type u_1)} {CC : outParam (C → Type w)} [outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))] (hom : {X Y : C} → (X ⟶ Y) → FC X Y) (ofHom : {X Y : C} → FC X Y → (X ⟶ Y)) (hom_ofHom : ∀ {X Y : C} (f : FC X Y), hom (ofHom f) = f := by cat_disch) (ofHom_hom : ∀ {X Y : C} (f : X ⟶ Y), ofHom (hom f) = f := by cat_disch) (id_apply : ∀ {X : C} (x : CC X), (hom (CategoryTheory.CategoryStruct.id X)) x = x := by cat_disch) (comp_apply : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (x : CC X), (hom (CategoryTheory.CategoryStruct.comp f g)) x = (hom g) ((hom f) x) := by cat_disch) : CategoryTheory.ConcreteCategory C FC
• CategoryTheory.Functor.whiskerLeft_id' 📋 Mathlib.CategoryTheory.Whiskering
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D E} : F.whiskerLeft (CategoryTheory.CategoryStruct.id G) = CategoryTheory.CategoryStruct.id (F.comp G)
• CategoryTheory.Functor.whiskerRight_id' 📋 Mathlib.CategoryTheory.Whiskering
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G : CategoryTheory.Functor C D} (F : CategoryTheory.Functor D E) : CategoryTheory.Functor.whiskerRight (CategoryTheory.CategoryStruct.id G) F = CategoryTheory.CategoryStruct.id (G.comp F)
• CategoryTheory.Functor.hcomp_id 📋 Mathlib.CategoryTheory.Whiskering
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {G H : CategoryTheory.Functor C D} (α : G ⟶ H) (F : CategoryTheory.Functor D E) : α ◫ CategoryTheory.CategoryStruct.id F = CategoryTheory.Functor.whiskerRight α F
• CategoryTheory.Functor.id_hcomp 📋 Mathlib.CategoryTheory.Whiskering
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) {G H : CategoryTheory.Functor D E} (α : G ⟶ H) : CategoryTheory.CategoryStruct.id F ◫ α = F.whiskerLeft α
• CategoryTheory.Functor.whiskeringLeftObjIdIso_hom_app_app 📋 Mathlib.CategoryTheory.Whiskering
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (X : CategoryTheory.Functor C E) (X✝ : C) : (CategoryTheory.Functor.whiskeringLeftObjIdIso.hom.app X).app X✝ = CategoryTheory.CategoryStruct.id (X.obj X✝)
• CategoryTheory.Functor.whiskeringLeftObjIdIso_inv_app_app 📋 Mathlib.CategoryTheory.Whiskering
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (X : CategoryTheory.Functor C E) (X✝ : C) : (CategoryTheory.Functor.whiskeringLeftObjIdIso.inv.app X).app X✝ = CategoryTheory.CategoryStruct.id (X.obj X✝)
• CategoryTheory.Functor.whiskeringRightObjIdIso_hom_app_app 📋 Mathlib.CategoryTheory.Whiskering
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (X : CategoryTheory.Functor E C) (X✝ : E) : (CategoryTheory.Functor.whiskeringRightObjIdIso.hom.app X).app X✝ = CategoryTheory.CategoryStruct.id (X.obj X✝)
• CategoryTheory.Functor.whiskeringRightObjIdIso_inv_app_app 📋 Mathlib.CategoryTheory.Whiskering
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (X : CategoryTheory.Functor E C) (X✝ : E) : (CategoryTheory.Functor.whiskeringRightObjIdIso.inv.app X).app X✝ = CategoryTheory.CategoryStruct.id (X.obj X✝)
• CategoryTheory.Functor.whiskeringLeftObjCompIso_hom_app_app 📋 Mathlib.CategoryTheory.Whiskering
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {D' : Type u₄} [CategoryTheory.Category.{v₄, u₄} D'] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D D') (X : CategoryTheory.Functor D' E) (X✝ : C) : ((F.whiskeringLeftObjCompIso G).hom.app X).app X✝ = CategoryTheory.CategoryStruct.id (X.obj (G.obj (F.obj X✝)))
• CategoryTheory.Functor.whiskeringLeftObjCompIso_inv_app_app 📋 Mathlib.CategoryTheory.Whiskering
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {D' : Type u₄} [CategoryTheory.Category.{v₄, u₄} D'] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D D') (X : CategoryTheory.Functor D' E) (X✝ : C) : ((F.whiskeringLeftObjCompIso G).inv.app X).app X✝ = CategoryTheory.CategoryStruct.id (X.obj (G.obj (F.obj X✝)))
• CategoryTheory.Functor.whiskeringRightObjCompIso_hom_app_app 📋 Mathlib.CategoryTheory.Whiskering
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {D' : Type u₄} [CategoryTheory.Category.{v₄, u₄} D'] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D D') (X : CategoryTheory.Functor E C) (X✝ : E) : ((F.whiskeringRightObjCompIso G).hom.app X).app X✝ = CategoryTheory.CategoryStruct.id (G.obj (F.obj (X.obj X✝)))
• CategoryTheory.Functor.whiskeringRightObjCompIso_inv_app_app 📋 Mathlib.CategoryTheory.Whiskering
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {D' : Type u₄} [CategoryTheory.Category.{v₄, u₄} D'] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D D') (X : CategoryTheory.Functor E C) (X✝ : E) : ((F.whiskeringRightObjCompIso G).inv.app X).app X✝ = CategoryTheory.CategoryStruct.id (G.obj (F.obj (X.obj X✝)))
• CategoryTheory.Functor.toEssImageCompι_hom_app 📋 Mathlib.CategoryTheory.EssentialImage
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C) : F.toEssImageCompι.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.Functor.toEssImageCompι_inv_app 📋 Mathlib.CategoryTheory.EssentialImage
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C) : F.toEssImageCompι.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.Equivalence.mkHom_id_functor 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {e : C ≌ D} : CategoryTheory.Equivalence.mkHom (CategoryTheory.CategoryStruct.id e.functor) = CategoryTheory.CategoryStruct.id e
• CategoryTheory.Equivalence.id_asNatTrans 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {e : C ≌ D} : CategoryTheory.Equivalence.asNatTrans (CategoryTheory.CategoryStruct.id e) = CategoryTheory.CategoryStruct.id e.functor
• CategoryTheory.Equivalence.mkHom_id_inverse 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {e : C ≌ D} : CategoryTheory.Equivalence.mkHom (CategoryTheory.CategoryStruct.id e.inverse) = CategoryTheory.CategoryStruct.id e.symm
• CategoryTheory.Equivalence.counitIso_inv_hom_id_app 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (Y : D) : CategoryTheory.CategoryStruct.comp (e.counitInv.app Y) (e.counit.app Y) = CategoryTheory.CategoryStruct.id Y
• CategoryTheory.Equivalence.unitIso_hom_inv_id_app 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X : C) : CategoryTheory.CategoryStruct.comp (e.unit.app X) (e.unitInv.app X) = CategoryTheory.CategoryStruct.id X
• CategoryTheory.Equivalence.counitIso_hom_inv_id_app 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (Y : D) : CategoryTheory.CategoryStruct.comp (e.counit.app Y) (e.counitInv.app Y) = CategoryTheory.CategoryStruct.id (e.functor.obj (e.inverse.obj Y))
• CategoryTheory.Equivalence.unitIso_inv_hom_id_app 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X : C) : CategoryTheory.CategoryStruct.comp (e.unitInv.app X) (e.unit.app X) = CategoryTheory.CategoryStruct.id (e.inverse.obj (e.functor.obj X))
• CategoryTheory.Equivalence.counitInv_functor_comp 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X : C) : CategoryTheory.CategoryStruct.comp (e.counitInv.app (e.functor.obj X)) (e.functor.map (e.unitInv.app X)) = CategoryTheory.CategoryStruct.id (e.functor.obj X)
• CategoryTheory.Equivalence.functor_unit_comp 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X : C) : CategoryTheory.CategoryStruct.comp (e.functor.map (e.unit.app X)) (e.counit.app (e.functor.obj X)) = CategoryTheory.CategoryStruct.id (e.functor.obj X)
• CategoryTheory.Equivalence.inverse_counitInv_comp 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (Y : D) : CategoryTheory.CategoryStruct.comp (e.inverse.map (e.counitInv.app Y)) (e.unitInv.app (e.inverse.obj Y)) = CategoryTheory.CategoryStruct.id (e.inverse.obj Y)
• CategoryTheory.Equivalence.unit_inverse_comp 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (Y : D) : CategoryTheory.CategoryStruct.comp (e.unit.app (e.inverse.obj Y)) (e.inverse.map (e.counit.app Y)) = CategoryTheory.CategoryStruct.id (e.inverse.obj Y)
• CategoryTheory.Equivalence.mk'' 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (functor : CategoryTheory.Functor C D) (inverse : CategoryTheory.Functor D C) (unitIso : CategoryTheory.Functor.id C ≅ functor.comp inverse) (counitIso : inverse.comp functor ≅ CategoryTheory.Functor.id D) (functor_unitIso_comp : ∀ (X : C), CategoryTheory.CategoryStruct.comp (counitIso.inv.app (functor.obj X)) (functor.map (unitIso.inv.app X)) = CategoryTheory.CategoryStruct.id (functor.obj X)) : C ≌ D
• CategoryTheory.Equivalence.mk' 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (functor : CategoryTheory.Functor C D) (inverse : CategoryTheory.Functor D C) (unitIso : CategoryTheory.Functor.id C ≅ functor.comp inverse) (counitIso : inverse.comp functor ≅ CategoryTheory.Functor.id D) (functor_unitIso_comp : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor.map (unitIso.hom.app X)) (counitIso.hom.app (functor.obj X)) = CategoryTheory.CategoryStruct.id (functor.obj X) := by cat_disch) : C ≌ D
• CategoryTheory.Equivalence.adjointify_η_ε 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (η : CategoryTheory.Functor.id C ≅ F.comp G) (ε : G.comp F ≅ CategoryTheory.Functor.id D) (X : C) : CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.Equivalence.adjointifyη η ε).hom.app X)) (ε.hom.app (F.obj X)) = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.Equivalence.counitIso_functor_comp 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X : C) : CategoryTheory.CategoryStruct.comp (e.counitIso.inv.app (e.functor.obj X)) (e.functor.map (e.unitIso.inv.app X)) = CategoryTheory.CategoryStruct.id (e.functor.obj X)
• CategoryTheory.Equivalence.functor_unitIso_comp 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (self : C ≌ D) (X : C) : CategoryTheory.CategoryStruct.comp (self.functor.map (self.unitIso.hom.app X)) (self.counitIso.hom.app (self.functor.obj X)) = CategoryTheory.CategoryStruct.id (self.functor.obj X)
• CategoryTheory.Equivalence.Equivalence_mk'_counit 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (functor : CategoryTheory.Functor C D) (inverse : CategoryTheory.Functor D C) (unit_iso : CategoryTheory.Functor.id C ≅ functor.comp inverse) (counit_iso : inverse.comp functor ≅ CategoryTheory.Functor.id D) (f : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) = CategoryTheory.CategoryStruct.id (functor.obj X)) : { functor := functor, inverse := inverse, unitIso := unit_iso, counitIso := counit_iso, functor_unitIso_comp := f }.counit = counit_iso.hom
• CategoryTheory.Equivalence.Equivalence_mk'_counitInv 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (functor : CategoryTheory.Functor C D) (inverse : CategoryTheory.Functor D C) (unit_iso : CategoryTheory.Functor.id C ≅ functor.comp inverse) (counit_iso : inverse.comp functor ≅ CategoryTheory.Functor.id D) (f : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) = CategoryTheory.CategoryStruct.id (functor.obj X)) : { functor := functor, inverse := inverse, unitIso := unit_iso, counitIso := counit_iso, functor_unitIso_comp := f }.counitInv = counit_iso.inv
• CategoryTheory.Equivalence.Equivalence_mk'_unit 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (functor : CategoryTheory.Functor C D) (inverse : CategoryTheory.Functor D C) (unit_iso : CategoryTheory.Functor.id C ≅ functor.comp inverse) (counit_iso : inverse.comp functor ≅ CategoryTheory.Functor.id D) (f : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) = CategoryTheory.CategoryStruct.id (functor.obj X)) : { functor := functor, inverse := inverse, unitIso := unit_iso, counitIso := counit_iso, functor_unitIso_comp := f }.unit = unit_iso.hom
• CategoryTheory.Equivalence.Equivalence_mk'_unitInv 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (functor : CategoryTheory.Functor C D) (inverse : CategoryTheory.Functor D C) (unit_iso : CategoryTheory.Functor.id C ≅ functor.comp inverse) (counit_iso : inverse.comp functor ≅ CategoryTheory.Functor.id D) (f : ∀ (X : C), CategoryTheory.CategoryStruct.comp (functor.map (unit_iso.hom.app X)) (counit_iso.hom.app (functor.obj X)) = CategoryTheory.CategoryStruct.id (functor.obj X)) : { functor := functor, inverse := inverse, unitIso := unit_iso, counitIso := counit_iso, functor_unitIso_comp := f }.unitInv = unit_iso.inv
• CategoryTheory.unop_id 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.CategoryStruct.{v₁, u₁} C] {X : Cᵒᵖ} : (CategoryTheory.CategoryStruct.id X).unop = CategoryTheory.CategoryStruct.id (Opposite.unop X)
• CategoryTheory.op_id 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.CategoryStruct.{v₁, u₁} C] {X : C} : (CategoryTheory.CategoryStruct.id X).op = CategoryTheory.CategoryStruct.id (Opposite.op X)
• CategoryTheory.unop_id_op 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.CategoryStruct.{v₁, u₁} C] {X : C} : (CategoryTheory.CategoryStruct.id (Opposite.op X)).unop = CategoryTheory.CategoryStruct.id X
• CategoryTheory.op_id_unop 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.CategoryStruct.{v₁, u₁} C] {X : Cᵒᵖ} : (CategoryTheory.CategoryStruct.id (Opposite.unop X)).op = CategoryTheory.CategoryStruct.id X
• CategoryTheory.Functor.opUnopIso_hom_app 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C) : F.opUnopIso.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.Functor.opUnopIso_inv_app 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C) : F.opUnopIso.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.NatTrans.removeOp_id 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : CategoryTheory.NatTrans.removeOp (CategoryTheory.CategoryStruct.id F.op) = CategoryTheory.CategoryStruct.id F
• CategoryTheory.Functor.unopId_hom_app 📋 Mathlib.CategoryTheory.Opposites
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : C) : (CategoryTheory.Functor.unopId C).hom.app X = CategoryTheory.CategoryStruct.id X
• CategoryTheory.Functor.unopId_inv_app 📋 Mathlib.CategoryTheory.Opposites
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : C) : (CategoryTheory.Functor.unopId C).inv.app X = CategoryTheory.CategoryStruct.id X
• CategoryTheory.NatTrans.removeLeftOp_id 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C Dᵒᵖ} : CategoryTheory.NatTrans.removeLeftOp (CategoryTheory.CategoryStruct.id F.leftOp) = CategoryTheory.CategoryStruct.id F
• CategoryTheory.NatTrans.removeRightOp_id 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor Cᵒᵖ D} : CategoryTheory.NatTrans.removeRightOp (CategoryTheory.CategoryStruct.id F.rightOp) = CategoryTheory.CategoryStruct.id F
• CategoryTheory.NatTrans.unop_id 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) : CategoryTheory.NatTrans.unop (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id F.unop
• CategoryTheory.Functor.rightOpLeftOpIso_hom_app 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ D) (X : Cᵒᵖ) : F.rightOpLeftOpIso.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.Functor.rightOpLeftOpIso_inv_app 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ D) (X : Cᵒᵖ) : F.rightOpLeftOpIso.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.NatTrans.leftOp_id 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C Dᵒᵖ} : CategoryTheory.NatTrans.leftOp (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id F.leftOp
• CategoryTheory.NatTrans.rightOp_id 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor Cᵒᵖ D} : CategoryTheory.NatTrans.rightOp (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id F.rightOp
• CategoryTheory.Functor.leftOpRightOpIso_hom_app 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C Dᵒᵖ) (X : C) : F.leftOpRightOpIso.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.Functor.leftOpRightOpIso_inv_app 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C Dᵒᵖ) (X : C) : F.leftOpRightOpIso.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.NatTrans.removeUnop_id 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) : CategoryTheory.NatTrans.removeUnop (CategoryTheory.CategoryStruct.id F.unop) = CategoryTheory.CategoryStruct.id F
• CategoryTheory.Functor.opId_hom_app 📋 Mathlib.CategoryTheory.Opposites
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : Cᵒᵖ) : (CategoryTheory.Functor.opId C).hom.app X = CategoryTheory.CategoryStruct.id X
• CategoryTheory.Functor.opId_inv_app 📋 Mathlib.CategoryTheory.Opposites
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : Cᵒᵖ) : (CategoryTheory.Functor.opId C).inv.app X = CategoryTheory.CategoryStruct.id X
• CategoryTheory.NatTrans.op_id 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : CategoryTheory.NatTrans.op (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id F.op
• CategoryTheory.Functor.unopOpIso_hom_app 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) (X : Cᵒᵖ) : F.unopOpIso.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.Functor.unopOpIso_inv_app 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) (X : Cᵒᵖ) : F.unopOpIso.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.Functor.leftOpId_hom_app 📋 Mathlib.CategoryTheory.Opposites
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : Cᵒᵖᵒᵖ) : (CategoryTheory.Functor.leftOpId C).hom.app X = CategoryTheory.CategoryStruct.id (Opposite.unop (Opposite.unop X))
• CategoryTheory.Functor.leftOpId_inv_app 📋 Mathlib.CategoryTheory.Opposites
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : Cᵒᵖᵒᵖ) : (CategoryTheory.Functor.leftOpId C).inv.app X = CategoryTheory.CategoryStruct.id (Opposite.unop (Opposite.unop X))
• CategoryTheory.Functor.rightOpId_hom_app 📋 Mathlib.CategoryTheory.Opposites
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : C) : (CategoryTheory.Functor.rightOpId C).hom.app X = CategoryTheory.CategoryStruct.id (Opposite.op (Opposite.op X))
• CategoryTheory.Functor.rightOpId_inv_app 📋 Mathlib.CategoryTheory.Opposites
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (X : C) : (CategoryTheory.Functor.rightOpId C).inv.app X = CategoryTheory.CategoryStruct.id (Opposite.op (Opposite.op X))
• CategoryTheory.Functor.leftOpComp_hom_app 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D Eᵒᵖ) (X : Cᵒᵖ) : (F.leftOpComp G).hom.app X = CategoryTheory.CategoryStruct.id (Opposite.unop (G.obj (F.obj (Opposite.unop X))))
• CategoryTheory.Functor.leftOpComp_inv_app 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D Eᵒᵖ) (X : Cᵒᵖ) : (F.leftOpComp G).inv.app X = CategoryTheory.CategoryStruct.id (Opposite.unop (G.obj (F.obj (Opposite.unop X))))
• CategoryTheory.Functor.opComp_hom_app 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) (X : Cᵒᵖ) : (F.opComp G).hom.app X = CategoryTheory.CategoryStruct.id (Opposite.op (G.obj (F.obj (Opposite.unop X))))
• CategoryTheory.Functor.opComp_inv_app 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) (X : Cᵒᵖ) : (F.opComp G).inv.app X = CategoryTheory.CategoryStruct.id (Opposite.op (G.obj (F.obj (Opposite.unop X))))
• CategoryTheory.Functor.rightOpComp_hom_app 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] (F : CategoryTheory.Functor Cᵒᵖ D) (G : CategoryTheory.Functor D E) (X : C) : (F.rightOpComp G).hom.app X = CategoryTheory.CategoryStruct.id (Opposite.op (G.obj (F.obj (Opposite.op X))))
• CategoryTheory.Functor.rightOpComp_inv_app 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] (F : CategoryTheory.Functor Cᵒᵖ D) (G : CategoryTheory.Functor D E) (X : C) : (F.rightOpComp G).inv.app X = CategoryTheory.CategoryStruct.id (Opposite.op (G.obj (F.obj (Opposite.op X))))
• CategoryTheory.Functor.unopComp_hom_app 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) (G : CategoryTheory.Functor Dᵒᵖ Eᵒᵖ) (X : C) : (F.unopComp G).hom.app X = CategoryTheory.CategoryStruct.id (Opposite.unop (G.obj (F.obj (Opposite.op X))))
• CategoryTheory.Functor.unopComp_inv_app 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{v_1, u_1} E] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) (G : CategoryTheory.Functor Dᵒᵖ Eᵒᵖ) (X : C) : (F.unopComp G).inv.app X = CategoryTheory.CategoryStruct.id (Opposite.unop (G.obj (F.obj (Opposite.op X))))
• CategoryTheory.Iso.unop_hom_inv_id_app 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {F G : CategoryTheory.Functor C Dᵒᵖ} (e : F ≅ G) (X : C) : CategoryTheory.CategoryStruct.comp (e.hom.app X).unop (e.inv.app X).unop = CategoryTheory.CategoryStruct.id (Opposite.unop (G.obj X))
• CategoryTheory.Iso.unop_inv_hom_id_app 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {F G : CategoryTheory.Functor C Dᵒᵖ} (e : F ≅ G) (X : C) : CategoryTheory.CategoryStruct.comp (e.inv.app X).unop (e.hom.app X).unop = CategoryTheory.CategoryStruct.id (Opposite.unop (F.obj X))
• CategoryTheory.Functor.leftOpRightOpEquiv_counitIso_hom_app_app 📋 Mathlib.CategoryTheory.Opposites
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (X : CategoryTheory.Functor C Dᵒᵖ) (X✝ : C) : ((CategoryTheory.Functor.leftOpRightOpEquiv C D).counitIso.hom.app X).app X✝ = CategoryTheory.CategoryStruct.id (X.obj X✝)
• CategoryTheory.Functor.leftOpRightOpEquiv_counitIso_inv_app_app 📋 Mathlib.CategoryTheory.Opposites
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (X : CategoryTheory.Functor C Dᵒᵖ) (X✝ : C) : ((CategoryTheory.Functor.leftOpRightOpEquiv C D).counitIso.inv.app X).app X✝ = CategoryTheory.CategoryStruct.id (X.obj X✝)
• CategoryTheory.eqToHom_refl 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.CategoryStruct.{v₁, u₁} C] (X : C) (p : X = X) : CategoryTheory.eqToHom p = CategoryTheory.CategoryStruct.id X
• CategoryTheory.eqToHom_heq_id_cod 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X Y : C) (h : X = Y) : CategoryTheory.eqToHom h ≍ CategoryTheory.CategoryStruct.id Y
• CategoryTheory.eqToHom_heq_id_dom 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X Y : C) (h : X = Y) : CategoryTheory.eqToHom h ≍ CategoryTheory.CategoryStruct.id X
• CategoryTheory.Functor.const_obj_map 📋 Mathlib.CategoryTheory.Functor.Const
  (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] (X : C) {X✝ Y✝ : J} (x✝ : X✝ ⟶ Y✝) : ((CategoryTheory.Functor.const J).obj X).map x✝ = CategoryTheory.CategoryStruct.id X
• CategoryTheory.Functor.const_map_app 📋 Mathlib.CategoryTheory.Functor.Const
  (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {X Y : C} (f : X ⟶ Y) (x✝ : J) : ((CategoryTheory.Functor.const J).map f).app x✝ = f
• CategoryTheory.Functor.const.unop_functor_op_obj_map 📋 Mathlib.CategoryTheory.Functor.Const
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] (X : Cᵒᵖ) {j₁ j₂ : J} (f : j₁ ⟶ j₂) : (Opposite.unop ((CategoryTheory.Functor.const J).op.obj X)).map f = CategoryTheory.CategoryStruct.id (Opposite.unop X)
• CategoryTheory.Functor.constComp_inv_app 📋 Mathlib.CategoryTheory.Functor.Const
  (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] (X : C) (F : CategoryTheory.Functor C D) (x✝ : J) : (CategoryTheory.Functor.constComp J X F).inv.app x✝ = CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.const J).obj (F.obj X)).obj x✝)
• CategoryTheory.Functor.constComp_hom_app 📋 Mathlib.CategoryTheory.Functor.Const
  (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] (X : C) (F : CategoryTheory.Functor C D) (x✝ : J) : (CategoryTheory.Functor.constComp J X F).hom.app x✝ = CategoryTheory.CategoryStruct.id ((((CategoryTheory.Functor.const J).obj X).comp F).obj x✝)
• CategoryTheory.Functor.const.opObjOp_inv_app 📋 Mathlib.CategoryTheory.Functor.Const
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] (X : C) (x✝ : Jᵒᵖ) : (CategoryTheory.Functor.const.opObjOp X).inv.app x✝ = CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.const J).obj X).op.obj x✝)
• CategoryTheory.Functor.const.opObjUnop_hom_app 📋 Mathlib.CategoryTheory.Functor.Const
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] (X : Cᵒᵖ) (j : Jᵒᵖ) : (CategoryTheory.Functor.const.opObjUnop X).hom.app j = CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.const Jᵒᵖ).obj (Opposite.unop X)).obj j)
• CategoryTheory.Functor.const.opObjUnop_inv_app 📋 Mathlib.CategoryTheory.Functor.Const
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] (X : Cᵒᵖ) (j : Jᵒᵖ) : (CategoryTheory.Functor.const.opObjUnop X).inv.app j = CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.const J).obj X).leftOp.obj j)
• CategoryTheory.Functor.const.opObjOp_hom_app 📋 Mathlib.CategoryTheory.Functor.Const
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] (X : C) (x✝ : Jᵒᵖ) : (CategoryTheory.Functor.const.opObjOp X).hom.app x✝ = CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.const Jᵒᵖ).obj (Opposite.op X)).obj x✝)
• CategoryTheory.Functor.constCompWhiskeringLeftIso_hom_app_app 📋 Mathlib.CategoryTheory.Functor.Const
  (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] (F : CategoryTheory.Functor J D) (X : C) (X✝ : J) : ((CategoryTheory.Functor.constCompWhiskeringLeftIso J F).hom.app X).app X✝ = CategoryTheory.CategoryStruct.id X
• CategoryTheory.Functor.constCompWhiskeringLeftIso_inv_app_app 📋 Mathlib.CategoryTheory.Functor.Const
  (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] (F : CategoryTheory.Functor J D) (X : C) (X✝ : J) : ((CategoryTheory.Functor.constCompWhiskeringLeftIso J F).inv.app X).app X✝ = CategoryTheory.CategoryStruct.id X
• CategoryTheory.Functor.compConstIso_hom_app_app 📋 Mathlib.CategoryTheory.Functor.Const
  (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] (F : CategoryTheory.Functor C D) (X : C) (X✝ : J) : ((CategoryTheory.Functor.compConstIso J F).hom.app X).app X✝ = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.Functor.compConstIso_inv_app_app 📋 Mathlib.CategoryTheory.Functor.Const
  (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] (F : CategoryTheory.Functor C D) (X : C) (X✝ : J) : ((CategoryTheory.Functor.compConstIso J F).inv.app X).app X✝ = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.prod_id 📋 Mathlib.CategoryTheory.Products.Basic
  {C : Type u₁} [CategoryTheory.CategoryStruct.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.CategoryStruct.{v₂, u₂} D] (X : C) (Y : D) : CategoryTheory.CategoryStruct.id (X, Y) = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Y)
• CategoryTheory.prod_id_fst 📋 Mathlib.CategoryTheory.Products.Basic
  (C : Type u₁) [CategoryTheory.CategoryStruct.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.CategoryStruct.{v₂, u₂} D] (X : C × D) : (CategoryTheory.CategoryStruct.id X).1 = CategoryTheory.CategoryStruct.id X.1
• CategoryTheory.prod_id_snd 📋 Mathlib.CategoryTheory.Products.Basic
  (C : Type u₁) [CategoryTheory.CategoryStruct.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.CategoryStruct.{v₂, u₂} D] (X : C × D) : (CategoryTheory.CategoryStruct.id X).2 = CategoryTheory.CategoryStruct.id X.2
• CategoryTheory.prod_id' 📋 Mathlib.CategoryTheory.Products.Basic
  {C : Type u₁} [CategoryTheory.CategoryStruct.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.CategoryStruct.{v₂, u₂} D] (X : C) (Y : D) : CategoryTheory.CategoryStruct.id (X, Y) = (CategoryTheory.CategoryStruct.id X, CategoryTheory.CategoryStruct.id Y)
• CategoryTheory.Prod.sectL_map 📋 Mathlib.CategoryTheory.Products.Basic
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (Z : D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (CategoryTheory.Prod.sectL C Z).map f = CategoryTheory.Prod.mkHom f (CategoryTheory.CategoryStruct.id Z)
• CategoryTheory.Prod.sectR_map 📋 Mathlib.CategoryTheory.Products.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (Z : C) (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) : (CategoryTheory.Prod.sectR Z D).map f = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id Z) f
• CategoryTheory.prod.etaIso_hom 📋 Mathlib.CategoryTheory.Products.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (X : C × D) : (CategoryTheory.prod.etaIso X).hom = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.1) (CategoryTheory.CategoryStruct.id X.2)
• CategoryTheory.prod.etaIso_inv 📋 Mathlib.CategoryTheory.Products.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (X : C × D) : (CategoryTheory.prod.etaIso X).inv = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.1) (CategoryTheory.CategoryStruct.id X.2)
• CategoryTheory.Functor.prod'CompFst_hom_app 📋 Mathlib.CategoryTheory.Products.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor A C) (X : A) : (F.prod'CompFst G).hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.Functor.prod'CompFst_inv_app 📋 Mathlib.CategoryTheory.Products.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor A C) (X : A) : (F.prod'CompFst G).inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.Functor.prod'CompSnd_hom_app 📋 Mathlib.CategoryTheory.Products.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor A C) (X : A) : (F.prod'CompSnd G).hom.app X = CategoryTheory.CategoryStruct.id (G.obj X)
• CategoryTheory.Functor.prod'CompSnd_inv_app 📋 Mathlib.CategoryTheory.Products.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor A C) (X : A) : (F.prod'CompSnd G).inv.app X = CategoryTheory.CategoryStruct.id (G.obj X)
• CategoryTheory.Prod.symmetry_hom_app 📋 Mathlib.CategoryTheory.Products.Basic
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (X : C × D) : (CategoryTheory.Prod.symmetry C D).hom.app X = CategoryTheory.CategoryStruct.id X
• CategoryTheory.Prod.symmetry_inv_app 📋 Mathlib.CategoryTheory.Products.Basic
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (X : C × D) : (CategoryTheory.Prod.symmetry C D).inv.app X = CategoryTheory.CategoryStruct.id X
• CategoryTheory.Prod.fac 📋 Mathlib.CategoryTheory.Products.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {x y : C × D} (f : x ⟶ y) : f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id x.1) f.2) (CategoryTheory.Prod.mkHom f.1 (CategoryTheory.CategoryStruct.id y.2))
• CategoryTheory.Prod.fac' 📋 Mathlib.CategoryTheory.Products.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {x y : C × D} (f : x ⟶ y) : f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Prod.mkHom f.1 (CategoryTheory.CategoryStruct.id x.2)) (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id y.1) f.2)
• CategoryTheory.Functor.constCompEvaluationObj_hom_app 📋 Mathlib.CategoryTheory.Products.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (X : C) (X✝ : D) : (CategoryTheory.Functor.constCompEvaluationObj D X).hom.app X✝ = CategoryTheory.CategoryStruct.id X✝
• CategoryTheory.Functor.constCompEvaluationObj_inv_app 📋 Mathlib.CategoryTheory.Products.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (X : C) (X✝ : D) : (CategoryTheory.Functor.constCompEvaluationObj D X).inv.app X✝ = CategoryTheory.CategoryStruct.id X✝
• CategoryTheory.Prod.fac'_assoc 📋 Mathlib.CategoryTheory.Products.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {x y : C × D} (f : x ⟶ y) {Z : C × D} (h : y ⟶ Z) : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Prod.mkHom f.1 (CategoryTheory.CategoryStruct.id x.2)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id y.1) f.2) h)
• CategoryTheory.Prod.fac_assoc 📋 Mathlib.CategoryTheory.Products.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {x y : C × D} (f : x ⟶ y) {Z : C × D} (h : y ⟶ Z) : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id x.1) f.2) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Prod.mkHom f.1 (CategoryTheory.CategoryStruct.id y.2)) h)
• CategoryTheory.prodOpEquiv_unitIso_hom_app 📋 Mathlib.CategoryTheory.Products.Basic
  (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (X : (C × D)ᵒᵖ) : (CategoryTheory.prodOpEquiv C).unitIso.hom.app X = CategoryTheory.CategoryStruct.id X
• CategoryTheory.prodOpEquiv_unitIso_inv_app 📋 Mathlib.CategoryTheory.Products.Basic
  (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (X : (C × D)ᵒᵖ) : (CategoryTheory.prodOpEquiv C).unitIso.inv.app X = CategoryTheory.CategoryStruct.id X
• CategoryTheory.compEvaluation_hom_app 📋 Mathlib.CategoryTheory.Products.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A (CategoryTheory.Functor B C)) (b : B) (X : A) : (CategoryTheory.compEvaluation F b).hom.app X = CategoryTheory.CategoryStruct.id ((F.obj X).obj b)
• CategoryTheory.compEvaluation_inv_app 📋 Mathlib.CategoryTheory.Products.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A (CategoryTheory.Functor B C)) (b : B) (X : A) : (CategoryTheory.compEvaluation F b).inv.app X = CategoryTheory.CategoryStruct.id ((F.obj X).obj b)
• CategoryTheory.flipCompEvaluation_hom_app 📋 Mathlib.CategoryTheory.Products.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A (CategoryTheory.Functor B C)) (a : A) (X : B) : (CategoryTheory.flipCompEvaluation F a).hom.app X = CategoryTheory.CategoryStruct.id ((F.obj a).obj X)
• CategoryTheory.flipCompEvaluation_inv_app 📋 Mathlib.CategoryTheory.Products.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A (CategoryTheory.Functor B C)) (a : A) (X : B) : (CategoryTheory.flipCompEvaluation F a).inv.app X = CategoryTheory.CategoryStruct.id ((F.obj a).obj X)
• CategoryTheory.whiskeringLeftCompEvaluation_hom_app 📋 Mathlib.CategoryTheory.Products.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (a : A) (X : CategoryTheory.Functor B C) : (CategoryTheory.whiskeringLeftCompEvaluation F a).hom.app X = CategoryTheory.CategoryStruct.id (X.obj (F.obj a))
• CategoryTheory.whiskeringLeftCompEvaluation_inv_app 📋 Mathlib.CategoryTheory.Products.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B) (a : A) (X : CategoryTheory.Functor B C) : (CategoryTheory.whiskeringLeftCompEvaluation F a).inv.app X = CategoryTheory.CategoryStruct.id (X.obj (F.obj a))
• CategoryTheory.whiskeringRightCompEvaluation_hom_app 📋 Mathlib.CategoryTheory.Products.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor B C) (a : A) (X : CategoryTheory.Functor A B) : (CategoryTheory.whiskeringRightCompEvaluation F a).hom.app X = CategoryTheory.CategoryStruct.id (F.obj (X.obj a))
• CategoryTheory.whiskeringRightCompEvaluation_inv_app 📋 Mathlib.CategoryTheory.Products.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor B C) (a : A) (X : CategoryTheory.Functor A B) : (CategoryTheory.whiskeringRightCompEvaluation F a).inv.app X = CategoryTheory.CategoryStruct.id (F.obj (X.obj a))
• CategoryTheory.functorProdFunctorEquivCounitIso_hom_app_app 📋 Mathlib.CategoryTheory.Products.Basic
  (A : Type u₁) [CategoryTheory.Category.{v₁, u₁} A] (B : Type u₂) [CategoryTheory.Category.{v₂, u₂} B] (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] (X : CategoryTheory.Functor A (B × C)) (X✝ : A) : ((CategoryTheory.functorProdFunctorEquivCounitIso A B C).hom.app X).app X✝ = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (X.obj X✝).1) (CategoryTheory.CategoryStruct.id (X.obj X✝).2)
• CategoryTheory.functorProdFunctorEquivCounitIso_inv_app_app 📋 Mathlib.CategoryTheory.Products.Basic
  (A : Type u₁) [CategoryTheory.Category.{v₁, u₁} A] (B : Type u₂) [CategoryTheory.Category.{v₂, u₂} B] (C : Type u₃) [CategoryTheory.Category.{v₃, u₃} C] (X : CategoryTheory.Functor A (B × C)) (X✝ : A) : ((CategoryTheory.functorProdFunctorEquivCounitIso A B C).inv.app X).app X✝ = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (X.obj X✝).1) (CategoryTheory.CategoryStruct.id (X.obj X✝).2)

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