Theorems · Theorem · category theory

CategoryTheory.LaxMonoidalFunctor.Hom.mk.inj

∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory D}
  {F G : CategoryTheory.LaxMonoidalFunctor C D} {hom : F.toFunctor ⟶ G.toFunctor}
  {isMonoidal :
    autoParam (CategoryTheory.NatTrans.IsMonoidal hom) CategoryTheory.LaxMonoidalFunctor.Hom.isMonoidal._autoParam}
  {hom_1 : F.toFunctor ⟶ G.toFunctor}
  {isMonoidal_1 :
    autoParam (CategoryTheory.NatTrans.IsMonoidal hom_1) CategoryTheory.LaxMonoidalFunctor.Hom.isMonoidal._autoParam},
  { hom := hom, isMonoidal := isMonoidal } = { hom := hom_1, isMonoidal := isMonoidal_1 } → hom = hom_1

Defined in

Mathlib.CategoryTheory.Monoidal.NaturalTransformation

Cited by

1 results in Mathlib

Foundations

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