# 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")
```