Theorems · Theorem · category theory

CategoryTheory.TransportEnrichment.forgetEnrichmentEquiv_inverse

∀ {V : Type u'} [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {W : Type u''}
  [inst_2 : CategoryTheory.Category.{v'', u''} W] [inst_3 : CategoryTheory.MonoidalCategory W]
  (F : CategoryTheory.Functor V W) [inst_4 : F.LaxMonoidal] (D : Type u) [inst_5 : 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

Defined in

Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Cited by

0 results in Mathlib

Foundations

Depth 54 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.Functor.LaxMonoidalCategoryTheory.EnrichedCategory