cartesian

The free cartesian category, i.e. diagrams with copy and discard.

Summary

Diagram	A cartesian diagram is a symmetric diagram with Copy boxes.
Box	A cartesian box is a symmetric box in a cartesian diagram.
Swap	Symmetric swap in a cartesian diagram.
Copy	The copy of an atomic type x some n number of times.
Category	A cartesian category is a symmetric category with a method copy.
Functor	A cartesian functor is a symmetric functor that preserves copies.

Axioms

Coherence holds on the nose.

>>> x, y = Ty('x'), Ty('y')
>>> multicopy = Copy(x) @ Copy(y) >> Id(x) @ Swap(x, y) @ Id(y)
>>> assert Diagram.copy(x @ y) == multicopy

The axioms of cartesian categories cannot be checked in DisCoPy, we can draw them and check whether they hold for a given Functor.

>>> copy_l = Copy(x) >> Copy(x) @ Id(x)
>>> copy_r = Copy(x) >> Id(x) @ Copy(x)

>>> from discopy.drawing import Equation
>>> Equation(copy_l, copy_r, symbol="=").draw(
...     path="docs/_static/cartesian/associativity.png")

>>> delete = lambda x: Copy(x, n=0)
>>> counit_l = Copy(x) >> delete(x) @ Id(x)
>>> counit_r = Copy(x) >> Id(x) @ delete(x)
>>> Equation(counit_l, Id(x), counit_r, symbol="=").draw(
...     path="docs/_static/cartesian/counit.png")