Loogle!

Result

Found 1373 declarations mentioning CategoryTheory.Equivalence.functor. Of these, only the first 200 are shown.

• CategoryTheory.Equivalence.functor 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (self : C ≌ D) : CategoryTheory.Functor C D
• CategoryTheory.Equivalence.refl_functor 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] : CategoryTheory.Equivalence.refl.functor = CategoryTheory.Functor.id C
• CategoryTheory.Equivalence.essSurj_functor 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ E) : e.functor.EssSurj
• CategoryTheory.Equivalence.faithful_functor 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ E) : e.functor.Faithful
• CategoryTheory.Equivalence.full_functor 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ E) : e.functor.Full
• CategoryTheory.Equivalence.fullyFaithfulFunctor 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ E) : e.functor.FullyFaithful
• CategoryTheory.Equivalence.isEquivalence_functor 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : C ≌ D) : F.functor.IsEquivalence
• CategoryTheory.Equivalence.symm_functor 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : e.symm.functor = e.inverse
• CategoryTheory.Equivalence.symm_inverse 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : e.symm.inverse = e.functor
• CategoryTheory.Functor.asEquivalence_functor 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.IsEquivalence] : F.asEquivalence.functor = F
• CategoryTheory.Equivalence.changeFunctor 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {G : CategoryTheory.Functor C D} (iso : e.functor ≅ G) : C ≌ D
• CategoryTheory.Equivalence.counitIso 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (self : C ≌ D) : self.inverse.comp self.functor ≅ CategoryTheory.Functor.id D
• CategoryTheory.Equivalence.unitIso 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (self : C ≌ D) : CategoryTheory.Functor.id C ≅ self.functor.comp self.inverse
• CategoryTheory.Equivalence.changeFunctor_refl 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : e.changeFunctor (CategoryTheory.Iso.refl e.functor) = e
• CategoryTheory.Equivalence.functorFunctor_obj 📋 Mathlib.CategoryTheory.Equivalence
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (f : C ≌ D) : (CategoryTheory.Equivalence.functorFunctor C D).obj f = f.functor
• CategoryTheory.Equivalence.mkIso 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {e f : C ≌ D} (η : e.functor ≅ f.functor) : e ≅ f
• CategoryTheory.Equivalence.changeFunctor_functor 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {G : CategoryTheory.Functor C D} (iso : e.functor ≅ G) : (e.changeFunctor iso).functor = G
• CategoryTheory.Equivalence.counit 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : e.inverse.comp e.functor ⟶ CategoryTheory.Functor.id D
• CategoryTheory.Equivalence.counitInv 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : CategoryTheory.Functor.id D ⟶ e.inverse.comp e.functor
• CategoryTheory.Equivalence.unit 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : CategoryTheory.Functor.id C ⟶ e.functor.comp e.inverse
• CategoryTheory.Equivalence.unitInv 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : e.functor.comp e.inverse ⟶ CategoryTheory.Functor.id C
• CategoryTheory.Equivalence.funInvIdAssoc 📋 Mathlib.CategoryTheory.Equivalence
  {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 : C ≌ D) (F : CategoryTheory.Functor C E) : e.functor.comp (e.inverse.comp F) ≅ F
• CategoryTheory.Equivalence.invFunIdAssoc 📋 Mathlib.CategoryTheory.Equivalence
  {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 : C ≌ D) (F : CategoryTheory.Functor D E) : e.inverse.comp (e.functor.comp F) ≅ F
• CategoryTheory.Equivalence.trans_functor 📋 Mathlib.CategoryTheory.Equivalence
  {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 : C ≌ D) (f : D ≌ E) : (e.trans f).functor = e.functor.comp f.functor
• CategoryTheory.Equivalence.changeFunctor_inverse 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {G : CategoryTheory.Functor C D} (iso : e.functor ≅ G) : (e.changeFunctor iso).inverse = e.inverse
• CategoryTheory.Equivalence.changeInverse_functor 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {G : CategoryTheory.Functor D C} (iso : e.inverse ≅ G) : (e.changeInverse iso).functor = e.functor
• CategoryTheory.Iso.isoFunctorOfIsoInverse 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G G' : C ≌ D} (i : G.inverse ≅ G'.inverse) : G.functor ≅ G'.functor
• CategoryTheory.Iso.isoInverseOfIsoFunctor 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G G' : C ≌ D} (i : G.functor ≅ G'.functor) : G.inverse ≅ G'.inverse
• CategoryTheory.ObjectProperty.fullSubcategoryCongr_functor 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P P' : CategoryTheory.ObjectProperty C} (h : P = P') : (CategoryTheory.ObjectProperty.fullSubcategoryCongr h).functor = CategoryTheory.ObjectProperty.ιOfLE ⋯
• CategoryTheory.Equivalence.asNatTrans 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {e f : C ≌ D} (η : e ⟶ f) : e.functor ⟶ f.functor
• CategoryTheory.Equivalence.mkHom 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {e f : C ≌ D} (η : e.functor ⟶ f.functor) : e ⟶ f
• CategoryTheory.Iso.compInverseIso 📋 Mathlib.CategoryTheory.Equivalence
  {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 E} {G : CategoryTheory.Functor C D} {H : D ≌ E} (i : F ≅ G.comp H.functor) : F.comp H.inverse ≅ G
• CategoryTheory.Iso.inverseCompIso 📋 Mathlib.CategoryTheory.Equivalence
  {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 E} {H : CategoryTheory.Functor D E} {G : C ≌ D} (i : F ≅ G.functor.comp H) : G.inverse.comp F ≅ H
• CategoryTheory.Iso.isoCompInverse 📋 Mathlib.CategoryTheory.Equivalence
  {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 E} {G : CategoryTheory.Functor C D} {H : D ≌ E} (i : G.comp H.functor ≅ F) : G ≅ F.comp H.inverse
• CategoryTheory.Iso.isoInverseComp 📋 Mathlib.CategoryTheory.Equivalence
  {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 E} {H : CategoryTheory.Functor D E} {G : C ≌ D} (i : G.functor.comp H ≅ F) : H ≅ G.inverse.comp F
