Theorems · Definition · category theory

CategoryTheory.CommComon.mk.noConfusion

{C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} →
      {inst_2 : CategoryTheory.BraidedCategory C} →
        {P : Sort u} →
          {X : C} →
            {comon : CategoryTheory.ComonObj X} →
              {comm : CategoryTheory.IsCommComonObj X} →
                {X' : C} →
                  {comon' : CategoryTheory.ComonObj X'} →
                    {comm' : CategoryTheory.IsCommComonObj X'} →
                      { X := X, comon := comon, comm := comm } = { X := X', comon := comon', comm := comm' } →
                        (X ≍ X' → comon ≍ comon' → P) → P

Defined in

Mathlib.CategoryTheory.Monoidal.CommComon_

Cited by

1 results in Mathlib

Foundations

Depth 9 from the axioms · uses no axioms