Loogle!

Result

Found 157 declarations mentioning CategoryTheory.EnrichedCategory.

• CategoryTheory.EnrichedCategory 📋 Mathlib.CategoryTheory.Enriched.Basic
  (V : Type v) [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] (C : Type u₁) : Type (max (max u₁ v) w)
• CategoryTheory.ForgetEnrichment 📋 Mathlib.CategoryTheory.Enriched.Basic
  (W : Type v) [CategoryTheory.Category.{w, v} W] [CategoryTheory.MonoidalCategory W] (C : Type u₁) [CategoryTheory.EnrichedCategory W C] : Type u₁
• CategoryTheory.categoryOfEnrichedCategoryType 📋 Mathlib.CategoryTheory.Enriched.Basic
  (C : Type u₁) [𝒞 : CategoryTheory.EnrichedCategory (Type v) C] : CategoryTheory.Category.{v, u₁} C
• CategoryTheory.enrichedCategoryTypeOfCategory 📋 Mathlib.CategoryTheory.Enriched.Basic
  (C : Type u₁) [𝒞 : CategoryTheory.Category.{v, u₁} C] : CategoryTheory.EnrichedCategory (Type v) C
• CategoryTheory.enrichedCategoryTypeEquivCategory 📋 Mathlib.CategoryTheory.Enriched.Basic
  (C : Type u₁) : CategoryTheory.EnrichedCategory (Type v) C ≃ CategoryTheory.Category.{v, u₁} C
• CategoryTheory.EnrichedCategory.Hom 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} {inst✝ : CategoryTheory.Category.{w, v} V} {inst✝¹ : CategoryTheory.MonoidalCategory V} {C : Type u₁} [self : CategoryTheory.EnrichedCategory V C] : C → C → V
• CategoryTheory.EnrichedFunctor 📋 Mathlib.CategoryTheory.Enriched.Basic
  (V : Type v) [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] (C : Type u₁) [CategoryTheory.EnrichedCategory V C] (D : Type u₂) [CategoryTheory.EnrichedCategory V D] : Type (max (max u₁ u₂) w)
• CategoryTheory.categoryForgetEnrichment 📋 Mathlib.CategoryTheory.Enriched.Basic
  {C : Type u₁} (W : Type v) [CategoryTheory.Category.{w, v} W] [CategoryTheory.MonoidalCategory W] [CategoryTheory.EnrichedCategory W C] : CategoryTheory.Category.{w, u₁} (CategoryTheory.ForgetEnrichment W C)
• CategoryTheory.ForgetEnrichment.of 📋 Mathlib.CategoryTheory.Enriched.Basic
  {C : Type u₁} (W : Type v) [CategoryTheory.Category.{w, v} W] [CategoryTheory.MonoidalCategory W] [CategoryTheory.EnrichedCategory W C] (X : C) : CategoryTheory.ForgetEnrichment W C
• CategoryTheory.ForgetEnrichment.to 📋 Mathlib.CategoryTheory.Enriched.Basic
  {C : Type u₁} (W : Type v) [CategoryTheory.Category.{w, v} W] [CategoryTheory.MonoidalCategory W] [CategoryTheory.EnrichedCategory W C] (X : CategoryTheory.ForgetEnrichment W C) : C
• CategoryTheory.EnrichedFunctor.id 📋 Mathlib.CategoryTheory.Enriched.Basic
  (V : Type v) [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] (C : Type u₁) [CategoryTheory.EnrichedCategory V C] : CategoryTheory.EnrichedFunctor V C C
• CategoryTheory.EnrichedFunctor.instInhabited 📋 Mathlib.CategoryTheory.Enriched.Basic
  (V : Type v) [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] : Inhabited (CategoryTheory.EnrichedFunctor V C C)
• CategoryTheory.EnrichedFunctor.category 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] : CategoryTheory.Category.{max u₁ w, max (max u₂ u₁) w} (CategoryTheory.EnrichedFunctor V C D)
• CategoryTheory.EnrichedFunctor.obj 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] (self : CategoryTheory.EnrichedFunctor V C D) : C → D
• CategoryTheory.ForgetEnrichment.to_of 📋 Mathlib.CategoryTheory.Enriched.Basic
  {C : Type u₁} (W : Type v) [CategoryTheory.Category.{w, v} W] [CategoryTheory.MonoidalCategory W] [CategoryTheory.EnrichedCategory W C] (X : C) : CategoryTheory.ForgetEnrichment.to W (CategoryTheory.ForgetEnrichment.of W X) = X
• CategoryTheory.EnrichedFunctor.id_obj 📋 Mathlib.CategoryTheory.Enriched.Basic
  (V : Type v) [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] (C : Type u₁) [CategoryTheory.EnrichedCategory V C] (X : C) : (CategoryTheory.EnrichedFunctor.id V C).obj X = X
• CategoryTheory.EnrichedNatTrans 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] (F G : CategoryTheory.EnrichedFunctor V C D) : Type (max u₁ w)
• CategoryTheory.eId 📋 Mathlib.CategoryTheory.Enriched.Basic
  (V : Type v) [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] (X : C) : CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ X ⟶[V] X
• CategoryTheory.EnrichedCategory.id 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} {inst✝ : CategoryTheory.Category.{w, v} V} {inst✝¹ : CategoryTheory.MonoidalCategory V} {C : Type u₁} [self : CategoryTheory.EnrichedCategory V C] (X : C) : CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ X ⟶[V] X
• CategoryTheory.GradedNatTrans 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] (A : CategoryTheory.Center V) (F G : CategoryTheory.EnrichedFunctor V C D) : Type (max u₁ w)
• CategoryTheory.ForgetEnrichment.of_to 📋 Mathlib.CategoryTheory.Enriched.Basic
  {C : Type u₁} (W : Type v) [CategoryTheory.Category.{w, v} W] [CategoryTheory.MonoidalCategory W] [CategoryTheory.EnrichedCategory W C] (X : CategoryTheory.ForgetEnrichment W C) : CategoryTheory.ForgetEnrichment.of W (CategoryTheory.ForgetEnrichment.to W X) = X
• CategoryTheory.instEnrichedCategoryTransportEnrichment 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {W : Type v'} [CategoryTheory.Category.{w', v'} W] [CategoryTheory.MonoidalCategory W] (F : CategoryTheory.Functor V W) [F.LaxMonoidal] : CategoryTheory.EnrichedCategory W (CategoryTheory.TransportEnrichment F C)
• CategoryTheory.enrichedNatTransYoneda 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] [CategoryTheory.BraidedCategory V] (F G : CategoryTheory.EnrichedFunctor V C D) : CategoryTheory.Functor Vᵒᵖ (Type (max u₁ w))
• CategoryTheory.enrichedFunctorTypeEquivFunctor 📋 Mathlib.CategoryTheory.Enriched.Basic
  {C : Type u₁} [𝒞 : CategoryTheory.EnrichedCategory (Type v) C] {D : Type u₂} [𝒟 : CategoryTheory.EnrichedCategory (Type v) D] : CategoryTheory.EnrichedFunctor (Type v) C D ≃ CategoryTheory.Functor C D
• CategoryTheory.EnrichedFunctor.comp 📋 Mathlib.CategoryTheory.Enriched.Basic
  (V : Type v) [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} {D : Type u₂} {E : Type u₃} [CategoryTheory.EnrichedCategory V C] [CategoryTheory.EnrichedCategory V D] [CategoryTheory.EnrichedCategory V E] (F : CategoryTheory.EnrichedFunctor V C D) (G : CategoryTheory.EnrichedFunctor V D E) : CategoryTheory.EnrichedFunctor V C E
• CategoryTheory.EnrichedFunctor.forget 📋 Mathlib.CategoryTheory.Enriched.Basic
  {W : Type v'} [CategoryTheory.Category.{w', v'} W] [CategoryTheory.MonoidalCategory W] {C : Type u₁} [CategoryTheory.EnrichedCategory W C] {D : Type u₂} [CategoryTheory.EnrichedCategory W D] (F : CategoryTheory.EnrichedFunctor W C D) : CategoryTheory.Functor (CategoryTheory.ForgetEnrichment W C) (CategoryTheory.ForgetEnrichment W D)
• CategoryTheory.eComp 📋 Mathlib.CategoryTheory.Enriched.Basic
  (V : Type v) [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] (X Y Z : C) : CategoryTheory.MonoidalCategoryStruct.tensorObj (X ⟶[V] Y) (Y ⟶[V] Z) ⟶ X ⟶[V] Z
• CategoryTheory.EnrichedCategory.comp 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} {inst✝ : CategoryTheory.Category.{w, v} V} {inst✝¹ : CategoryTheory.MonoidalCategory V} {C : Type u₁} [self : CategoryTheory.EnrichedCategory V C] (X Y Z : C) : CategoryTheory.MonoidalCategoryStruct.tensorObj (X ⟶[V] Y) (Y ⟶[V] Z) ⟶ X ⟶[V] Z
• CategoryTheory.EnrichedFunctor.id_map 📋 Mathlib.CategoryTheory.Enriched.Basic
  (V : Type v) [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] (C : Type u₁) [CategoryTheory.EnrichedCategory V C] (x✝ x✝¹ : C) : (CategoryTheory.EnrichedFunctor.id V C).map x✝ x✝¹ = CategoryTheory.CategoryStruct.id (x✝ ⟶[V] x✝¹)
• CategoryTheory.EnrichedFunctor.map 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] (self : CategoryTheory.EnrichedFunctor V C D) (X Y : C) : (X ⟶[V] Y) ⟶ self.obj X ⟶[V] self.obj Y
• CategoryTheory.ForgetEnrichment.homOf 📋 Mathlib.CategoryTheory.Enriched.Basic
  {C : Type u₁} (W : Type v) [CategoryTheory.Category.{w, v} W] [CategoryTheory.MonoidalCategory W] [CategoryTheory.EnrichedCategory W C] {X Y : C} (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit W ⟶ X ⟶[W] Y) : CategoryTheory.ForgetEnrichment.of W X ⟶ CategoryTheory.ForgetEnrichment.of W Y
• CategoryTheory.EnrichedFunctor.comp_obj 📋 Mathlib.CategoryTheory.Enriched.Basic
  (V : Type v) [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} {D : Type u₂} {E : Type u₃} [CategoryTheory.EnrichedCategory V C] [CategoryTheory.EnrichedCategory V D] [CategoryTheory.EnrichedCategory V E] (F : CategoryTheory.EnrichedFunctor V C D) (G : CategoryTheory.EnrichedFunctor V D E) (X : C) : (CategoryTheory.EnrichedFunctor.comp V F G).obj X = G.obj (F.obj X)
• CategoryTheory.ForgetEnrichment.homTo 📋 Mathlib.CategoryTheory.Enriched.Basic
  {C : Type u₁} (W : Type v) [CategoryTheory.Category.{w, v} W] [CategoryTheory.MonoidalCategory W] [CategoryTheory.EnrichedCategory W C] {X Y : CategoryTheory.ForgetEnrichment W C} (f : X ⟶ Y) : CategoryTheory.MonoidalCategoryStruct.tensorUnit W ⟶ CategoryTheory.ForgetEnrichment.to W X ⟶[W] CategoryTheory.ForgetEnrichment.to W Y
• CategoryTheory.EnrichedFunctor.forgetId 📋 Mathlib.CategoryTheory.Enriched.Basic
  (W : Type v') [CategoryTheory.Category.{w', v'} W] [CategoryTheory.MonoidalCategory W] (C : Type u₁) [CategoryTheory.EnrichedCategory W C] : (CategoryTheory.EnrichedFunctor.id W C).forget ≅ CategoryTheory.Functor.id (CategoryTheory.ForgetEnrichment W C)
• CategoryTheory.enrichedNatTransYoneda_obj 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] [CategoryTheory.BraidedCategory V] (F G : CategoryTheory.EnrichedFunctor V C D) (A : Vᵒᵖ) : (CategoryTheory.enrichedNatTransYoneda F G).obj A = CategoryTheory.GradedNatTrans ((CategoryTheory.Center.ofBraided V).obj (Opposite.unop A)) F G
• CategoryTheory.GradedNatTrans.app 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] {A : CategoryTheory.Center V} {F G : CategoryTheory.EnrichedFunctor V C D} (self : CategoryTheory.GradedNatTrans A F G) (X : C) : A.fst ⟶ F.obj X ⟶[V] G.obj X
• CategoryTheory.ForgetEnrichment.homTo_id 📋 Mathlib.CategoryTheory.Enriched.Basic
  {C : Type u₁} (W : Type v) [CategoryTheory.Category.{w, v} W] [CategoryTheory.MonoidalCategory W] [CategoryTheory.EnrichedCategory W C] (X : CategoryTheory.ForgetEnrichment W C) : CategoryTheory.ForgetEnrichment.homTo W (CategoryTheory.CategoryStruct.id X) = CategoryTheory.eId W (CategoryTheory.ForgetEnrichment.to W X)
• CategoryTheory.EnrichedFunctor.forget_obj 📋 Mathlib.CategoryTheory.Enriched.Basic
  {W : Type v'} [CategoryTheory.Category.{w', v'} W] [CategoryTheory.MonoidalCategory W] {C : Type u₁} [CategoryTheory.EnrichedCategory W C] {D : Type u₂} [CategoryTheory.EnrichedCategory W D] (F : CategoryTheory.EnrichedFunctor W C D) (X : CategoryTheory.ForgetEnrichment W C) : F.forget.obj X = CategoryTheory.ForgetEnrichment.of W (F.obj (CategoryTheory.ForgetEnrichment.to W X))
• CategoryTheory.ForgetEnrichment.homOf_eId 📋 Mathlib.CategoryTheory.Enriched.Basic
  {C : Type u₁} (W : Type v) [CategoryTheory.Category.{w, v} W] [CategoryTheory.MonoidalCategory W] [CategoryTheory.EnrichedCategory W C] (X : C) : CategoryTheory.ForgetEnrichment.homOf W (CategoryTheory.eId W X) = CategoryTheory.CategoryStruct.id (CategoryTheory.ForgetEnrichment.of W X)
• CategoryTheory.ForgetEnrichment.homTo_homOf 📋 Mathlib.CategoryTheory.Enriched.Basic
  {C : Type u₁} (W : Type v) [CategoryTheory.Category.{w, v} W] [CategoryTheory.MonoidalCategory W] [CategoryTheory.EnrichedCategory W C] {X Y : C} (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit W ⟶ X ⟶[W] Y) : CategoryTheory.ForgetEnrichment.homTo W (CategoryTheory.ForgetEnrichment.homOf W f) = f
• CategoryTheory.EnrichedFunctor.isoMk 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] {F G : CategoryTheory.EnrichedFunctor V C D} (h : F.forget ≅ G.forget) : F ≅ G
• CategoryTheory.ForgetEnrichment.homOf_homTo 📋 Mathlib.CategoryTheory.Enriched.Basic
  {C : Type u₁} (W : Type v) [CategoryTheory.Category.{w, v} W] [CategoryTheory.MonoidalCategory W] [CategoryTheory.EnrichedCategory W C] {X Y : CategoryTheory.ForgetEnrichment W C} (f : X ⟶ Y) : CategoryTheory.ForgetEnrichment.homOf W (CategoryTheory.ForgetEnrichment.homTo W f) = f
• CategoryTheory.GradedNatTrans.ext 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} {inst✝ : CategoryTheory.Category.{w, v} V} {inst✝¹ : CategoryTheory.MonoidalCategory V} {C : Type u₁} {inst✝² : CategoryTheory.EnrichedCategory V C} {D : Type u₂} {inst✝³ : CategoryTheory.EnrichedCategory V D} {A : CategoryTheory.Center V} {F G : CategoryTheory.EnrichedFunctor V C D} {x y : CategoryTheory.GradedNatTrans A F G} (app : x.app = y.app) : x = y
• CategoryTheory.GradedNatTrans.ext_iff 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} {inst✝ : CategoryTheory.Category.{w, v} V} {inst✝¹ : CategoryTheory.MonoidalCategory V} {C : Type u₁} {inst✝² : CategoryTheory.EnrichedCategory V C} {D : Type u₂} {inst✝³ : CategoryTheory.EnrichedCategory V D} {A : CategoryTheory.Center V} {F G : CategoryTheory.EnrichedFunctor V C D} {x y : CategoryTheory.GradedNatTrans A F G} : x = y ↔ x.app = y.app
• CategoryTheory.EnrichedFunctor.map_id 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] (self : CategoryTheory.EnrichedFunctor V C D) (X : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eId V X) (self.map X X) = CategoryTheory.eId V (self.obj X)
• CategoryTheory.EnrichedNatTrans.mk 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] {F G : CategoryTheory.EnrichedFunctor V C D} (out : F.forget ⟶ G.forget) : CategoryTheory.EnrichedNatTrans F G
• CategoryTheory.EnrichedNatTrans.out 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] {F G : CategoryTheory.EnrichedFunctor V C D} (self : CategoryTheory.EnrichedNatTrans F G) : F.forget ⟶ G.forget
• CategoryTheory.EnrichedFunctor.forgetComp 📋 Mathlib.CategoryTheory.Enriched.Basic
  {W : Type v'} [CategoryTheory.Category.{w', v'} W] [CategoryTheory.MonoidalCategory W] {C : Type u₁} [CategoryTheory.EnrichedCategory W C] {D : Type u₂} [CategoryTheory.EnrichedCategory W D] {E : Type u₃} [CategoryTheory.EnrichedCategory W E] (F : CategoryTheory.EnrichedFunctor W C D) (G : CategoryTheory.EnrichedFunctor W D E) : (CategoryTheory.EnrichedFunctor.comp W F G).forget ≅ F.forget.comp G.forget
• CategoryTheory.TransportEnrichment.eId_eq 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {W : Type v'} [CategoryTheory.Category.{w', v'} W] [CategoryTheory.MonoidalCategory W] (F : CategoryTheory.Functor V W) [F.LaxMonoidal] (X : CategoryTheory.TransportEnrichment F C) : CategoryTheory.eId W X = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map (CategoryTheory.eId V X))
• CategoryTheory.enrichedFunctorTypeEquivFunctor_apply_obj 📋 Mathlib.CategoryTheory.Enriched.Basic
  {C : Type u₁} [𝒞 : CategoryTheory.EnrichedCategory (Type v) C] {D : Type u₂} [𝒟 : CategoryTheory.EnrichedCategory (Type v) D] (F : CategoryTheory.EnrichedFunctor (Type v) C D) (X : C) : (CategoryTheory.enrichedFunctorTypeEquivFunctor F).obj X = F.obj X
• CategoryTheory.EnrichedFunctor.map_id_assoc 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] (self : CategoryTheory.EnrichedFunctor V C D) (X : C) {Z : V} (h : (self.obj X ⟶[V] self.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eId V X) (CategoryTheory.CategoryStruct.comp (self.map X X) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eId V (self.obj X)) h
• CategoryTheory.enrichedFunctorTypeEquivFunctor_symm_apply_obj 📋 Mathlib.CategoryTheory.Enriched.Basic
  {C : Type u₁} [𝒞 : CategoryTheory.EnrichedCategory (Type v) C] {D : Type u₂} [𝒟 : CategoryTheory.EnrichedCategory (Type v) D] (F : CategoryTheory.Functor C D) (X : C) : (CategoryTheory.enrichedFunctorTypeEquivFunctor.symm F).obj X = F.obj X
• CategoryTheory.e_comp_id 📋 Mathlib.CategoryTheory.Enriched.Basic
  (V : Type v) [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] (X Y : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (X ⟶[V] Y)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X ⟶[V] Y) (CategoryTheory.eId V Y)) (CategoryTheory.eComp V X Y Y)) = CategoryTheory.CategoryStruct.id (X ⟶[V] Y)