• CategoryTheory.Iso.isoFunctorOfIsoInverse_isoInverseOfIsoFunctor 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G G' : C ≌ D} (i : G.functor ≅ G'.functor) : i.isoInverseOfIsoFunctor.isoFunctorOfIsoInverse = i
• CategoryTheory.Equivalence.symm_counit 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : e.symm.counit = e.unitInv
• CategoryTheory.Equivalence.symm_unit 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : e.symm.unit = e.counitInv
• 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.asNatTrans_mkHom 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {e f : C ≌ D} (η : e ⟶ f) : CategoryTheory.Equivalence.asNatTrans (CategoryTheory.Equivalence.mkHom η) = η
• CategoryTheory.Equivalence.mkHom_asNatTrans 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {e f : C ≌ D} (η : e.functor ⟶ f.functor) : CategoryTheory.Equivalence.mkHom (CategoryTheory.Equivalence.asNatTrans η) = η
• 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.symm_counitIso 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : e.symm.counitIso = e.unitIso.symm
• CategoryTheory.Equivalence.symm_unitIso 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : e.symm.unitIso = e.counitIso.symm
• CategoryTheory.Equivalence.changeFunctor_trans 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {G G' : CategoryTheory.Functor C D} (iso₁ : e.functor ≅ G) (iso₂ : G ≅ G') : (e.changeFunctor iso₁).changeFunctor iso₂ = e.changeFunctor (iso₁ ≪≫ iso₂)
• CategoryTheory.Equivalence.functorFunctor_map 📋 Mathlib.CategoryTheory.Equivalence
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] {X✝ Y✝ : C ≌ D} (α : X✝ ⟶ Y✝) : (CategoryTheory.Equivalence.functorFunctor C D).map α = CategoryTheory.Equivalence.asNatTrans α
• CategoryTheory.Equivalence.mkIso_hom 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {e f : C ≌ D} (η : e.functor ≅ f.functor) : (CategoryTheory.Equivalence.mkIso η).hom = CategoryTheory.Equivalence.mkHom η.hom
• CategoryTheory.Equivalence.mkIso_inv 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {e f : C ≌ D} (η : e.functor ≅ f.functor) : (CategoryTheory.Equivalence.mkIso η).inv = CategoryTheory.Equivalence.mkHom η.inv
• 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.congrLeft_functor 📋 Mathlib.CategoryTheory.Equivalence
  {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 : C ≌ D) : e.congrLeft.functor = (CategoryTheory.Functor.whiskeringLeft D C E).obj e.inverse
• CategoryTheory.Equivalence.congrLeft_inverse 📋 Mathlib.CategoryTheory.Equivalence
  {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 : C ≌ D) : e.congrLeft.inverse = (CategoryTheory.Functor.whiskeringLeft C D E).obj e.functor
• CategoryTheory.Equivalence.congrRight_functor 📋 Mathlib.CategoryTheory.Equivalence
  {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 : C ≌ D) : e.congrRight.functor = (CategoryTheory.Functor.whiskeringRight E C D).obj e.functor
