Cartesian Categories as Copy-Discard Categories

Every cartesian monoidal category is a copy-discard category where:

• Copy is the diagonal map
• Discard is the unique map to terminal

Main results

• CopyDiscardCategory instance for cartesian monoidal categories
• All morphisms in cartesian categories are deterministic

Tags

cartesian, copy-discard, comonoid, symmetric monoidal

@[reducible, inline]

abbrev CategoryTheory.CartesianCopyDiscard.instComonObjOfCartesian {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (X : C) : ComonObj X

Provide ComonObj instances using the canonical cartesian comonoid structure.

Equations

• CategoryTheory.CartesianCopyDiscard.instComonObjOfCartesian X = ((CategoryTheory.cartesianComon C).obj X).comon

instance CategoryTheory.CartesianCopyDiscard.instIsCommComonObjOfCartesian {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (X : C) : IsCommComonObj X

Every object in a cartesian category has commutative comonoid structure.

@[reducible, inline]

abbrev CategoryTheory.CartesianCopyDiscard.ofCartesianMonoidalCategory {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] : CopyDiscardCategory C

Cartesian categories have copy-discard structure.

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.CartesianCopyDiscard.instDeterministic {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {X Y : C} (f : X ⟶ Y) : Deterministic f

In cartesian categories, every morphism is deterministic (preserves the comonoid structure).