• CategoryTheory.e_id_comp 📋 Mathlib.CategoryTheory.Enriched.Basic
  (V : Type v) [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] (X Y : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (X ⟶[V] Y)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.eId V X) (X ⟶[V] Y)) (CategoryTheory.eComp V X X Y)) = CategoryTheory.CategoryStruct.id (X ⟶[V] Y)
• CategoryTheory.EnrichedCategory.comp_id 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} {inst✝ : CategoryTheory.Category.{w, v} V} {inst✝¹ : CategoryTheory.MonoidalCategory V} {C : Type u₁} [self : CategoryTheory.EnrichedCategory V C] (X Y : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (X ⟶[V] Y)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X ⟶[V] Y) (CategoryTheory.EnrichedCategory.id Y)) (CategoryTheory.EnrichedCategory.comp X Y Y)) = CategoryTheory.CategoryStruct.id (X ⟶[V] Y)
• CategoryTheory.EnrichedCategory.id_comp 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} {inst✝ : CategoryTheory.Category.{w, v} V} {inst✝¹ : CategoryTheory.MonoidalCategory V} {C : Type u₁} [self : CategoryTheory.EnrichedCategory V C] (X Y : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (X ⟶[V] Y)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.EnrichedCategory.id X) (X ⟶[V] Y)) (CategoryTheory.EnrichedCategory.comp X X Y)) = CategoryTheory.CategoryStruct.id (X ⟶[V] Y)
• CategoryTheory.EnrichedFunctor.comp_map 📋 Mathlib.CategoryTheory.Enriched.Basic
  (V : Type v) [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} {D : Type u₂} {E : Type u₃} [CategoryTheory.EnrichedCategory V C] [CategoryTheory.EnrichedCategory V D] [CategoryTheory.EnrichedCategory V E] (F : CategoryTheory.EnrichedFunctor V C D) (G : CategoryTheory.EnrichedFunctor V D E) (x✝ x✝¹ : C) : (CategoryTheory.EnrichedFunctor.comp V F G).map x✝ x✝¹ = CategoryTheory.CategoryStruct.comp (F.map x✝ x✝¹) (G.map (F.obj x✝) (F.obj x✝¹))
• CategoryTheory.e_comp_id_assoc 📋 Mathlib.CategoryTheory.Enriched.Basic
  (V : Type v) [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] (X Y : C) {Z : V} (h : (X ⟶[V] Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (X ⟶[V] Y)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X ⟶[V] Y) (CategoryTheory.eId V Y)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Y) h)) = h
• CategoryTheory.e_id_comp_assoc 📋 Mathlib.CategoryTheory.Enriched.Basic
  (V : Type v) [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] (X Y : C) {Z : V} (h : (X ⟶[V] Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (X ⟶[V] Y)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.eId V X) (X ⟶[V] Y)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X X Y) h)) = h
• CategoryTheory.EnrichedFunctor.ext 📋 Mathlib.CategoryTheory.Enriched.Basic
  (V : Type v) [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} {D : Type u₂} [CategoryTheory.EnrichedCategory V C] [CategoryTheory.EnrichedCategory V D] {F G : CategoryTheory.EnrichedFunctor V C D} (h_obj : ∀ (X : C), F.obj X = G.obj X) (h_map : ∀ (X Y : C), CategoryTheory.CategoryStruct.comp (F.map X Y) (CategoryTheory.eqToHom ⋯) = G.map X Y) : F = G
• CategoryTheory.EnrichedFunctor.category_id_out 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] (F : CategoryTheory.EnrichedFunctor V C D) : (CategoryTheory.CategoryStruct.id F).out = CategoryTheory.CategoryStruct.id F.forget
• CategoryTheory.EnrichedFunctor.forgetId_hom_app 📋 Mathlib.CategoryTheory.Enriched.Basic
  (W : Type v') [CategoryTheory.Category.{w', v'} W] [CategoryTheory.MonoidalCategory W] (C : Type u₁) [CategoryTheory.EnrichedCategory W C] (X : CategoryTheory.ForgetEnrichment W C) : (CategoryTheory.EnrichedFunctor.forgetId W C).hom.app X = CategoryTheory.CategoryStruct.id X
• CategoryTheory.EnrichedFunctor.forgetId_inv_app 📋 Mathlib.CategoryTheory.Enriched.Basic
  (W : Type v') [CategoryTheory.Category.{w', v'} W] [CategoryTheory.MonoidalCategory W] (C : Type u₁) [CategoryTheory.EnrichedCategory W C] (X : CategoryTheory.ForgetEnrichment W C) : (CategoryTheory.EnrichedFunctor.forgetId W C).inv.app X = CategoryTheory.CategoryStruct.id X
• CategoryTheory.EnrichedFunctor.forget_map 📋 Mathlib.CategoryTheory.Enriched.Basic
  {W : Type v'} [CategoryTheory.Category.{w', v'} W] [CategoryTheory.MonoidalCategory W] {C : Type u₁} [CategoryTheory.EnrichedCategory W C] {D : Type u₂} [CategoryTheory.EnrichedCategory W D] (F : CategoryTheory.EnrichedFunctor W C D) {X✝ Y✝ : CategoryTheory.ForgetEnrichment W C} (f : X✝ ⟶ Y✝) : F.forget.map f = CategoryTheory.ForgetEnrichment.homOf W (CategoryTheory.CategoryStruct.comp (CategoryTheory.ForgetEnrichment.homTo W f) (F.map (CategoryTheory.ForgetEnrichment.to W X✝) (CategoryTheory.ForgetEnrichment.to W Y✝)))
• CategoryTheory.EnrichedFunctor.isoMk_hom_out 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] {F G : CategoryTheory.EnrichedFunctor V C D} (h : F.forget ≅ G.forget) : (CategoryTheory.EnrichedFunctor.isoMk h).hom.out = h.hom
• CategoryTheory.EnrichedFunctor.isoMk_inv_out 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] {F G : CategoryTheory.EnrichedFunctor V C D} (h : F.forget ≅ G.forget) : (CategoryTheory.EnrichedFunctor.isoMk h).inv.out = h.inv
• CategoryTheory.TransportEnrichment.eComp_eq 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {W : Type v'} [CategoryTheory.Category.{w', v'} W] [CategoryTheory.MonoidalCategory W] (F : CategoryTheory.Functor V W) [F.LaxMonoidal] (X Y Z : CategoryTheory.TransportEnrichment F C) : CategoryTheory.eComp W X Y Z = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F (X ⟶[V] Y) (Y ⟶[V] Z)) (F.map (CategoryTheory.eComp V X Y Z))
• CategoryTheory.enrichedFunctorTypeEquivFunctor_symm_apply_map 📋 Mathlib.CategoryTheory.Enriched.Basic
  {C : Type u₁} [𝒞 : CategoryTheory.EnrichedCategory (Type v) C] {D : Type u₂} [𝒟 : CategoryTheory.EnrichedCategory (Type v) D] (F : CategoryTheory.Functor C D) (x✝ x✝¹ : C) : (CategoryTheory.enrichedFunctorTypeEquivFunctor.symm F).map x✝ x✝¹ = TypeCat.ofHom fun f => F.map f
• CategoryTheory.EnrichedFunctor.category_comp_out 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] {X✝ Y✝ Z✝ : CategoryTheory.EnrichedFunctor V C D} (F : CategoryTheory.EnrichedNatTrans X✝ Y✝) (G : CategoryTheory.EnrichedNatTrans Y✝ Z✝) : (CategoryTheory.CategoryStruct.comp F G).out = CategoryTheory.CategoryStruct.comp F.out G.out
• CategoryTheory.EnrichedFunctor.hom_ext 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] {F G : CategoryTheory.EnrichedFunctor V C D} {α β : F ⟶ G} (h : ∀ (X : C), α.out.app X = β.out.app X) : α = β
• CategoryTheory.EnrichedFunctor.hom_ext_iff 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] {F G : CategoryTheory.EnrichedFunctor V C D} {α β : F ⟶ G} : α = β ↔ ∀ (X : C), α.out.app X = β.out.app X
• CategoryTheory.ForgetEnrichment.homOf_comp 📋 Mathlib.CategoryTheory.Enriched.Basic
  {C : Type u₁} (W : Type v) [CategoryTheory.Category.{w, v} W] [CategoryTheory.MonoidalCategory W] [CategoryTheory.EnrichedCategory W C] {X Y Z : C} (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit W ⟶ X ⟶[W] Y) (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit W ⟶ Y ⟶[W] Z) : CategoryTheory.ForgetEnrichment.homOf W (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit W)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) (CategoryTheory.eComp W X Y Z))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ForgetEnrichment.homOf W f) (CategoryTheory.ForgetEnrichment.homOf W g)
• CategoryTheory.EnrichedFunctor.mk 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] (obj : C → D) (map : (X Y : C) → (X ⟶[V] Y) ⟶ obj X ⟶[V] obj Y) (map_id : ∀ (X : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.eId V X) (map X X) = CategoryTheory.eId V (obj X) := by cat_disch) (map_comp : ∀ (X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Z) (map X Z) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (map X Y) (map Y Z)) (CategoryTheory.eComp V (obj X) (obj Y) (obj Z)) := by cat_disch) : CategoryTheory.EnrichedFunctor V C D
• CategoryTheory.enrichedNatTransYoneda_map 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] [CategoryTheory.BraidedCategory V] (F G : CategoryTheory.EnrichedFunctor V C D) {X✝ Y✝ : Vᵒᵖ} (f : X✝ ⟶ Y✝) : (CategoryTheory.enrichedNatTransYoneda F G).map f = TypeCat.ofHom fun σ => { app := fun X => CategoryTheory.CategoryStruct.comp f.unop (σ.app X), naturality := ⋯ }
• CategoryTheory.EnrichedFunctor.map_comp 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] (self : CategoryTheory.EnrichedFunctor V C D) (X Y Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Z) (self.map X Z) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (self.map X Y) (self.map Y Z)) (CategoryTheory.eComp V (self.obj X) (self.obj Y) (self.obj Z))
• CategoryTheory.enrichedNatTransYonedaTypeIsoYonedaNatTrans 📋 Mathlib.CategoryTheory.Enriched.Basic
  {C : Type v} [CategoryTheory.EnrichedCategory (Type v) C] {D : Type v} [CategoryTheory.EnrichedCategory (Type v) D] (F G : CategoryTheory.EnrichedFunctor (Type v) C D) : CategoryTheory.enrichedNatTransYoneda F G ≅ CategoryTheory.yoneda.obj (CategoryTheory.enrichedFunctorTypeEquivFunctor F ⟶ CategoryTheory.enrichedFunctorTypeEquivFunctor G)