• CategoryTheory.Equivalence.hom_ext 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {e f : C ≌ D} {α β : e ⟶ f} (h : CategoryTheory.Equivalence.asNatTrans α = CategoryTheory.Equivalence.asNatTrans β) : α = β
• CategoryTheory.Equivalence.hom_ext_iff 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {e f : C ≌ D} {α β : e ⟶ f} : α = β ↔ CategoryTheory.Equivalence.asNatTrans α = CategoryTheory.Equivalence.asNatTrans β
• CategoryTheory.Equivalence.counitIso_inv_hom_id_app_assoc 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (Y : D) {Z : D} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.counitInv.app Y) (CategoryTheory.CategoryStruct.comp (e.counit.app Y) h) = h
• CategoryTheory.Equivalence.unitIso_hom_inv_id_app_assoc 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X : C) {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.unit.app X) (CategoryTheory.CategoryStruct.comp (e.unitInv.app X) h) = h
• CategoryTheory.Equivalence.comp_asNatTrans 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {e f g : C ≌ D} (α : e ⟶ f) (β : f ⟶ g) : CategoryTheory.Equivalence.asNatTrans (CategoryTheory.CategoryStruct.comp α β) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Equivalence.asNatTrans α) (CategoryTheory.Equivalence.asNatTrans β)
• CategoryTheory.Equivalence.mkHom_comp 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {e f g : C ≌ D} (α : e.functor ⟶ f.functor) (β : f.functor ⟶ g.functor) : CategoryTheory.Equivalence.mkHom (CategoryTheory.CategoryStruct.comp α β) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Equivalence.mkHom α) (CategoryTheory.Equivalence.mkHom β)
• CategoryTheory.Equivalence.counitInv_app_functor 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X : C) : e.counitInv.app (e.functor.obj X) = e.functor.map (e.unit.app X)
• CategoryTheory.Equivalence.counit_app_functor 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X : C) : e.counit.app (e.functor.obj X) = e.functor.map (e.unitInv.app X)
• CategoryTheory.Equivalence.unitInv_app_inverse 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (Y : D) : e.unitInv.app (e.inverse.obj Y) = e.inverse.map (e.counit.app Y)
• CategoryTheory.Equivalence.unit_app_inverse 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (Y : D) : e.unit.app (e.inverse.obj Y) = e.inverse.map (e.counitInv.app Y)
• CategoryTheory.Equivalence.counitIso_hom_inv_id_app_assoc 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (Y : D) {Z : D} (h : e.functor.obj (e.inverse.obj Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.counit.app Y) (CategoryTheory.CategoryStruct.comp (e.counitInv.app Y) h) = h
• CategoryTheory.Equivalence.unitIso_inv_hom_id_app_assoc 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X : C) {Z : C} (h : e.inverse.obj (e.functor.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.unitInv.app X) (CategoryTheory.CategoryStruct.comp (e.unit.app X) h) = h
• CategoryTheory.Equivalence.cancel_counitInv_right 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {X Y : D} (f f' : X ⟶ Y) : CategoryTheory.CategoryStruct.comp f (e.counitInv.app Y) = CategoryTheory.CategoryStruct.comp f' (e.counitInv.app Y) ↔ f = f'
• CategoryTheory.Equivalence.cancel_counit_left 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {X Y : D} (f f' : Y ⟶ X) : CategoryTheory.CategoryStruct.comp (e.counit.app Y) f = CategoryTheory.CategoryStruct.comp (e.counit.app Y) f' ↔ f = f'
• CategoryTheory.Equivalence.cancel_unitInv_left 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {X Y : C} (f f' : Y ⟶ X) : CategoryTheory.CategoryStruct.comp (e.unitInv.app Y) f = CategoryTheory.CategoryStruct.comp (e.unitInv.app Y) f' ↔ f = f'
• CategoryTheory.Equivalence.cancel_unit_right 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {X Y : C} (f f' : X ⟶ Y) : CategoryTheory.CategoryStruct.comp f (e.unit.app Y) = CategoryTheory.CategoryStruct.comp f' (e.unit.app Y) ↔ f = f'
• 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.ext 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} {D : Type u₂} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.Category.{v₂, u₂} D} {x y : C ≌ D} (functor : x.functor = y.functor) (inverse : x.inverse = y.inverse) (unitIso : x.unitIso ≍ y.unitIso) (counitIso : x.counitIso ≍ y.counitIso) : x = y
• CategoryTheory.Equivalence.ext_iff 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} {D : Type u₂} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.Category.{v₂, u₂} D} {x y : C ≌ D} : x = y ↔ x.functor = y.functor ∧ x.inverse = y.inverse ∧ x.unitIso ≍ y.unitIso ∧ x.counitIso ≍ y.counitIso
• CategoryTheory.Equivalence.funInvIdAssoc_hom_app 📋 Mathlib.CategoryTheory.Equivalence
  {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 : C ≌ D) (F : CategoryTheory.Functor C E) (X : C) : (e.funInvIdAssoc F).hom.app X = F.map (e.unitInv.app X)
• CategoryTheory.Equivalence.funInvIdAssoc_inv_app 📋 Mathlib.CategoryTheory.Equivalence
  {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 : C ≌ D) (F : CategoryTheory.Functor C E) (X : C) : (e.funInvIdAssoc F).inv.app X = F.map (e.unit.app X)
• CategoryTheory.Equivalence.invFunIdAssoc_hom_app 📋 Mathlib.CategoryTheory.Equivalence
  {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 : C ≌ D) (F : CategoryTheory.Functor D E) (X : D) : (e.invFunIdAssoc F).hom.app X = F.map (e.counit.app X)
• CategoryTheory.Equivalence.invFunIdAssoc_inv_app 📋 Mathlib.CategoryTheory.Equivalence
  {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 : C ≌ D) (F : CategoryTheory.Functor D E) (X : D) : (e.invFunIdAssoc F).inv.app X = F.map (e.counitInv.app 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.counitInv_naturality 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {X Y : D} (f : Y ⟶ X) : CategoryTheory.CategoryStruct.comp (e.counitInv.app Y) (e.functor.map (e.inverse.map f)) = CategoryTheory.CategoryStruct.comp f (e.counitInv.app X)
• CategoryTheory.Equivalence.counit_naturality 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {X Y : D} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (e.functor.map (e.inverse.map f)) (e.counit.app Y) = CategoryTheory.CategoryStruct.comp (e.counit.app X) f
• CategoryTheory.Equivalence.unitInv_naturality 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {X Y : C} (f : Y ⟶ X) : CategoryTheory.CategoryStruct.comp (e.inverse.map (e.functor.map f)) (e.unitInv.app X) = CategoryTheory.CategoryStruct.comp (e.unitInv.app Y) f
• CategoryTheory.Equivalence.unit_naturality 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {X Y : C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (e.unit.app X) (e.inverse.map (e.functor.map f)) = CategoryTheory.CategoryStruct.comp f (e.unit.app Y)
• CategoryTheory.Equivalence.mkHom_comp_assoc 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {e f g : C ≌ D} (α : e.functor ⟶ f.functor) (β : f.functor ⟶ g.functor) {Z : C ≌ D} (h : g ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Equivalence.mkHom (CategoryTheory.CategoryStruct.comp α β)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Equivalence.mkHom α) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Equivalence.mkHom β) h)
• CategoryTheory.Equivalence.cancel_counitInv_left 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {X Y : D} (f f' : e.functor.obj (e.inverse.obj Y) ⟶ X) : CategoryTheory.CategoryStruct.comp (e.counitInv.app Y) f = CategoryTheory.CategoryStruct.comp (e.counitInv.app Y) f' ↔ f = f'
• CategoryTheory.Equivalence.cancel_counit_right 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {X Y : D} (f f' : X ⟶ e.functor.obj (e.inverse.obj Y)) : CategoryTheory.CategoryStruct.comp f (e.counit.app Y) = CategoryTheory.CategoryStruct.comp f' (e.counit.app Y) ↔ f = f'
• CategoryTheory.Equivalence.cancel_unitInv_right 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {X Y : C} (f f' : X ⟶ e.inverse.obj (e.functor.obj Y)) : CategoryTheory.CategoryStruct.comp f (e.unitInv.app Y) = CategoryTheory.CategoryStruct.comp f' (e.unitInv.app Y) ↔ f = f'
• CategoryTheory.Equivalence.cancel_unit_left 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {X Y : C} (f f' : e.inverse.obj (e.functor.obj Y) ⟶ X) : CategoryTheory.CategoryStruct.comp (e.unit.app Y) f = CategoryTheory.CategoryStruct.comp (e.unit.app Y) f' ↔ f = f'
• CategoryTheory.Equivalence.comp_asNatTrans_assoc 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {e f g : C ≌ D} (α : e ⟶ f) (β : f ⟶ g) {Z : CategoryTheory.Functor C D} (h : g.functor ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Equivalence.asNatTrans (CategoryTheory.CategoryStruct.comp α β)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Equivalence.asNatTrans α) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Equivalence.asNatTrans β) h)
• CategoryTheory.Equivalence.counitInv_functor_comp_assoc 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X : C) {Z : D} (h : e.functor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.counitInv.app (e.functor.obj X)) (CategoryTheory.CategoryStruct.comp (e.functor.map (e.unitInv.app X)) h) = h
• CategoryTheory.Equivalence.functor_unit_comp_assoc 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X : C) {Z : D} (h : e.functor.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.functor.map (e.unit.app X)) (CategoryTheory.CategoryStruct.comp (e.counit.app (e.functor.obj X)) h) = h
• CategoryTheory.Equivalence.inverse_counitInv_comp_assoc 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (Y : D) {Z : C} (h : e.inverse.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.inverse.map (e.counitInv.app Y)) (CategoryTheory.CategoryStruct.comp (e.unitInv.app (e.inverse.obj Y)) h) = h
• CategoryTheory.Equivalence.unit_inverse_comp_assoc 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (Y : D) {Z : C} (h : e.inverse.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.unit.app (e.inverse.obj Y)) (CategoryTheory.CategoryStruct.comp (e.inverse.map (e.counit.app Y)) h) = h
• CategoryTheory.Equivalence.changeFunctor_counitIso_hom_app 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {G : CategoryTheory.Functor C D} (iso : e.functor ≅ G) (X : D) : (e.changeFunctor iso).counitIso.hom.app X = CategoryTheory.CategoryStruct.comp (iso.inv.app (e.inverse.obj X)) (e.counitIso.hom.app X)
• CategoryTheory.Equivalence.changeFunctor_counitIso_inv_app 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {G : CategoryTheory.Functor C D} (iso : e.functor ≅ G) (X : D) : (e.changeFunctor iso).counitIso.inv.app X = CategoryTheory.CategoryStruct.comp (e.counitIso.inv.app X) (iso.hom.app (e.inverse.obj X))
• CategoryTheory.Equivalence.changeInverse_unitIso_hom_app 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {G : CategoryTheory.Functor D C} (iso : e.inverse ≅ G) (X : C) : (e.changeInverse iso).unitIso.hom.app X = CategoryTheory.CategoryStruct.comp (e.unitIso.hom.app X) (iso.hom.app (e.functor.obj X))
• CategoryTheory.Equivalence.changeInverse_unitIso_inv_app 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {G : CategoryTheory.Functor D C} (iso : e.inverse ≅ G) (X : C) : (e.changeInverse iso).unitIso.inv.app X = CategoryTheory.CategoryStruct.comp (iso.inv.app (e.functor.obj X)) (e.unitIso.inv.app X)
• CategoryTheory.Equivalence.fun_inv_map 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X Y : D) (f : X ⟶ Y) : e.functor.map (e.inverse.map f) = CategoryTheory.CategoryStruct.comp (e.counit.app X) (CategoryTheory.CategoryStruct.comp f (e.counitInv.app Y))
• CategoryTheory.Equivalence.inv_fun_map 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X Y : C) (f : X ⟶ Y) : e.inverse.map (e.functor.map f) = CategoryTheory.CategoryStruct.comp (e.unitInv.app X) (CategoryTheory.CategoryStruct.comp f (e.unit.app Y))
• CategoryTheory.Equivalence.counitInv_naturality_assoc 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {X Y : D} (f : Y ⟶ X) {Z : D} (h : e.functor.obj (e.inverse.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.counitInv.app Y) (CategoryTheory.CategoryStruct.comp (e.functor.map (e.inverse.map f)) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (e.counitInv.app X) h)
• 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.counit_naturality_assoc 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {X Y : D} (f : X ⟶ Y) {Z : D} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.functor.map (e.inverse.map f)) (CategoryTheory.CategoryStruct.comp (e.counit.app Y) h) = CategoryTheory.CategoryStruct.comp (e.counit.app X) (CategoryTheory.CategoryStruct.comp f h)
• 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.unitInv_naturality_assoc 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {X Y : C} (f : Y ⟶ X) {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.inverse.map (e.functor.map f)) (CategoryTheory.CategoryStruct.comp (e.unitInv.app X) h) = CategoryTheory.CategoryStruct.comp (e.unitInv.app Y) (CategoryTheory.CategoryStruct.comp f h)
• CategoryTheory.Equivalence.unit_naturality_assoc 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {X Y : C} (f : X ⟶ Y) {Z : C} (h : e.inverse.obj (e.functor.obj Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.unit.app X) (CategoryTheory.CategoryStruct.comp (e.inverse.map (e.functor.map f)) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (e.unit.app Y) h)
• CategoryTheory.Equivalence.changeFunctor_unitIso_hom_app 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {G : CategoryTheory.Functor C D} (iso : e.functor ≅ G) (X : C) : (e.changeFunctor iso).unitIso.hom.app X = CategoryTheory.CategoryStruct.comp (e.unitIso.hom.app X) (e.inverse.map (iso.hom.app X))
• CategoryTheory.Equivalence.changeFunctor_unitIso_inv_app 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {G : CategoryTheory.Functor C D} (iso : e.functor ≅ G) (X : C) : (e.changeFunctor iso).unitIso.inv.app X = CategoryTheory.CategoryStruct.comp (e.inverse.map (iso.inv.app X)) (e.unitIso.inv.app X)
• CategoryTheory.Equivalence.changeInverse_counitIso_hom_app 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {G : CategoryTheory.Functor D C} (iso : e.inverse ≅ G) (X : D) : (e.changeInverse iso).counitIso.hom.app X = CategoryTheory.CategoryStruct.comp (e.functor.map (iso.inv.app X)) (e.counitIso.hom.app X)
• CategoryTheory.Equivalence.changeInverse_counitIso_inv_app 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {G : CategoryTheory.Functor D C} (iso : e.inverse ≅ G) (X : D) : (e.changeInverse iso).counitIso.inv.app X = CategoryTheory.CategoryStruct.comp (e.counitIso.inv.app X) (e.functor.map (iso.hom.app X))
• CategoryTheory.Equivalence.cancel_counitInv_right_assoc 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {W X X' Y : D} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X') (g' : X' ⟶ Y) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g (e.counitInv.app Y)) = CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g' (e.counitInv.app Y)) ↔ CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f' g'
• CategoryTheory.Equivalence.cancel_unit_right_assoc 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {W X X' Y : C} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X') (g' : X' ⟶ Y) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g (e.unit.app Y)) = CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g' (e.unit.app Y)) ↔ CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f' g'
• CategoryTheory.Equivalence.fun_inv_map_assoc 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X Y : D) (f : X ⟶ Y) {Z : D} (h : e.functor.obj (e.inverse.obj Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.functor.map (e.inverse.map f)) h = CategoryTheory.CategoryStruct.comp (e.counit.app X) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (e.counitInv.app Y) h))
• CategoryTheory.Equivalence.inv_fun_map_assoc 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X Y : C) (f : X ⟶ Y) {Z : C} (h : e.inverse.obj (e.functor.obj Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp (e.inverse.map (e.functor.map f)) h = CategoryTheory.CategoryStruct.comp (e.unitInv.app X) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (e.unit.app Y) h))
• CategoryTheory.Equivalence.congrRightFunctor_map 📋 Mathlib.CategoryTheory.Equivalence
  {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 f : C ≌ D} (α : e ⟶ f) : (CategoryTheory.Equivalence.congrRightFunctor E).map α = CategoryTheory.Equivalence.mkHom ((CategoryTheory.Functor.whiskeringRight E C D).map (CategoryTheory.Equivalence.asNatTrans α))
