Loogle!

Result

Found 70 declarations mentioning CategoryTheory.ForgetEnrichment.

• 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.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.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.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.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.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.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.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.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.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.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.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.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.ForgetEnrichment.equiv 📋 Mathlib.CategoryTheory.Enriched.Ordinary.Basic
  (V : Type u') [CategoryTheory.Category.{v', u'} V] [CategoryTheory.MonoidalCategory V] {D : Type u''} [CategoryTheory.Category.{v'', u''} D] [CategoryTheory.EnrichedOrdinaryCategory V D] : CategoryTheory.ForgetEnrichment V D ≌ D
• CategoryTheory.ForgetEnrichment.equivFunctor 📋 Mathlib.CategoryTheory.Enriched.Ordinary.Basic
  (V : Type u') [CategoryTheory.Category.{v', u'} V] [CategoryTheory.MonoidalCategory V] (D : Type u'') [CategoryTheory.Category.{v'', u''} D] [CategoryTheory.EnrichedOrdinaryCategory V D] : CategoryTheory.Functor (CategoryTheory.ForgetEnrichment V D) D
• CategoryTheory.ForgetEnrichment.equivInverse 📋 Mathlib.CategoryTheory.Enriched.Ordinary.Basic
  (V : Type u') [CategoryTheory.Category.{v', u'} V] [CategoryTheory.MonoidalCategory V] (D : Type u'') [CategoryTheory.Category.{v'', u''} D] [CategoryTheory.EnrichedOrdinaryCategory V D] : CategoryTheory.Functor D (CategoryTheory.ForgetEnrichment V D)
• CategoryTheory.ForgetEnrichment.equivFunctor_obj 📋 Mathlib.CategoryTheory.Enriched.Ordinary.Basic
  (V : Type u') [CategoryTheory.Category.{v', u'} V] [CategoryTheory.MonoidalCategory V] (D : Type u'') [CategoryTheory.Category.{v'', u''} D] [CategoryTheory.EnrichedOrdinaryCategory V D] (X : CategoryTheory.ForgetEnrichment V D) : (CategoryTheory.ForgetEnrichment.equivFunctor V D).obj X = CategoryTheory.ForgetEnrichment.to V X
• CategoryTheory.ForgetEnrichment.equivInverse_obj 📋 Mathlib.CategoryTheory.Enriched.Ordinary.Basic
  (V : Type u') [CategoryTheory.Category.{v', u'} V] [CategoryTheory.MonoidalCategory V] (D : Type u'') [CategoryTheory.Category.{v'', u''} D] [CategoryTheory.EnrichedOrdinaryCategory V D] (X : D) : (CategoryTheory.ForgetEnrichment.equivInverse V D).obj X = CategoryTheory.ForgetEnrichment.of V X
• CategoryTheory.ForgetEnrichment.equiv_functor 📋 Mathlib.CategoryTheory.Enriched.Ordinary.Basic
  (V : Type u') [CategoryTheory.Category.{v', u'} V] [CategoryTheory.MonoidalCategory V] {D : Type u''} [CategoryTheory.Category.{v'', u''} D] [CategoryTheory.EnrichedOrdinaryCategory V D] : (CategoryTheory.ForgetEnrichment.equiv V).functor = CategoryTheory.ForgetEnrichment.equivFunctor V D
• CategoryTheory.ForgetEnrichment.equiv_inverse 📋 Mathlib.CategoryTheory.Enriched.Ordinary.Basic
  (V : Type u') [CategoryTheory.Category.{v', u'} V] [CategoryTheory.MonoidalCategory V] {D : Type u''} [CategoryTheory.Category.{v'', u''} D] [CategoryTheory.EnrichedOrdinaryCategory V D] : (CategoryTheory.ForgetEnrichment.equiv V).inverse = CategoryTheory.ForgetEnrichment.equivInverse V D
• CategoryTheory.ForgetEnrichment.equiv_counitIso 📋 Mathlib.CategoryTheory.Enriched.Ordinary.Basic
  (V : Type u') [CategoryTheory.Category.{v', u'} V] [CategoryTheory.MonoidalCategory V] {D : Type u''} [CategoryTheory.Category.{v'', u''} D] [CategoryTheory.EnrichedOrdinaryCategory V D] : (CategoryTheory.ForgetEnrichment.equiv V).counitIso = CategoryTheory.NatIso.ofComponents (fun X => CategoryTheory.Iso.refl (((CategoryTheory.ForgetEnrichment.equivInverse V D).comp (CategoryTheory.ForgetEnrichment.equivFunctor V D)).obj X)) ⋯
• CategoryTheory.ForgetEnrichment.equivInverse_map 📋 Mathlib.CategoryTheory.Enriched.Ordinary.Basic
  (V : Type u') [CategoryTheory.Category.{v', u'} V] [CategoryTheory.MonoidalCategory V] (D : Type u'') [CategoryTheory.Category.{v'', u''} D] [CategoryTheory.EnrichedOrdinaryCategory V D] {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) : (CategoryTheory.ForgetEnrichment.equivInverse V D).map f = CategoryTheory.ForgetEnrichment.homOf V ((CategoryTheory.eHomEquiv V) f)
• 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.ForgetEnrichment.equiv_unitIso 📋 Mathlib.CategoryTheory.Enriched.Ordinary.Basic
  (V : Type u') [CategoryTheory.Category.{v', u'} V] [CategoryTheory.MonoidalCategory V] {D : Type u''} [CategoryTheory.Category.{v'', u''} D] [CategoryTheory.EnrichedOrdinaryCategory V D] : (CategoryTheory.ForgetEnrichment.equiv V).unitIso = CategoryTheory.NatIso.ofComponents (fun X => CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.ForgetEnrichment V D)).obj X)) ⋯
• 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.ForgetEnrichment.equivFunctor_map 📋 Mathlib.CategoryTheory.Enriched.Ordinary.Basic
  (V : Type u') [CategoryTheory.Category.{v', u'} V] [CategoryTheory.MonoidalCategory V] (D : Type u'') [CategoryTheory.Category.{v'', u''} D] [CategoryTheory.EnrichedOrdinaryCategory V D] {X✝ Y✝ : CategoryTheory.ForgetEnrichment V D} (f : X✝ ⟶ Y✝) : (CategoryTheory.ForgetEnrichment.equivFunctor V D).map f = (CategoryTheory.eHomEquiv V).symm (CategoryTheory.ForgetEnrichment.homTo V f)
• 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))
• SSet.QCat.forgetEnrichment.equiv 📋 Mathlib.AlgebraicTopology.Quasicategory.StrictBicategory
  : CategoryTheory.ForgetEnrichment CategoryTheory.Cat SSet.QCat ≌ SSet.QCat
• 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.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.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.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)) ⋯

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