Theorems · Theorem · category theory

CategoryTheory.WideSubcategory.whiskerRight_hom

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.MorphismProperty C)
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : P.IsMonoidalStable] {X₁ X₂ : CategoryTheory.WideSubcategory P}
  (f : X₁ ⟶ X₂) (c' : CategoryTheory.WideSubcategory P),
  (CategoryTheory.MonoidalCategoryStruct.whiskerRight f c').hom =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom c'.obj

Defined in

Mathlib.CategoryTheory.Monoidal.Widesubcategory

Cited by

0 results in Mathlib

Foundations

Depth 16 from the axioms · uses propext

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.MorphismProperty.IsMonoidalStable