• 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.Functor.inv_fun_map 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.IsEquivalence] (X Y : C) (f : X ⟶ Y) : F.inv.map (F.map f) = CategoryTheory.CategoryStruct.comp (F.asEquivalence.unitInv.app X) (CategoryTheory.CategoryStruct.comp f (F.asEquivalence.unit.app Y))
• CategoryTheory.Iso.inverseCompIso_hom_app 📋 Mathlib.CategoryTheory.Equivalence
  {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 E} {H : CategoryTheory.Functor D E} {G : C ≌ D} (i : F ≅ G.functor.comp H) (X : D) : i.inverseCompIso.hom.app X = CategoryTheory.CategoryStruct.comp (i.hom.app (G.inverse.obj X)) (H.map (G.counitIso.hom.app X))
• CategoryTheory.Iso.inverseCompIso_inv_app 📋 Mathlib.CategoryTheory.Equivalence
  {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 E} {H : CategoryTheory.Functor D E} {G : C ≌ D} (i : F ≅ G.functor.comp H) (X : D) : i.inverseCompIso.inv.app X = CategoryTheory.CategoryStruct.comp (H.map (G.counitIso.inv.app X)) (i.inv.app (G.inverse.obj X))
• CategoryTheory.Iso.isoInverseComp_hom_app 📋 Mathlib.CategoryTheory.Equivalence
  {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 E} {H : CategoryTheory.Functor D E} {G : C ≌ D} (i : G.functor.comp H ≅ F) (X : D) : i.isoInverseComp.hom.app X = CategoryTheory.CategoryStruct.comp (H.map (G.counitIso.inv.app X)) (i.hom.app (G.inverse.obj X))
