Theorems · Definition · category theory

CategoryTheory.CartesianMonoidalCategory.mk.noConfusion

{C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {P : Sort u_1} →
      {toSemiCartesianMonoidalCategory : CategoryTheory.SemiCartesianMonoidalCategory C} →
        {tensorProductIsBinaryProduct :
            (X Y : C) →
              CategoryTheory.Limits.IsLimit
                (CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y)
                  (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y))} →
          {toSemiCartesianMonoidalCategory' : CategoryTheory.SemiCartesianMonoidalCategory C} →
            {tensorProductIsBinaryProduct' :
                (X Y : C) →
                  CategoryTheory.Limits.IsLimit
                    (CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y)
                      (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y))} →
              { toSemiCartesianMonoidalCategory := toSemiCartesianMonoidalCategory,
                    tensorProductIsBinaryProduct := tensorProductIsBinaryProduct } =
                  { toSemiCartesianMonoidalCategory := toSemiCartesianMonoidalCategory',
                    tensorProductIsBinaryProduct := tensorProductIsBinaryProduct' } →
                (toSemiCartesianMonoidalCategory ≍ toSemiCartesianMonoidalCategory' →
                    tensorProductIsBinaryProduct ≍ tensorProductIsBinaryProduct' → P) →
                  P

Defined in

Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Cited by

0 results in Mathlib

Foundations

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