Theorems · Theorem · category theory

CategoryTheory.EnrichedCat.whiskerRight_out_app

∀ {V : Type v} [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_2 : CategoryTheory.EnrichedCategory V C] {D : Type u₁} [inst_3 : CategoryTheory.EnrichedCategory V D]
  {E : Type u₂} [inst_4 : 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))))

Defined in

Mathlib.CategoryTheory.Enriched.EnrichedCat

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.EnrichedCategoryCategoryTheory.EnrichedCategoryCategoryTheory.EnrichedCategory