• CategoryTheory.Iso.isoInverseComp_inv_app 📋 Mathlib.CategoryTheory.Equivalence
  {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 E} {H : CategoryTheory.Functor D E} {G : C ≌ D} (i : G.functor.comp H ≅ F) (X : D) : i.isoInverseComp.inv.app X = CategoryTheory.CategoryStruct.comp (i.inv.app (G.inverse.obj X)) (H.map (G.counitIso.hom.app X))
• CategoryTheory.Iso.compInverseIso_hom_app 📋 Mathlib.CategoryTheory.Equivalence
  {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 E} {G : CategoryTheory.Functor C D} {H : D ≌ E} (i : F ≅ G.comp H.functor) (X : C) : i.compInverseIso.hom.app X = CategoryTheory.CategoryStruct.comp (H.inverse.map (i.hom.app X)) (H.unitIso.inv.app (G.obj X))
• CategoryTheory.Iso.compInverseIso_inv_app 📋 Mathlib.CategoryTheory.Equivalence
  {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 E} {G : CategoryTheory.Functor C D} {H : D ≌ E} (i : F ≅ G.comp H.functor) (X : C) : i.compInverseIso.inv.app X = CategoryTheory.CategoryStruct.comp (H.unitIso.hom.app (G.obj X)) (H.inverse.map (i.inv.app X))
• CategoryTheory.Iso.isoCompInverse_hom_app 📋 Mathlib.CategoryTheory.Equivalence
  {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 E} {G : CategoryTheory.Functor C D} {H : D ≌ E} (i : G.comp H.functor ≅ F) (X : C) : i.isoCompInverse.hom.app X = CategoryTheory.CategoryStruct.comp (H.unitIso.hom.app (G.obj X)) (H.inverse.map (i.hom.app X))
• CategoryTheory.Iso.isoCompInverse_inv_app 📋 Mathlib.CategoryTheory.Equivalence
  {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 E} {G : CategoryTheory.Functor C D} {H : D ≌ E} (i : G.comp H.functor ≅ F) (X : C) : i.isoCompInverse.inv.app X = CategoryTheory.CategoryStruct.comp (H.inverse.map (i.inv.app X)) (H.unitIso.inv.app (G.obj X))