• CategoryTheory.ForgetEnrichment.homTo_comp 📋 Mathlib.CategoryTheory.Enriched.Basic
  {C : Type u₁} (W : Type v) [CategoryTheory.Category.{w, v} W] [CategoryTheory.MonoidalCategory W] [CategoryTheory.EnrichedCategory W C] {X Y Z : CategoryTheory.ForgetEnrichment W C} (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.ForgetEnrichment.homTo W (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit W)).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.ForgetEnrichment.homTo W f) (CategoryTheory.ForgetEnrichment.homTo W g))) (CategoryTheory.eComp W (CategoryTheory.ForgetEnrichment.to W X) (CategoryTheory.ForgetEnrichment.to W Y) (CategoryTheory.ForgetEnrichment.to W Z))
• CategoryTheory.EnrichedFunctor.forgetComp_hom_app 📋 Mathlib.CategoryTheory.Enriched.Basic
  {W : Type v'} [CategoryTheory.Category.{w', v'} W] [CategoryTheory.MonoidalCategory W] {C : Type u₁} [CategoryTheory.EnrichedCategory W C] {D : Type u₂} [CategoryTheory.EnrichedCategory W D] {E : Type u₃} [CategoryTheory.EnrichedCategory W E] (F : CategoryTheory.EnrichedFunctor W C D) (G : CategoryTheory.EnrichedFunctor W D E) (X : CategoryTheory.ForgetEnrichment W C) : (F.forgetComp G).hom.app X = CategoryTheory.CategoryStruct.id (CategoryTheory.ForgetEnrichment.of W (G.obj (F.obj (CategoryTheory.ForgetEnrichment.to W X))))
• CategoryTheory.EnrichedFunctor.forgetComp_inv_app 📋 Mathlib.CategoryTheory.Enriched.Basic
  {W : Type v'} [CategoryTheory.Category.{w', v'} W] [CategoryTheory.MonoidalCategory W] {C : Type u₁} [CategoryTheory.EnrichedCategory W C] {D : Type u₂} [CategoryTheory.EnrichedCategory W D] {E : Type u₃} [CategoryTheory.EnrichedCategory W E] (F : CategoryTheory.EnrichedFunctor W C D) (G : CategoryTheory.EnrichedFunctor W D E) (X : CategoryTheory.ForgetEnrichment W C) : (F.forgetComp G).inv.app X = CategoryTheory.CategoryStruct.id (CategoryTheory.ForgetEnrichment.of W (G.obj (F.obj (CategoryTheory.ForgetEnrichment.to W X))))
• CategoryTheory.EnrichedFunctor.map_comp_assoc 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] (self : CategoryTheory.EnrichedFunctor V C D) (X Y Z : C) {Z✝ : V} (h : (self.obj X ⟶[V] self.obj Z) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Z) (CategoryTheory.CategoryStruct.comp (self.map X Z) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (self.map X Y) (self.map Y Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V (self.obj X) (self.obj Y) (self.obj Z)) h)
• CategoryTheory.enrichedFunctorTypeEquivFunctor_apply_map 📋 Mathlib.CategoryTheory.Enriched.Basic
  {C : Type u₁} [𝒞 : CategoryTheory.EnrichedCategory (Type v) C] {D : Type u₂} [𝒟 : CategoryTheory.EnrichedCategory (Type v) D] (F : CategoryTheory.EnrichedFunctor (Type v) C D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (CategoryTheory.enrichedFunctorTypeEquivFunctor F).map f = (CategoryTheory.ConcreteCategory.hom (F.map X✝ Y✝)) f
• CategoryTheory.e_assoc 📋 Mathlib.CategoryTheory.Enriched.Basic
  (V : Type v) [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] (W X Y Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (W ⟶[V] X) (X ⟶[V] Y) (Y ⟶[V] Z)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.eComp V W X Y) (Y ⟶[V] Z)) (CategoryTheory.eComp V W Y Z)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (W ⟶[V] X) (CategoryTheory.eComp V X Y Z)) (CategoryTheory.eComp V W X Z)
• CategoryTheory.e_assoc' 📋 Mathlib.CategoryTheory.Enriched.Basic
  (V : Type v) [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] (W X Y Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (W ⟶[V] X) (X ⟶[V] Y) (Y ⟶[V] Z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (W ⟶[V] X) (CategoryTheory.eComp V X Y Z)) (CategoryTheory.eComp V W X Z)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.eComp V W X Y) (Y ⟶[V] Z)) (CategoryTheory.eComp V W Y Z)
• CategoryTheory.EnrichedCategory.assoc 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} {inst✝ : CategoryTheory.Category.{w, v} V} {inst✝¹ : CategoryTheory.MonoidalCategory V} {C : Type u₁} [self : CategoryTheory.EnrichedCategory V C] (W X Y Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (W ⟶[V] X) (X ⟶[V] Y) (Y ⟶[V] Z)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.EnrichedCategory.comp W X Y) (Y ⟶[V] Z)) (CategoryTheory.EnrichedCategory.comp W Y Z)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (W ⟶[V] X) (CategoryTheory.EnrichedCategory.comp X Y Z)) (CategoryTheory.EnrichedCategory.comp W X Z)
• CategoryTheory.e_assoc'_assoc 📋 Mathlib.CategoryTheory.Enriched.Basic
  (V : Type v) [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] (W X Y Z : C) {Z✝ : V} (h : (W ⟶[V] Z) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (W ⟶[V] X) (X ⟶[V] Y) (Y ⟶[V] Z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (W ⟶[V] X) (CategoryTheory.eComp V X Y Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V W X Z) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.eComp V W X Y) (Y ⟶[V] Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V W Y Z) h)
• CategoryTheory.e_assoc_assoc 📋 Mathlib.CategoryTheory.Enriched.Basic
  (V : Type v) [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] (W X Y Z : C) {Z✝ : V} (h : (W ⟶[V] Z) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (W ⟶[V] X) (X ⟶[V] Y) (Y ⟶[V] Z)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.eComp V W X Y) (Y ⟶[V] Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V W Y Z) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (W ⟶[V] X) (CategoryTheory.eComp V X Y Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V W X Z) h)
