Theorems · Theorem · category theory

CategoryTheory.MonoidalCategory.DayConvolution.unit_uniqueUpToIso_hom

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  {F G : CategoryTheory.Functor C V} (h h' : CategoryTheory.MonoidalCategory.DayConvolution F G),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.unit F G)
      ((CategoryTheory.MonoidalCategory.tensor C).whiskerLeft (h.uniqueUpToIso h').hom) =
    CategoryTheory.MonoidalCategory.DayConvolution.unit F G

Defined in

Mathlib.CategoryTheory.Monoidal.DayConvolution

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.MonoidalCategory