• CategoryTheory.Functor.fun_inv_map 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.IsEquivalence] (X Y : D) (f : X ⟶ Y) : F.map (F.inv.map f) = CategoryTheory.CategoryStruct.comp (F.asEquivalence.counit.app X) (CategoryTheory.CategoryStruct.comp f (F.asEquivalence.counitInv.app Y))
• CategoryTheory.Equivalence.cancel_counitInv_right_assoc' 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {W X X' Y Y' Z : D} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z) (f' : W ⟶ X') (g' : X' ⟶ Y') (h' : Y' ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp h (e.counitInv.app Z))) = CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g' (CategoryTheory.CategoryStruct.comp h' (e.counitInv.app Z))) ↔ CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g' h')
• CategoryTheory.Equivalence.cancel_unit_right_assoc' 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) {W X X' Y Y' Z : C} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z) (f' : W ⟶ X') (g' : X' ⟶ Y') (h' : Y' ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp h (e.unit.app Z))) = CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g' (CategoryTheory.CategoryStruct.comp h' (e.unit.app Z))) ↔ CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g' h')
• CategoryTheory.Iso.isoInverseOfIsoFunctor_hom_app 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G G' : C ≌ D} (i : G.functor ≅ G'.functor) (X : D) : i.isoInverseOfIsoFunctor.hom.app X = CategoryTheory.CategoryStruct.comp (G'.unitIso.hom.app (G.inverse.obj X)) (CategoryTheory.CategoryStruct.comp (G'.inverse.map (i.inv.app (G.inverse.obj X))) (G'.inverse.map (G.counitIso.hom.app X)))
• CategoryTheory.Iso.isoInverseOfIsoFunctor_inv_app 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G G' : C ≌ D} (i : G.functor ≅ G'.functor) (X : D) : i.isoInverseOfIsoFunctor.inv.app X = CategoryTheory.CategoryStruct.comp (G'.inverse.map (G.counitIso.inv.app X)) (CategoryTheory.CategoryStruct.comp (G'.inverse.map (i.hom.app (G.inverse.obj X))) (G'.unitIso.inv.app (G.inverse.obj X)))
• CategoryTheory.Iso.isoFunctorOfIsoInverse_hom_app 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G G' : C ≌ D} (i : G.inverse ≅ G'.inverse) (X : C) : i.isoFunctorOfIsoInverse.hom.app X = CategoryTheory.CategoryStruct.comp (G'.counitIso.inv.app (G.functor.obj X)) (CategoryTheory.CategoryStruct.comp (G'.functor.map (i.inv.app (G.functor.obj X))) (G'.functor.map (G.unitIso.inv.app X)))
• CategoryTheory.Iso.isoFunctorOfIsoInverse_inv_app 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {G G' : C ≌ D} (i : G.inverse ≅ G'.inverse) (X : C) : i.isoFunctorOfIsoInverse.inv.app X = CategoryTheory.CategoryStruct.comp (G'.functor.map (G.unitIso.hom.app X)) (CategoryTheory.CategoryStruct.comp (G'.functor.map (i.hom.app (G.functor.obj X))) (G'.counitIso.hom.app (G.functor.obj X)))
• CategoryTheory.Equivalence.trans_counitIso 📋 Mathlib.CategoryTheory.Equivalence
  {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 : C ≌ D) (f : D ≌ E) : (e.trans f).counitIso = ((f.inverse.comp e.inverse).associator e.functor f.functor).symm ≪≫ CategoryTheory.Functor.isoWhiskerRight (f.inverse.associator e.inverse e.functor ≪≫ f.inverse.isoWhiskerLeft e.counitIso ≪≫ f.inverse.rightUnitor) f.functor ≪≫ f.counitIso
• CategoryTheory.Equivalence.trans_unitIso 📋 Mathlib.CategoryTheory.Equivalence
  {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 : C ≌ D) (f : D ≌ E) : (e.trans f).unitIso = e.unitIso ≪≫ CategoryTheory.Functor.isoWhiskerRight (e.functor.rightUnitor.symm ≪≫ e.functor.isoWhiskerLeft f.unitIso ≪≫ (e.functor.associator f.functor f.inverse).symm) e.inverse ≪≫ (e.functor.comp f.functor).associator f.inverse e.inverse
• CategoryTheory.Equivalence.congrLeft_counitIso_hom_app 📋 Mathlib.CategoryTheory.Equivalence
  {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 : C ≌ D) (X : CategoryTheory.Functor D E) : e.congrLeft.counitIso.hom.app X = (e.invFunIdAssoc X).hom
• CategoryTheory.Equivalence.congrLeft_counitIso_inv_app 📋 Mathlib.CategoryTheory.Equivalence
  {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 : C ≌ D) (X : CategoryTheory.Functor D E) : e.congrLeft.counitIso.inv.app X = (e.invFunIdAssoc X).inv
• CategoryTheory.Equivalence.congrLeft_unitIso_hom_app 📋 Mathlib.CategoryTheory.Equivalence
  {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 : C ≌ D) (X : CategoryTheory.Functor C E) : e.congrLeft.unitIso.hom.app X = (e.funInvIdAssoc X).inv
• CategoryTheory.Equivalence.congrLeft_unitIso_inv_app 📋 Mathlib.CategoryTheory.Equivalence
  {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 : C ≌ D) (X : CategoryTheory.Functor C E) : e.congrLeft.unitIso.inv.app X = (e.funInvIdAssoc X).hom
• CategoryTheory.Equivalence.congrRight_counitIso_hom_app 📋 Mathlib.CategoryTheory.Equivalence
  {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 : C ≌ D) (X : CategoryTheory.Functor E D) : e.congrRight.counitIso.hom.app X = CategoryTheory.CategoryStruct.comp (X.associator e.inverse e.functor).hom (CategoryTheory.CategoryStruct.comp (X.whiskerLeft e.counitIso.hom) X.rightUnitor.hom)
• CategoryTheory.Equivalence.congrRight_unitIso_inv_app 📋 Mathlib.CategoryTheory.Equivalence
  {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 : C ≌ D) (X : CategoryTheory.Functor E C) : e.congrRight.unitIso.inv.app X = CategoryTheory.CategoryStruct.comp (X.associator e.functor e.inverse).inv (CategoryTheory.CategoryStruct.comp (X.whiskerLeft e.unitIso.inv) X.rightUnitor.hom)
• CategoryTheory.Equivalence.congrRight_counitIso_inv_app 📋 Mathlib.CategoryTheory.Equivalence
  {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 : C ≌ D) (X : CategoryTheory.Functor E D) : e.congrRight.counitIso.inv.app X = CategoryTheory.CategoryStruct.comp X.rightUnitor.inv (CategoryTheory.CategoryStruct.comp (X.whiskerLeft e.counitIso.inv) (X.associator e.inverse e.functor).inv)
• CategoryTheory.Equivalence.congrRight_unitIso_hom_app 📋 Mathlib.CategoryTheory.Equivalence
  {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 : C ≌ D) (X : CategoryTheory.Functor E C) : e.congrRight.unitIso.hom.app X = CategoryTheory.CategoryStruct.comp X.rightUnitor.inv (CategoryTheory.CategoryStruct.comp (X.whiskerLeft e.unitIso.hom) (X.associator e.functor e.inverse).hom)
• CategoryTheory.opOpEquivalence_functor 📋 Mathlib.CategoryTheory.Opposites
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : (CategoryTheory.opOpEquivalence C).functor = CategoryTheory.unopUnop C
• CategoryTheory.Equivalence.op_functor 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : e.op.functor = e.functor.op
• CategoryTheory.Equivalence.unop_functor 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ Dᵒᵖ) : e.unop.functor = e.functor.unop
• CategoryTheory.Equivalence.leftOp_functor_obj 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ Dᵒᵖ) (X : Cᵒᵖ) : e.leftOp.functor.obj X = Opposite.unop (e.functor.obj (Opposite.unop X))
• CategoryTheory.Equivalence.rightOp_functor_obj 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ D) (X : C) : e.rightOp.functor.obj X = Opposite.op (e.functor.obj (Opposite.op X))
• CategoryTheory.Functor.opUnopEquiv_functor 📋 Mathlib.CategoryTheory.Opposites
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] : (CategoryTheory.Functor.opUnopEquiv C D).functor = CategoryTheory.Functor.opHom C D
• CategoryTheory.Functor.leftOpRightOpEquiv_functor_obj_obj 📋 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) : ((CategoryTheory.Functor.leftOpRightOpEquiv C D).functor.obj F).obj X = Opposite.op ((Opposite.unop F).obj (Opposite.op X))
• CategoryTheory.Equivalence.op_counitIso 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : e.op.counitIso = (CategoryTheory.NatIso.op e.counitIso).symm
• CategoryTheory.Equivalence.op_unitIso 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) : e.op.unitIso = (CategoryTheory.NatIso.op e.unitIso).symm
• CategoryTheory.Equivalence.unop_counitIso 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ Dᵒᵖ) : e.unop.counitIso = (CategoryTheory.NatIso.unop e.counitIso).symm
• CategoryTheory.Equivalence.unop_unitIso 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ Dᵒᵖ) : e.unop.unitIso = (CategoryTheory.NatIso.unop e.unitIso).symm
• CategoryTheory.Functor.leftOpRightOpEquiv_functor_obj_map 📋 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✝ Y✝ : C} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Functor.leftOpRightOpEquiv C D).functor.obj F).map f = ((Opposite.unop F).map f.op).op
• CategoryTheory.Equivalence.leftOp_functor_map 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ Dᵒᵖ) {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) : e.leftOp.functor.map f = (e.functor.map f.unop).unop
• CategoryTheory.Equivalence.rightOp_functor_map 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : e.rightOp.functor.map f = (e.functor.map f.op).op
• CategoryTheory.Functor.leftOpRightOpEquiv_functor_map_app 📋 Mathlib.CategoryTheory.Opposites
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] {X✝ Y✝ : (CategoryTheory.Functor Cᵒᵖ D)ᵒᵖ} (η : X✝ ⟶ Y✝) (x✝ : C) : ((CategoryTheory.Functor.leftOpRightOpEquiv C D).functor.map η).app x✝ = (η.unop.app (Opposite.op x✝)).op
• CategoryTheory.Equivalence.leftOp_counitIso_hom_app 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ Dᵒᵖ) (X : D) : e.leftOp.counitIso.hom.app X = (e.counitIso.inv.app (Opposite.op X)).unop
• CategoryTheory.Equivalence.leftOp_counitIso_inv_app 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ Dᵒᵖ) (X : D) : e.leftOp.counitIso.inv.app X = (e.counitIso.hom.app (Opposite.op X)).unop
• CategoryTheory.Equivalence.leftOp_unitIso_hom_app 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ Dᵒᵖ) (X : Cᵒᵖ) : e.leftOp.unitIso.hom.app X = (e.unitIso.inv.app (Opposite.unop X)).op
• CategoryTheory.Equivalence.leftOp_unitIso_inv_app 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ Dᵒᵖ) (X : Cᵒᵖ) : e.leftOp.unitIso.inv.app X = (e.unitIso.hom.app (Opposite.unop X)).op
• CategoryTheory.Equivalence.rightOp_unitIso_hom_app 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ D) (X : C) : e.rightOp.unitIso.hom.app X = (e.unitIso.inv.app (Opposite.op X)).unop
• CategoryTheory.Equivalence.rightOp_unitIso_inv_app 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ D) (X : C) : e.rightOp.unitIso.inv.app X = (e.unitIso.hom.app (Opposite.op X)).unop
• CategoryTheory.Equivalence.rightOp_counitIso_hom_app 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ D) (X : Dᵒᵖ) : e.rightOp.counitIso.hom.app X = (e.counitIso.inv.app (Opposite.unop X)).op
• CategoryTheory.Equivalence.rightOp_counitIso_inv_app 📋 Mathlib.CategoryTheory.Opposites
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (e : Cᵒᵖ ≌ D) (X : Dᵒᵖ) : e.rightOp.counitIso.inv.app X = (e.counitIso.hom.app (Opposite.unop X)).op
• CategoryTheory.Equivalence.induced_functor 📋 Mathlib.CategoryTheory.EqToHom
  {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {T : Type u_2} (e : T ≃ D) : (CategoryTheory.Equivalence.induced e).functor = CategoryTheory.inducedFunctor ⇑e
• CategoryTheory.Prod.braiding_functor 📋 Mathlib.CategoryTheory.Products.Basic
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] : (CategoryTheory.Prod.braiding C D).functor = CategoryTheory.Prod.swap C D
• CategoryTheory.Equivalence.prod_functor 📋 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] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (E₁ : A ≌ B) (E₂ : C ≌ D) : (E₁.prod E₂).functor = E₁.functor.prod E₂.functor
• CategoryTheory.prodOpEquiv_functor_obj 📋 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).functor.obj X = (Opposite.op (Opposite.unop X).1, Opposite.op (Opposite.unop X).2)
• CategoryTheory.functorProdFunctorEquiv_functor 📋 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] : (CategoryTheory.functorProdFunctorEquiv A B C).functor = CategoryTheory.prodFunctorToFunctorProd A B C
• CategoryTheory.Equivalence.prod_counitIso 📋 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] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (E₁ : A ≌ B) (E₂ : C ≌ D) : (E₁.prod E₂).counitIso = CategoryTheory.NatIso.prod E₁.counitIso E₂.counitIso
• CategoryTheory.Equivalence.prod_unitIso 📋 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] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (E₁ : A ≌ B) (E₂ : C ≌ D) : (E₁.prod E₂).unitIso = CategoryTheory.NatIso.prod E₁.unitIso E₂.unitIso
• CategoryTheory.prodOpEquiv_functor_map 📋 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✝) : (CategoryTheory.prodOpEquiv C).functor.map f = CategoryTheory.Prod.mkHom f.unop.1.op f.unop.2.op
• CategoryTheory.Equivalence.pi_functor 📋 Mathlib.CategoryTheory.Pi.Basic
  {I : Type w₀} {C : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : I → Type u₂} [(i : I) → CategoryTheory.Category.{v₂, u₂} (D i)] (E : (i : I) → C i ≌ D i) : (CategoryTheory.Equivalence.pi E).functor = CategoryTheory.Functor.pi fun i => (E i).functor