• CategoryTheory.EnrichedCategory.mk 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} (Hom : C → C → V) (id : (X : C) → CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ Hom X X) (comp : (X Y Z : C) → CategoryTheory.MonoidalCategoryStruct.tensorObj (Hom X Y) (Hom Y Z) ⟶ Hom X Z) (id_comp : ∀ (X Y : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (Hom X Y)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (id X) (Hom X Y)) (comp X X Y)) = CategoryTheory.CategoryStruct.id (Hom X Y) := by cat_disch) (comp_id : ∀ (X Y : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (Hom X Y)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (Hom X Y) (id Y)) (comp X Y Y)) = CategoryTheory.CategoryStruct.id (Hom X Y) := by cat_disch) (assoc : ∀ (W X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (Hom W X) (Hom X Y) (Hom Y Z)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (comp W X Y) (Hom Y Z)) (comp W Y Z)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (Hom W X) (comp X Y Z)) (comp W X Z) := by cat_disch) : CategoryTheory.EnrichedCategory V C
• CategoryTheory.GradedNatTrans.naturality 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] {A : CategoryTheory.Center V} {F G : CategoryTheory.EnrichedFunctor V C D} (self : CategoryTheory.GradedNatTrans A F G) (X Y : C) : CategoryTheory.CategoryStruct.comp (A.snd.β (X ⟶[V] Y)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map X Y) (self.app Y)) (CategoryTheory.eComp V (F.obj X) (F.obj Y) (G.obj Y))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (self.app X) (G.map X Y)) (CategoryTheory.eComp V (F.obj X) (G.obj X) (G.obj Y))
• CategoryTheory.GradedNatTrans.mk 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] {A : CategoryTheory.Center V} {F G : CategoryTheory.EnrichedFunctor V C D} (app : (X : C) → A.fst ⟶ F.obj X ⟶[V] G.obj X) (naturality : ∀ (X Y : C), CategoryTheory.CategoryStruct.comp (A.snd.β (X ⟶[V] Y)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map X Y) (app Y)) (CategoryTheory.eComp V (F.obj X) (F.obj Y) (G.obj Y))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (app X) (G.map X Y)) (CategoryTheory.eComp V (F.obj X) (G.obj X) (G.obj Y))) : CategoryTheory.GradedNatTrans A F G
• CategoryTheory.GradedNatTrans.naturality_assoc 📋 Mathlib.CategoryTheory.Enriched.Basic
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u₁} [CategoryTheory.EnrichedCategory V C] {D : Type u₂} [CategoryTheory.EnrichedCategory V D] {A : CategoryTheory.Center V} {F G : CategoryTheory.EnrichedFunctor V C D} (self : CategoryTheory.GradedNatTrans A F G) (X Y : C) {Z : V} (h : (F.obj X ⟶[V] G.obj Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp (A.snd.β (X ⟶[V] Y)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map X Y) (self.app Y)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V (F.obj X) (F.obj Y) (G.obj Y)) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (self.app X) (G.map X Y)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V (F.obj X) (G.obj X) (G.obj Y)) h)
• CategoryTheory.EnrichedOrdinaryCategory.toEnrichedCategory 📋 Mathlib.CategoryTheory.Enriched.Ordinary.Basic
  {V : Type u'} {inst✝ : CategoryTheory.Category.{v', u'} V} {inst✝¹ : CategoryTheory.MonoidalCategory V} {C : Type u} {inst✝² : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.EnrichedOrdinaryCategory V C] : CategoryTheory.EnrichedCategory V C
• CategoryTheory.ForgetEnrichment.enrichedOrdinaryCategory 📋 Mathlib.CategoryTheory.Enriched.Ordinary.Basic
  (V : Type u') [CategoryTheory.Category.{v', u'} V] [CategoryTheory.MonoidalCategory V] {D : Type u_1} [CategoryTheory.EnrichedCategory V D] : CategoryTheory.EnrichedOrdinaryCategory V (CategoryTheory.ForgetEnrichment V D)
• CategoryTheory.TransportEnrichment.forgetEnrichmentEquiv 📋 Mathlib.CategoryTheory.Enriched.Ordinary.Basic
  {V : Type u'} [CategoryTheory.Category.{v', u'} V] [CategoryTheory.MonoidalCategory V] {W : Type u''} [CategoryTheory.Category.{v'', u''} W] [CategoryTheory.MonoidalCategory W] (F : CategoryTheory.Functor V W) [F.LaxMonoidal] (D : Type u) [CategoryTheory.EnrichedCategory V D] (e : (v : V) → (CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v) ≃ (CategoryTheory.MonoidalCategoryStruct.tensorUnit W ⟶ F.obj v)) (h : ∀ (v : V) (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v), (e v) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map f)) : CategoryTheory.TransportEnrichment F (CategoryTheory.ForgetEnrichment V D) ≌ CategoryTheory.ForgetEnrichment W (CategoryTheory.TransportEnrichment F D)
• CategoryTheory.TransportEnrichment.forgetEnrichmentEquivFunctor 📋 Mathlib.CategoryTheory.Enriched.Ordinary.Basic
  {V : Type u'} [CategoryTheory.Category.{v', u'} V] [CategoryTheory.MonoidalCategory V] {W : Type u''} [CategoryTheory.Category.{v'', u''} W] [CategoryTheory.MonoidalCategory W] (F : CategoryTheory.Functor V W) [F.LaxMonoidal] (D : Type u) [CategoryTheory.EnrichedCategory V D] (e : (v : V) → (CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v) ≃ (CategoryTheory.MonoidalCategoryStruct.tensorUnit W ⟶ F.obj v)) (h : ∀ (v : V) (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v), (e v) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map f)) : CategoryTheory.Functor (CategoryTheory.TransportEnrichment F (CategoryTheory.ForgetEnrichment V D)) (CategoryTheory.ForgetEnrichment W (CategoryTheory.TransportEnrichment F D))
• CategoryTheory.TransportEnrichment.forgetEnrichmentEquivInverse 📋 Mathlib.CategoryTheory.Enriched.Ordinary.Basic
  {V : Type u'} [CategoryTheory.Category.{v', u'} V] [CategoryTheory.MonoidalCategory V] {W : Type u''} [CategoryTheory.Category.{v'', u''} W] [CategoryTheory.MonoidalCategory W] (F : CategoryTheory.Functor V W) [F.LaxMonoidal] (D : Type u) [CategoryTheory.EnrichedCategory V D] (e : (v : V) → (CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v) ≃ (CategoryTheory.MonoidalCategoryStruct.tensorUnit W ⟶ F.obj v)) (h : ∀ (v : V) (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v), (e v) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map f)) : CategoryTheory.Functor (CategoryTheory.ForgetEnrichment W (CategoryTheory.TransportEnrichment F D)) (CategoryTheory.TransportEnrichment F (CategoryTheory.ForgetEnrichment V D))
• CategoryTheory.TransportEnrichment.forgetEnrichmentEquivInverse_obj 📋 Mathlib.CategoryTheory.Enriched.Ordinary.Basic
  {V : Type u'} [CategoryTheory.Category.{v', u'} V] [CategoryTheory.MonoidalCategory V] {W : Type u''} [CategoryTheory.Category.{v'', u''} W] [CategoryTheory.MonoidalCategory W] (F : CategoryTheory.Functor V W) [F.LaxMonoidal] (D : Type u) [CategoryTheory.EnrichedCategory V D] (e : (v : V) → (CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v) ≃ (CategoryTheory.MonoidalCategoryStruct.tensorUnit W ⟶ F.obj v)) (h : ∀ (v : V) (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v), (e v) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map f)) (X : CategoryTheory.ForgetEnrichment W (CategoryTheory.TransportEnrichment F D)) : (CategoryTheory.TransportEnrichment.forgetEnrichmentEquivInverse F D e h).obj X = CategoryTheory.ForgetEnrichment.of V (CategoryTheory.ForgetEnrichment.to W X)
• CategoryTheory.TransportEnrichment.forgetEnrichmentEquivFunctor_obj 📋 Mathlib.CategoryTheory.Enriched.Ordinary.Basic
  {V : Type u'} [CategoryTheory.Category.{v', u'} V] [CategoryTheory.MonoidalCategory V] {W : Type u''} [CategoryTheory.Category.{v'', u''} W] [CategoryTheory.MonoidalCategory W] (F : CategoryTheory.Functor V W) [F.LaxMonoidal] (D : Type u) [CategoryTheory.EnrichedCategory V D] (e : (v : V) → (CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v) ≃ (CategoryTheory.MonoidalCategoryStruct.tensorUnit W ⟶ F.obj v)) (h : ∀ (v : V) (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v), (e v) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map f)) (X : CategoryTheory.TransportEnrichment F (CategoryTheory.ForgetEnrichment V D)) : (CategoryTheory.TransportEnrichment.forgetEnrichmentEquivFunctor F D e h).obj X = CategoryTheory.ForgetEnrichment.of W X
• CategoryTheory.TransportEnrichment.forgetEnrichmentEquiv_functor 📋 Mathlib.CategoryTheory.Enriched.Ordinary.Basic
  {V : Type u'} [CategoryTheory.Category.{v', u'} V] [CategoryTheory.MonoidalCategory V] {W : Type u''} [CategoryTheory.Category.{v'', u''} W] [CategoryTheory.MonoidalCategory W] (F : CategoryTheory.Functor V W) [F.LaxMonoidal] (D : Type u) [CategoryTheory.EnrichedCategory V D] (e : (v : V) → (CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v) ≃ (CategoryTheory.MonoidalCategoryStruct.tensorUnit W ⟶ F.obj v)) (h : ∀ (v : V) (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v), (e v) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map f)) : (CategoryTheory.TransportEnrichment.forgetEnrichmentEquiv F D e h).functor = CategoryTheory.TransportEnrichment.forgetEnrichmentEquivFunctor F D e h
• CategoryTheory.TransportEnrichment.forgetEnrichmentEquiv_inverse 📋 Mathlib.CategoryTheory.Enriched.Ordinary.Basic
  {V : Type u'} [CategoryTheory.Category.{v', u'} V] [CategoryTheory.MonoidalCategory V] {W : Type u''} [CategoryTheory.Category.{v'', u''} W] [CategoryTheory.MonoidalCategory W] (F : CategoryTheory.Functor V W) [F.LaxMonoidal] (D : Type u) [CategoryTheory.EnrichedCategory V D] (e : (v : V) → (CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v) ≃ (CategoryTheory.MonoidalCategoryStruct.tensorUnit W ⟶ F.obj v)) (h : ∀ (v : V) (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v), (e v) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map f)) : (CategoryTheory.TransportEnrichment.forgetEnrichmentEquiv F D e h).inverse = CategoryTheory.TransportEnrichment.forgetEnrichmentEquivInverse F D e h
• CategoryTheory.EnrichedOrdinaryCategory.mk 📋 Mathlib.CategoryTheory.Enriched.Ordinary.Basic
  {V : Type u'} [CategoryTheory.Category.{v', u'} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.Category.{v, u} C] [toEnrichedCategory : CategoryTheory.EnrichedCategory V C] (homEquiv : {X Y : C} → (X ⟶ Y) ≃ (CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ X ⟶[V] Y)) (homEquiv_id : ∀ (X : C), homEquiv (CategoryTheory.CategoryStruct.id X) = CategoryTheory.eId V X := by cat_disch) (homEquiv_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), homEquiv (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (homEquiv f) (homEquiv g)) (CategoryTheory.eComp V X Y Z)) := by cat_disch) : CategoryTheory.EnrichedOrdinaryCategory V C
• CategoryTheory.TransportEnrichment.forgetEnrichmentEquiv_unitIso 📋 Mathlib.CategoryTheory.Enriched.Ordinary.Basic
  {V : Type u'} [CategoryTheory.Category.{v', u'} V] [CategoryTheory.MonoidalCategory V] {W : Type u''} [CategoryTheory.Category.{v'', u''} W] [CategoryTheory.MonoidalCategory W] (F : CategoryTheory.Functor V W) [F.LaxMonoidal] (D : Type u) [CategoryTheory.EnrichedCategory V D] (e : (v : V) → (CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v) ≃ (CategoryTheory.MonoidalCategoryStruct.tensorUnit W ⟶ F.obj v)) (h : ∀ (v : V) (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v), (e v) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map f)) : (CategoryTheory.TransportEnrichment.forgetEnrichmentEquiv F D e h).unitIso = CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.TransportEnrichment F (CategoryTheory.ForgetEnrichment V D))).obj x)) ⋯
• CategoryTheory.TransportEnrichment.forgetEnrichmentEquivFunctor_map 📋 Mathlib.CategoryTheory.Enriched.Ordinary.Basic
  {V : Type u'} [CategoryTheory.Category.{v', u'} V] [CategoryTheory.MonoidalCategory V] {W : Type u''} [CategoryTheory.Category.{v'', u''} W] [CategoryTheory.MonoidalCategory W] (F : CategoryTheory.Functor V W) [F.LaxMonoidal] (D : Type u) [CategoryTheory.EnrichedCategory V D] (e : (v : V) → (CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v) ≃ (CategoryTheory.MonoidalCategoryStruct.tensorUnit W ⟶ F.obj v)) (h : ∀ (v : V) (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v), (e v) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map f)) {X Y : CategoryTheory.TransportEnrichment F (CategoryTheory.ForgetEnrichment V D)} (f : X ⟶ Y) : (CategoryTheory.TransportEnrichment.forgetEnrichmentEquivFunctor F D e h).map f = CategoryTheory.ForgetEnrichment.homOf W ((e (X ⟶[V] Y)) (CategoryTheory.ForgetEnrichment.homTo V f))
• CategoryTheory.TransportEnrichment.forgetEnrichmentEquiv_counitIso 📋 Mathlib.CategoryTheory.Enriched.Ordinary.Basic
  {V : Type u'} [CategoryTheory.Category.{v', u'} V] [CategoryTheory.MonoidalCategory V] {W : Type u''} [CategoryTheory.Category.{v'', u''} W] [CategoryTheory.MonoidalCategory W] (F : CategoryTheory.Functor V W) [F.LaxMonoidal] (D : Type u) [CategoryTheory.EnrichedCategory V D] (e : (v : V) → (CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v) ≃ (CategoryTheory.MonoidalCategoryStruct.tensorUnit W ⟶ F.obj v)) (h : ∀ (v : V) (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v), (e v) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map f)) : (CategoryTheory.TransportEnrichment.forgetEnrichmentEquiv F D e h).counitIso = CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.Iso.refl (((CategoryTheory.TransportEnrichment.forgetEnrichmentEquivInverse F D e h).comp (CategoryTheory.TransportEnrichment.forgetEnrichmentEquivFunctor F D e h)).obj x)) ⋯
• CategoryTheory.TransportEnrichment.forgetEnrichmentEquivInverse_map 📋 Mathlib.CategoryTheory.Enriched.Ordinary.Basic
  {V : Type u'} [CategoryTheory.Category.{v', u'} V] [CategoryTheory.MonoidalCategory V] {W : Type u''} [CategoryTheory.Category.{v'', u''} W] [CategoryTheory.MonoidalCategory W] (F : CategoryTheory.Functor V W) [F.LaxMonoidal] (D : Type u) [CategoryTheory.EnrichedCategory V D] (e : (v : V) → (CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v) ≃ (CategoryTheory.MonoidalCategoryStruct.tensorUnit W ⟶ F.obj v)) (h : ∀ (v : V) (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v), (e v) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map f)) {X✝ Y✝ : CategoryTheory.ForgetEnrichment W (CategoryTheory.TransportEnrichment F D)} (f : X✝ ⟶ Y✝) : (CategoryTheory.TransportEnrichment.forgetEnrichmentEquivInverse F D e h).map f = CategoryTheory.ForgetEnrichment.homOf V ((e (CategoryTheory.ForgetEnrichment.to W X✝ ⟶[V] CategoryTheory.ForgetEnrichment.to W Y✝)).symm (CategoryTheory.ForgetEnrichment.homTo W f))
• CategoryTheory.CatEnriched.instBicategory 📋 Mathlib.CategoryTheory.Bicategory.CatEnriched
  {C : Type u_1} [CategoryTheory.EnrichedCategory CategoryTheory.Cat C] : CategoryTheory.Bicategory (CategoryTheory.CatEnriched C)
• CategoryTheory.CatEnriched.instCategory 📋 Mathlib.CategoryTheory.Bicategory.CatEnriched
  {C : Type u_1} [CategoryTheory.EnrichedCategory CategoryTheory.Cat C] : CategoryTheory.Category.{u_2, u_1} (CategoryTheory.CatEnriched C)
• CategoryTheory.CatEnriched.instCategoryStruct 📋 Mathlib.CategoryTheory.Bicategory.CatEnriched
  {C : Type u_1} [CategoryTheory.EnrichedCategory CategoryTheory.Cat C] : CategoryTheory.CategoryStruct.{u_2, u_1} (CategoryTheory.CatEnriched C)
• CategoryTheory.CatEnriched.instStrict 📋 Mathlib.CategoryTheory.Bicategory.CatEnriched
  {C : Type u_1} [CategoryTheory.EnrichedCategory CategoryTheory.Cat C] : CategoryTheory.Bicategory.Strict (CategoryTheory.CatEnriched C)
• CategoryTheory.CatEnriched.instEnrichedCategoryCat 📋 Mathlib.CategoryTheory.Bicategory.CatEnriched
  {C : Type u_1} [CategoryTheory.EnrichedCategory CategoryTheory.Cat C] : CategoryTheory.EnrichedCategory CategoryTheory.Cat (CategoryTheory.CatEnriched C)
• CategoryTheory.CatEnriched.instEnrichedOrdinaryCategoryCat 📋 Mathlib.CategoryTheory.Bicategory.CatEnriched
  {C : Type u_1} [CategoryTheory.EnrichedCategory CategoryTheory.Cat C] : CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat (CategoryTheory.CatEnriched C)
• CategoryTheory.CatEnrichedOrdinary.instEnrichedCategoryCat 📋 Mathlib.CategoryTheory.Bicategory.CatEnriched
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C] : CategoryTheory.EnrichedCategory CategoryTheory.Cat (CategoryTheory.CatEnrichedOrdinary C)
• CategoryTheory.CatEnriched.instCategoryHom 📋 Mathlib.CategoryTheory.Bicategory.CatEnriched
  {C : Type u_1} [CategoryTheory.EnrichedCategory CategoryTheory.Cat C] {X Y : CategoryTheory.CatEnriched C} : CategoryTheory.Category.{u_3, u_2} (X ⟶ Y)
• CategoryTheory.CatEnriched.id_eq 📋 Mathlib.CategoryTheory.Bicategory.CatEnriched
  {C : Type u_1} [CategoryTheory.EnrichedCategory CategoryTheory.Cat C] (X : CategoryTheory.CatEnriched C) : CategoryTheory.CategoryStruct.id X = (CategoryTheory.eId CategoryTheory.Cat X).toFunctor.obj { down := { as := () } }
• CategoryTheory.CatEnriched.hComp 📋 Mathlib.CategoryTheory.Bicategory.CatEnriched
  {C : Type u_1} [CategoryTheory.EnrichedCategory CategoryTheory.Cat C] {a b c : CategoryTheory.CatEnriched C} {f f' : a ⟶ b} {g g' : b ⟶ c} (η : f ⟶ f') (θ : g ⟶ g') : CategoryTheory.CategoryStruct.comp f g ⟶ CategoryTheory.CategoryStruct.comp f' g'
• CategoryTheory.CatEnriched.id_hComp_id 📋 Mathlib.CategoryTheory.Bicategory.CatEnriched
  {C : Type u_1} [CategoryTheory.EnrichedCategory CategoryTheory.Cat C] {a b c : CategoryTheory.CatEnriched C} (f : a ⟶ b) (g : b ⟶ c) : CategoryTheory.CatEnriched.hComp (CategoryTheory.CategoryStruct.id f) (CategoryTheory.CategoryStruct.id g) = CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f g)
• CategoryTheory.CatEnriched.hComp_id_heq 📋 Mathlib.CategoryTheory.Bicategory.CatEnriched
  {C : Type u_1} [CategoryTheory.EnrichedCategory CategoryTheory.Cat C] {a b : CategoryTheory.CatEnriched C} {f f' : a ⟶ b} (η : f ⟶ f') : CategoryTheory.CatEnriched.hComp η (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id b)) ≍ η
• CategoryTheory.CatEnriched.id_hComp_heq 📋 Mathlib.CategoryTheory.Bicategory.CatEnriched
  {C : Type u_1} [CategoryTheory.EnrichedCategory CategoryTheory.Cat C] {a b : CategoryTheory.CatEnriched C} {f f' : a ⟶ b} (η : f ⟶ f') : CategoryTheory.CatEnriched.hComp (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id a)) η ≍ η
• CategoryTheory.CatEnriched.comp_eq 📋 Mathlib.CategoryTheory.Bicategory.CatEnriched
  {C : Type u_1} [CategoryTheory.EnrichedCategory CategoryTheory.Cat C] {X Y Z : CategoryTheory.CatEnriched C} (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp f g = (CategoryTheory.eComp CategoryTheory.Cat X Y Z).toFunctor.obj (f, g)
• CategoryTheory.CatEnriched.eqToHom_hComp_eqToHom 📋 Mathlib.CategoryTheory.Bicategory.CatEnriched
  {C : Type u_1} [CategoryTheory.EnrichedCategory CategoryTheory.Cat C] {a b c : CategoryTheory.CatEnriched C} {f f' : a ⟶ b} (α : f = f') {g g' : b ⟶ c} (β : g = g') : CategoryTheory.CatEnriched.hComp (CategoryTheory.eqToHom α) (CategoryTheory.eqToHom β) = CategoryTheory.eqToHom ⋯
• CategoryTheory.CatEnriched.hComp_assoc_heq 📋 Mathlib.CategoryTheory.Bicategory.CatEnriched
  {C : Type u_1} [CategoryTheory.EnrichedCategory CategoryTheory.Cat C] {a b c d : CategoryTheory.CatEnriched C} {f f' : a ⟶ b} {g g' : b ⟶ c} {h h' : c ⟶ d} (η : f ⟶ f') (θ : g ⟶ g') (κ : h ⟶ h') : CategoryTheory.CatEnriched.hComp (CategoryTheory.CatEnriched.hComp η θ) κ ≍ CategoryTheory.CatEnriched.hComp η (CategoryTheory.CatEnriched.hComp θ κ)
• CategoryTheory.CatEnriched.hComp_comp 📋 Mathlib.CategoryTheory.Bicategory.CatEnriched
  {C : Type u_1} [CategoryTheory.EnrichedCategory CategoryTheory.Cat C] {a b c : CategoryTheory.CatEnriched C} {f₁ f₂ f₃ : a ⟶ b} {g₁ g₂ g₃ : b ⟶ c} (η : f₁ ⟶ f₂) (η' : f₂ ⟶ f₃) (θ : g₁ ⟶ g₂) (θ' : g₂ ⟶ g₃) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CatEnriched.hComp η θ) (CategoryTheory.CatEnriched.hComp η' θ') = CategoryTheory.CatEnriched.hComp (CategoryTheory.CategoryStruct.comp η η') (CategoryTheory.CategoryStruct.comp θ θ')
• CategoryTheory.CatEnriched.hComp_id 📋 Mathlib.CategoryTheory.Bicategory.CatEnriched
  {C : Type u_1} [CategoryTheory.EnrichedCategory CategoryTheory.Cat C] {a b : CategoryTheory.CatEnriched C} {f f' : a ⟶ b} (η : f ⟶ f') : CategoryTheory.CatEnriched.hComp η (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id b)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp η (CategoryTheory.eqToHom ⋯))
• CategoryTheory.CatEnriched.id_hComp 📋 Mathlib.CategoryTheory.Bicategory.CatEnriched
  {C : Type u_1} [CategoryTheory.EnrichedCategory CategoryTheory.Cat C] {a b : CategoryTheory.CatEnriched C} {f f' : a ⟶ b} (η : f ⟶ f') : CategoryTheory.CatEnriched.hComp (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id a)) η = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp η (CategoryTheory.eqToHom ⋯))
• CategoryTheory.CatEnriched.hComp_assoc 📋 Mathlib.CategoryTheory.Bicategory.CatEnriched
  {C : Type u_1} [CategoryTheory.EnrichedCategory CategoryTheory.Cat C] {a b c d : CategoryTheory.CatEnriched C} {f f' : a ⟶ b} {g g' : b ⟶ c} {h h' : c ⟶ d} (η : f ⟶ f') (θ : g ⟶ g') (κ : h ⟶ h') : CategoryTheory.CatEnriched.hComp (CategoryTheory.CatEnriched.hComp η θ) κ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CatEnriched.hComp η (CategoryTheory.CatEnriched.hComp θ κ)) (CategoryTheory.eqToHom ⋯))
• CategoryTheory.Enriched.Functor.instEnrichedCategoryFunctorType 📋 Mathlib.CategoryTheory.Functor.FunctorHom
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] : CategoryTheory.EnrichedCategory (CategoryTheory.Functor C (Type (max v' v u))) (CategoryTheory.Functor C D)
• CategoryTheory.SimplicialObject.instEnrichedCategorySSet 📋 Mathlib.AlgebraicTopology.SimplicialCategory.SimplicialObject
  {D : Type u} [CategoryTheory.Category.{v, u} D] : CategoryTheory.EnrichedCategory SSet (CategoryTheory.SimplicialObject D)
• CategoryTheory.EnrichedCat.of 📋 Mathlib.CategoryTheory.Enriched.EnrichedCat
  (V : Type v) [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] (C : Type u) [CategoryTheory.EnrichedCategory V C] : CategoryTheory.EnrichedCat V
• CategoryTheory.EnrichedCat.str 📋 Mathlib.CategoryTheory.Enriched.EnrichedCat
  (V : Type v) [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] (C : CategoryTheory.EnrichedCat V) : CategoryTheory.EnrichedCategory V ↑C
• CategoryTheory.EnrichedCat.leftUnitor 📋 Mathlib.CategoryTheory.Enriched.EnrichedCat
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.EnrichedCategory V C] {D : Type u₁} [CategoryTheory.EnrichedCategory V D] (F : CategoryTheory.EnrichedFunctor V C D) : CategoryTheory.EnrichedFunctor.comp V (CategoryTheory.EnrichedFunctor.id V C) F ≅ F
• CategoryTheory.EnrichedCat.rightUnitor 📋 Mathlib.CategoryTheory.Enriched.EnrichedCat
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.EnrichedCategory V C] {D : Type u₁} [CategoryTheory.EnrichedCategory V D] (F : CategoryTheory.EnrichedFunctor V C D) : CategoryTheory.EnrichedFunctor.comp V F (CategoryTheory.EnrichedFunctor.id V D) ≅ F
• CategoryTheory.EnrichedCat.associator 📋 Mathlib.CategoryTheory.Enriched.EnrichedCat
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.EnrichedCategory V C] {D : Type u₁} [CategoryTheory.EnrichedCategory V D] {E : Type u₂} [CategoryTheory.EnrichedCategory V E] {E' : Type u₃} [CategoryTheory.EnrichedCategory V E'] (F : CategoryTheory.EnrichedFunctor V C D) (G : CategoryTheory.EnrichedFunctor V D E) (H : CategoryTheory.EnrichedFunctor V E E') : CategoryTheory.EnrichedFunctor.comp V (CategoryTheory.EnrichedFunctor.comp V F G) H ≅ CategoryTheory.EnrichedFunctor.comp V F (CategoryTheory.EnrichedFunctor.comp V G H)
• CategoryTheory.EnrichedCat.whiskerLeft 📋 Mathlib.CategoryTheory.Enriched.EnrichedCat
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.EnrichedCategory V C] {D : Type u₁} [CategoryTheory.EnrichedCategory V D] {E : Type u₂} [CategoryTheory.EnrichedCategory V E] (F : CategoryTheory.EnrichedFunctor V C D) {G H : CategoryTheory.EnrichedFunctor V D E} (α : G ⟶ H) : CategoryTheory.EnrichedFunctor.comp V F G ⟶ CategoryTheory.EnrichedFunctor.comp V F H
• CategoryTheory.EnrichedCat.whiskerRight 📋 Mathlib.CategoryTheory.Enriched.EnrichedCat
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.EnrichedCategory V C] {D : Type u₁} [CategoryTheory.EnrichedCategory V D] {E : Type u₂} [CategoryTheory.EnrichedCategory V E] {F G : CategoryTheory.EnrichedFunctor V C D} (α : F ⟶ G) (H : CategoryTheory.EnrichedFunctor V D E) : CategoryTheory.EnrichedFunctor.comp V F H ⟶ CategoryTheory.EnrichedFunctor.comp V G H
• CategoryTheory.EnrichedCat.leftUnitor_hom_out_app 📋 Mathlib.CategoryTheory.Enriched.EnrichedCat
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.EnrichedCategory V C] {D : Type u₁} [CategoryTheory.EnrichedCategory V D] (F : CategoryTheory.EnrichedFunctor V C D) (X : CategoryTheory.ForgetEnrichment V C) : (CategoryTheory.EnrichedCat.leftUnitor F).hom.out.app X = CategoryTheory.CategoryStruct.id (CategoryTheory.ForgetEnrichment.of V (F.obj (CategoryTheory.ForgetEnrichment.to V X)))
• CategoryTheory.EnrichedCat.leftUnitor_inv_out_app 📋 Mathlib.CategoryTheory.Enriched.EnrichedCat
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.EnrichedCategory V C] {D : Type u₁} [CategoryTheory.EnrichedCategory V D] (F : CategoryTheory.EnrichedFunctor V C D) (X : CategoryTheory.ForgetEnrichment V C) : (CategoryTheory.EnrichedCat.leftUnitor F).inv.out.app X = CategoryTheory.CategoryStruct.id (CategoryTheory.ForgetEnrichment.of V (F.obj (CategoryTheory.ForgetEnrichment.to V X)))
• CategoryTheory.EnrichedCat.rightUnitor_hom_out_app 📋 Mathlib.CategoryTheory.Enriched.EnrichedCat
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.EnrichedCategory V C] {D : Type u₁} [CategoryTheory.EnrichedCategory V D] (F : CategoryTheory.EnrichedFunctor V C D) (X : CategoryTheory.ForgetEnrichment V C) : (CategoryTheory.EnrichedCat.rightUnitor F).hom.out.app X = CategoryTheory.CategoryStruct.id (CategoryTheory.ForgetEnrichment.of V (F.obj (CategoryTheory.ForgetEnrichment.to V X)))
• CategoryTheory.EnrichedCat.rightUnitor_inv_out_app 📋 Mathlib.CategoryTheory.Enriched.EnrichedCat
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.EnrichedCategory V C] {D : Type u₁} [CategoryTheory.EnrichedCategory V D] (F : CategoryTheory.EnrichedFunctor V C D) (X : CategoryTheory.ForgetEnrichment V C) : (CategoryTheory.EnrichedCat.rightUnitor F).inv.out.app X = CategoryTheory.CategoryStruct.id (CategoryTheory.ForgetEnrichment.of V (F.obj (CategoryTheory.ForgetEnrichment.to V X)))
• CategoryTheory.EnrichedCat.whisker_exchange 📋 Mathlib.CategoryTheory.Enriched.EnrichedCat
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.EnrichedCategory V C] {D : Type u₁} [CategoryTheory.EnrichedCategory V D] {E : Type u₂} [CategoryTheory.EnrichedCategory V E] {F G : CategoryTheory.EnrichedFunctor V C D} {H I : CategoryTheory.EnrichedFunctor V D E} (α : F ⟶ G) (β : H ⟶ I) : CategoryTheory.CategoryStruct.comp (CategoryTheory.EnrichedCat.whiskerLeft F β) (CategoryTheory.EnrichedCat.whiskerRight α I) = CategoryTheory.CategoryStruct.comp (CategoryTheory.EnrichedCat.whiskerRight α H) (CategoryTheory.EnrichedCat.whiskerLeft G β)
• CategoryTheory.EnrichedCat.whiskerLeft_out_app 📋 Mathlib.CategoryTheory.Enriched.EnrichedCat
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.EnrichedCategory V C] {D : Type u₁} [CategoryTheory.EnrichedCategory V D] {E : Type u₂} [CategoryTheory.EnrichedCategory V E] (F : CategoryTheory.EnrichedFunctor V C D) {G H : CategoryTheory.EnrichedFunctor V D E} (α : G ⟶ H) (X : CategoryTheory.ForgetEnrichment V C) : (CategoryTheory.EnrichedCat.whiskerLeft F α).out.app X = α.out.app (CategoryTheory.ForgetEnrichment.of V (F.obj (CategoryTheory.ForgetEnrichment.to V X)))
• CategoryTheory.EnrichedCat.comp_whiskerRight 📋 Mathlib.CategoryTheory.Enriched.EnrichedCat
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.EnrichedCategory V C] {D : Type u₁} [CategoryTheory.EnrichedCategory V D] {E : Type u₂} [CategoryTheory.EnrichedCategory V E] {F G H : CategoryTheory.EnrichedFunctor V C D} (α : F ⟶ G) (β : G ⟶ H) (I : CategoryTheory.EnrichedFunctor V D E) : CategoryTheory.EnrichedCat.whiskerRight { out := CategoryTheory.CategoryStruct.comp α.out β.out } I = CategoryTheory.CategoryStruct.comp (CategoryTheory.EnrichedCat.whiskerRight α I) (CategoryTheory.EnrichedCat.whiskerRight β I)
• CategoryTheory.EnrichedCat.associator_hom_out_app 📋 Mathlib.CategoryTheory.Enriched.EnrichedCat
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.EnrichedCategory V C] {D : Type u₁} [CategoryTheory.EnrichedCategory V D] {E : Type u₂} [CategoryTheory.EnrichedCategory V E] {E' : Type u₃} [CategoryTheory.EnrichedCategory V E'] (F : CategoryTheory.EnrichedFunctor V C D) (G : CategoryTheory.EnrichedFunctor V D E) (H : CategoryTheory.EnrichedFunctor V E E') (X : CategoryTheory.ForgetEnrichment V C) : (CategoryTheory.EnrichedCat.associator F G H).hom.out.app X = CategoryTheory.CategoryStruct.id (CategoryTheory.ForgetEnrichment.of V (H.obj (G.obj (F.obj (CategoryTheory.ForgetEnrichment.to V X)))))
• CategoryTheory.EnrichedCat.associator_inv_out_app 📋 Mathlib.CategoryTheory.Enriched.EnrichedCat
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.EnrichedCategory V C] {D : Type u₁} [CategoryTheory.EnrichedCategory V D] {E : Type u₂} [CategoryTheory.EnrichedCategory V E] {E' : Type u₃} [CategoryTheory.EnrichedCategory V E'] (F : CategoryTheory.EnrichedFunctor V C D) (G : CategoryTheory.EnrichedFunctor V D E) (H : CategoryTheory.EnrichedFunctor V E E') (X : CategoryTheory.ForgetEnrichment V C) : (CategoryTheory.EnrichedCat.associator F G H).inv.out.app X = CategoryTheory.CategoryStruct.id (CategoryTheory.ForgetEnrichment.of V (H.obj (G.obj (F.obj (CategoryTheory.ForgetEnrichment.to V X)))))
• CategoryTheory.EnrichedCat.whiskerRight_out_app 📋 Mathlib.CategoryTheory.Enriched.EnrichedCat
  {V : Type v} [CategoryTheory.Category.{w, v} V] [CategoryTheory.MonoidalCategory V] {C : Type u} [CategoryTheory.EnrichedCategory V C] {D : Type u₁} [CategoryTheory.EnrichedCategory V D] {E : Type u₂} [CategoryTheory.EnrichedCategory V E] {F G : CategoryTheory.EnrichedFunctor V C D} (α : F ⟶ G) (H : CategoryTheory.EnrichedFunctor V D E) (X : CategoryTheory.ForgetEnrichment V C) : (CategoryTheory.EnrichedCat.whiskerRight α H).out.app X = CategoryTheory.ForgetEnrichment.homOf V (CategoryTheory.CategoryStruct.comp (CategoryTheory.ForgetEnrichment.homTo V (α.out.app X)) (H.map (F.obj (CategoryTheory.ForgetEnrichment.to V X)) (G.obj (CategoryTheory.ForgetEnrichment.to V X))))
• CategoryTheory.Enriched.FunctorCategory.functorEnrichedCategory 📋 Mathlib.CategoryTheory.Enriched.FunctorCategory
  (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] (C : Type u₂) [CategoryTheory.Category.{v₂, u₂} C] (J : Type u₃) [CategoryTheory.Category.{v₃, u₃} J] [CategoryTheory.EnrichedOrdinaryCategory V C] [∀ (F₁ F₂ : CategoryTheory.Functor J C), CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₂] : CategoryTheory.EnrichedCategory (CategoryTheory.Functor J V) (CategoryTheory.Functor J C)
• CategoryTheory.EnrichedCategory.opposite 📋 Mathlib.CategoryTheory.Enriched.Opposite
  (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] (C : Type u) [CategoryTheory.EnrichedCategory V C] : CategoryTheory.EnrichedCategory V Cᵒᵖ
• CategoryTheory.forgetEnrichmentOppositeEquivalence 📋 Mathlib.CategoryTheory.Enriched.Opposite
  (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] (C : Type u) [CategoryTheory.EnrichedCategory V C] : CategoryTheory.ForgetEnrichment V Cᵒᵖ ≌ (CategoryTheory.ForgetEnrichment V C)ᵒᵖ
• CategoryTheory.forgetEnrichmentOppositeEquivalence.functor 📋 Mathlib.CategoryTheory.Enriched.Opposite
  (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] (C : Type u) [CategoryTheory.EnrichedCategory V C] : CategoryTheory.Functor (CategoryTheory.ForgetEnrichment V Cᵒᵖ) (CategoryTheory.ForgetEnrichment V C)ᵒᵖ
• CategoryTheory.forgetEnrichmentOppositeEquivalence.inverse 📋 Mathlib.CategoryTheory.Enriched.Opposite
  (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] (C : Type u) [CategoryTheory.EnrichedCategory V C] : CategoryTheory.Functor (CategoryTheory.ForgetEnrichment V C)ᵒᵖ (CategoryTheory.ForgetEnrichment V Cᵒᵖ)
• CategoryTheory.forgetEnrichmentOppositeEquivalence_functor 📋 Mathlib.CategoryTheory.Enriched.Opposite
  (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] (C : Type u) [CategoryTheory.EnrichedCategory V C] : (CategoryTheory.forgetEnrichmentOppositeEquivalence V C).functor = CategoryTheory.forgetEnrichmentOppositeEquivalence.functor V C
• CategoryTheory.forgetEnrichmentOppositeEquivalence_inverse 📋 Mathlib.CategoryTheory.Enriched.Opposite
  (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] (C : Type u) [CategoryTheory.EnrichedCategory V C] : (CategoryTheory.forgetEnrichmentOppositeEquivalence V C).inverse = CategoryTheory.forgetEnrichmentOppositeEquivalence.inverse V C
• CategoryTheory.eComp_op_eq 📋 Mathlib.CategoryTheory.Enriched.Opposite
  (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] {C : Type u} [CategoryTheory.EnrichedCategory V C] (x y z : Cᵒᵖ) : CategoryTheory.eComp V z y x = CategoryTheory.CategoryStruct.comp (β_ (Opposite.unop y ⟶[V] Opposite.unop z) (Opposite.unop x ⟶[V] Opposite.unop y)).hom (CategoryTheory.eComp V (Opposite.unop x) (Opposite.unop y) (Opposite.unop z))
• CategoryTheory.eComp_op_eq_assoc 📋 Mathlib.CategoryTheory.Enriched.Opposite
  (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] {C : Type u} [CategoryTheory.EnrichedCategory V C] (x y z : Cᵒᵖ) {Z : V} (h : (z ⟶[V] x) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V z y x) h = CategoryTheory.CategoryStruct.comp (β_ (Opposite.unop y ⟶[V] Opposite.unop z) (Opposite.unop x ⟶[V] Opposite.unop y)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V (Opposite.unop x) (Opposite.unop y) (Opposite.unop z)) h)
