Theorems · Theorem · category theory

CategoryTheory.EnrichedCat.whiskerLeft_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 : 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)))

Defined in

Mathlib.CategoryTheory.Enriched.EnrichedCat

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.EnrichedCategoryCategoryTheory.EnrichedCategoryCategoryTheory.EnrichedCategory