• CategoryTheory.Pi.evalCompEqToEquivalenceFunctor 📋 Mathlib.CategoryTheory.Pi.Basic
  {I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {i j : I} (h : i = j) : (CategoryTheory.Pi.eval C i).comp (CategoryTheory.Pi.eqToEquivalence C h).functor ≅ CategoryTheory.Pi.eval C j
• CategoryTheory.Pi.eqToEquivalenceFunctorIso 📋 Mathlib.CategoryTheory.Pi.Basic
  {I : Type w₀} {J : Type w₁} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (f : J → I) {i' j' : J} (h : i' = j') : (CategoryTheory.Pi.eqToEquivalence C ⋯).functor ≅ (CategoryTheory.Pi.eqToEquivalence (fun i' => C (f i')) h).functor
• CategoryTheory.Pi.optionEquivalence_functor 📋 Mathlib.CategoryTheory.Pi.Basic
  {J : Type w₁} (C' : Option J → Type u₁) [(i : Option J) → CategoryTheory.Category.{v₁, u₁} (C' i)] : (CategoryTheory.Pi.optionEquivalence C').functor = (CategoryTheory.Pi.eval C' none).prod' (CategoryTheory.Functor.pi' fun i => CategoryTheory.Pi.eval C' (some i))
• CategoryTheory.Equivalence.pi_counitIso 📋 Mathlib.CategoryTheory.Pi.Basic
  {I : Type w₀} {C : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : I → Type u₂} [(i : I) → CategoryTheory.Category.{v₂, u₂} (D i)] (E : (i : I) → C i ≌ D i) : (CategoryTheory.Equivalence.pi E).counitIso = CategoryTheory.NatIso.pi fun i => (E i).counitIso
• CategoryTheory.Equivalence.pi_unitIso 📋 Mathlib.CategoryTheory.Pi.Basic
  {I : Type w₀} {C : I → Type u₁} [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : I → Type u₂} [(i : I) → CategoryTheory.Category.{v₂, u₂} (D i)] (E : (i : I) → C i ≌ D i) : (CategoryTheory.Equivalence.pi E).unitIso = CategoryTheory.NatIso.pi fun i => (E i).unitIso
