Theorems · Theorem · category theory

CategoryTheory.NatTrans.tensor_naturality_assoc

∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.MonoidalCategory C]
  {F G F' G' : CategoryTheory.Functor J C} (α : F ⟶ F') (β : G ⟶ G') {X Y X' Y' : J} (f : X ⟶ Y) (g : X' ⟶ Y') {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (F'.obj Y) (G'.obj Y') ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map f) (G.map g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (α.app Y) (β.app Y')) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (α.app X) (β.app X'))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (F'.map f) (G'.map g)) h)

Defined in

Mathlib.CategoryTheory.Monoidal.Category

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.MonoidalCategory