• CategoryTheory.tensorHom_eComp_op_eq 📋 Mathlib.CategoryTheory.Enriched.Opposite
  (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] {C : Type u} [CategoryTheory.EnrichedCategory V C] {x y z : Cᵒᵖ} {v w : V} (f : v ⟶ z ⟶[V] y) (g : w ⟶ y ⟶[V] x) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) (CategoryTheory.eComp V z y x) = CategoryTheory.CategoryStruct.comp (β_ v w).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom g f) (CategoryTheory.eComp V (Opposite.unop x) (Opposite.unop y) (Opposite.unop z)))
• CategoryTheory.tensorHom_eComp_op_eq_assoc 📋 Mathlib.CategoryTheory.Enriched.Opposite
  (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] {C : Type u} [CategoryTheory.EnrichedCategory V C] {x y z : Cᵒᵖ} {v w : V} (f : v ⟶ z ⟶[V] y) (g : w ⟶ y ⟶[V] x) {Z : V} (h : (z ⟶[V] x) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V z y x) h) = CategoryTheory.CategoryStruct.comp (β_ v w).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom g f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V (Opposite.unop x) (Opposite.unop y) (Opposite.unop z)) h))
• CategoryTheory.forgetEnrichmentOppositeEquivalence_counitIso 📋 Mathlib.CategoryTheory.Enriched.Opposite
  (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] (C : Type u) [CategoryTheory.EnrichedCategory V C] : (CategoryTheory.forgetEnrichmentOppositeEquivalence V C).counitIso = CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.Iso.refl (((CategoryTheory.forgetEnrichmentOppositeEquivalence.inverse V C).comp (CategoryTheory.forgetEnrichmentOppositeEquivalence.functor V C)).obj x)) ⋯
• CategoryTheory.forgetEnrichmentOppositeEquivalence_unitIso 📋 Mathlib.CategoryTheory.Enriched.Opposite
  (V : Type u₁) [CategoryTheory.Category.{v₁, u₁} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.BraidedCategory V] (C : Type u) [CategoryTheory.EnrichedCategory V C] : (CategoryTheory.forgetEnrichmentOppositeEquivalence V C).unitIso = CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.ForgetEnrichment V Cᵒᵖ)).obj x)) ⋯
• CategoryTheory.MonoidalClosed.enrichedCategorySelf 📋 Mathlib.CategoryTheory.Monoidal.Closed.Enrichment
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalClosed C] : CategoryTheory.EnrichedCategory C 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 ce5dd8c