• CategoryTheory.Pi.evalCompEqToEquivalenceFunctor_hom 📋 Mathlib.CategoryTheory.Pi.Basic
  {I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {i j : I} (h : i = j) : (CategoryTheory.Pi.evalCompEqToEquivalenceFunctor C h).hom = CategoryTheory.eqToHom ⋯
• CategoryTheory.Pi.eqToEquivalenceFunctorIso_hom 📋 Mathlib.CategoryTheory.Pi.Basic
  {I : Type w₀} {J : Type w₁} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (f : J → I) {i' j' : J} (h : i' = j') : (CategoryTheory.Pi.eqToEquivalenceFunctorIso C f h).hom = CategoryTheory.eqToHom ⋯
• CategoryTheory.Pi.evalCompEqToEquivalenceFunctor_inv 📋 Mathlib.CategoryTheory.Pi.Basic
  {I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {i j : I} (h : i = j) : (CategoryTheory.Pi.evalCompEqToEquivalenceFunctor C h).inv = CategoryTheory.eqToHom ⋯
• CategoryTheory.Pi.eqToEquivalenceFunctorIso_inv 📋 Mathlib.CategoryTheory.Pi.Basic
  {I : Type w₀} {J : Type w₁} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (f : J → I) {i' j' : J} (h : i' = j') : (CategoryTheory.Pi.eqToEquivalenceFunctorIso C f h).inv = CategoryTheory.eqToHom ⋯
• CategoryTheory.Pi.equivalenceOfEquiv_functor 📋 Mathlib.CategoryTheory.Pi.Basic
  {I : Type w₀} {J : Type w₁} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (e : J ≃ I) : (CategoryTheory.Pi.equivalenceOfEquiv C e).functor = CategoryTheory.Functor.pi' fun i => (CategoryTheory.Pi.eval (fun j => C (e j)) (e.symm i)).comp (CategoryTheory.Pi.eqToEquivalence C ⋯).functor
• CategoryTheory.Pi.equivalenceOfEquiv_counitIso 📋 Mathlib.CategoryTheory.Pi.Basic
  {I : Type w₀} {J : Type w₁} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (e : J ≃ I) : (CategoryTheory.Pi.equivalenceOfEquiv C e).counitIso = CategoryTheory.NatIso.pi' fun i => ((CategoryTheory.Functor.pi' fun i' => CategoryTheory.Pi.eval C (e i')).associator (CategoryTheory.Pi.eval (fun j => C (e j)) (e.symm i)) (CategoryTheory.Pi.eqToEquivalence C ⋯).functor).symm ≪≫ CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.Functor.pi'CompEval (fun i' => CategoryTheory.Pi.eval C (e i')) (e.symm i)) (CategoryTheory.Pi.eqToEquivalence C ⋯).functor ≪≫ CategoryTheory.Pi.evalCompEqToEquivalenceFunctor C ⋯ ≪≫ (CategoryTheory.Pi.eval C i).leftUnitor.symm
• CategoryTheory.Pi.equivalenceOfEquiv_unitIso 📋 Mathlib.CategoryTheory.Pi.Basic
  {I : Type w₀} {J : Type w₁} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (e : J ≃ I) : (CategoryTheory.Pi.equivalenceOfEquiv C e).unitIso = CategoryTheory.NatIso.pi' fun i' => (CategoryTheory.Pi.eval (fun i => C (e i)) i').leftUnitor ≪≫ (CategoryTheory.Pi.evalCompEqToEquivalenceFunctor (fun j => C (e j)) ⋯).symm ≪≫ (CategoryTheory.Pi.eval (fun j => C (e j)) (e.symm (e i'))).isoWhiskerLeft (CategoryTheory.Pi.eqToEquivalenceFunctorIso C ⇑e ⋯).symm ≪≫ (CategoryTheory.Functor.pi'CompEval (CategoryTheory.Pi.eval (fun j => C (e j)) (e.symm (e i'))).comp (CategoryTheory.Pi.eqToEquivalence C ⋯).functor).symm ≪≫ (CategoryTheory.Functor.pi' (CategoryTheory.Pi.eval (fun j => C (e j)) (e.symm (e i'))).comp).isoWhiskerLeft (CategoryTheory.Functor.pi'CompEval (CategoryTheory.Pi.eval fun i => C (e i')) (CategoryTheory.Pi.eqToEquivalence C ⋯).functor).symm ≪≫ ((CategoryTheory.Functor.pi' (CategoryTheory.Pi.eval (fun j => C (e j)) (e.symm (e i'))).comp).associator (CategoryTheory.Functor.pi' (CategoryTheory.Pi.eval fun i => C (e i'))) (CategoryTheory.Pi.eval (fun i => C (e i')) (CategoryTheory.Pi.eqToEquivalence C ⋯).functor)).symm
• CategoryTheory.Discrete.opposite_functor_obj_as 📋 Mathlib.CategoryTheory.Discrete.Basic
  (α : Type u₁) (X : (CategoryTheory.Discrete α)ᵒᵖ) : ((CategoryTheory.Discrete.opposite α).functor.obj X).as = (Opposite.unop X).as
• CategoryTheory.Discrete.equivalence_functor 📋 Mathlib.CategoryTheory.Discrete.Basic
  {I : Type u₁} {J : Type u₂} (e : I ≃ J) : (CategoryTheory.Discrete.equivalence e).functor = CategoryTheory.Discrete.functor (CategoryTheory.Discrete.mk ∘ ⇑e)
• CategoryTheory.piEquivalenceFunctorDiscrete_functor_obj 📋 Mathlib.CategoryTheory.Discrete.Basic
  (J : Type u₂) (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (F : J → C) : (CategoryTheory.piEquivalenceFunctorDiscrete J C).functor.obj F = CategoryTheory.Discrete.functor F
• CategoryTheory.Discrete.equivOfEquivalence_apply 📋 Mathlib.CategoryTheory.Discrete.Basic
  {α : Type u₁} {β : Type u₂} (h : CategoryTheory.Discrete α ≌ CategoryTheory.Discrete β) (a✝ : α) : (CategoryTheory.Discrete.equivOfEquivalence h) a✝ = (CategoryTheory.Discrete.as ∘ h.functor.obj ∘ CategoryTheory.Discrete.mk) a✝
• CategoryTheory.piEquivalenceFunctorDiscreteCompEvaluationIso 📋 Mathlib.CategoryTheory.Discrete.Basic
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] {J : Type u_2} (j : J) : (CategoryTheory.piEquivalenceFunctorDiscrete J C).functor.comp ((CategoryTheory.evaluation (CategoryTheory.Discrete J) C).obj { as := j }) ≅ CategoryTheory.Pi.eval (fun a => C) j
• CategoryTheory.piEquivalenceFunctorDiscrete_functor_map 📋 Mathlib.CategoryTheory.Discrete.Basic
  (J : Type u₂) (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] {X✝ Y✝ : J → C} (f : X✝ ⟶ Y✝) : (CategoryTheory.piEquivalenceFunctorDiscrete J C).functor.map f = CategoryTheory.Discrete.natTrans fun j => f j.as
• CategoryTheory.piEquivalenceFunctorDiscreteCompEvaluationIso_hom_app 📋 Mathlib.CategoryTheory.Discrete.Basic
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] {J : Type u_2} (j : J) (X : J → C) : (CategoryTheory.piEquivalenceFunctorDiscreteCompEvaluationIso C j).hom.app X = CategoryTheory.CategoryStruct.id (X j)
• CategoryTheory.piEquivalenceFunctorDiscreteCompEvaluationIso_inv_app 📋 Mathlib.CategoryTheory.Discrete.Basic
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] {J : Type u_2} (j : J) (X : J → C) : (CategoryTheory.piEquivalenceFunctorDiscreteCompEvaluationIso C j).inv.app X = CategoryTheory.CategoryStruct.id (X j)
• CategoryTheory.prod.leftUnitorEquivalence_functor 📋 Mathlib.CategoryTheory.Products.Unitor
  (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.prod.leftUnitorEquivalence C).functor = CategoryTheory.prod.leftUnitor C
• CategoryTheory.prod.rightUnitorEquivalence_functor 📋 Mathlib.CategoryTheory.Products.Unitor
  (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.prod.rightUnitorEquivalence C).functor = CategoryTheory.prod.rightUnitor C

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 69fae59