Theorems · Theorem · category theory

CategoryTheory.CommComon.mk.inj

∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} {X : C} {comon : CategoryTheory.ComonObj X}
  {comm : CategoryTheory.IsCommComonObj X} {X_1 : C} {comon_1 : CategoryTheory.ComonObj X_1}
  {comm_1 : CategoryTheory.IsCommComonObj X_1},
  { X := X, comon := comon, comm := comm } = { X := X_1, comon := comon_1, comm := comm_1 } → X = X_1 ∧ comon ≍ comon_1

Defined in

Mathlib.CategoryTheory.Monoidal.CommComon_

Cited by

1 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms