Theorems · Theorem · category theory

CategoryTheory.ForgetEnrichment.homOf_comp

∀ {C : Type u₁} (W : Type v) [inst : CategoryTheory.Category.{w, v} W] [inst_1 : CategoryTheory.MonoidalCategory W]
  [inst_2 : 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)

Defined in

Mathlib.CategoryTheory.Enriched.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.EnrichedCategory