monoidal

The free (pre)monoidal category, i.e. planar diagrams.

Summary

Ty	A type is a tuple of objects with Ty.tensor() as concatenation.
PRO	A PRO is a natural number n seen as a type with addition as tensor.
Layer	A layer is a box in the middle of a pair of types left and right.
Diagram	A diagram is a tuple of composable layers inside with a pair of types dom and cod as domain and codomain.
Box	A box is a diagram with a name and the layer of just itself inside.
Sum	A sum is a tuple of diagrams terms with the same domain and codomain.
Bubble	A bubble is a box with a diagram arg inside and an optional pair of types dom and cod.
Category	A monoidal category is a category with a method tensor.
Functor	A monoidal functor is a functor that preserves the tensor product.
Whiskerable	Abstract class implementing the syntactic sugar @ for whiskering and parallel composition with some method tensor.

Axioms

We can check the axioms for Ty being a monoid.

>>> x, y, z, unit = Ty('x'), Ty('y'), Ty('z'), Ty()
>>> assert x @ unit == x == unit @ x
>>> assert (x @ y) @ z == x @ y @ z == x @ (y @ z)

We can check the axioms for dagger monoidal categories, up to interchanger.

>>> x, y, z, w = Ty('x'), Ty('y'), Ty('z'), Ty('w')
>>> f0, f1 = Box('f0', x, y), Box('f1', z, w)
>>> d = Id(x) @ f1 >> f0 @ Id(w)
>>> assert d == (f0 @ f1).interchange(0, 1)
>>> assert f0 @ f1 == d.interchange(0, 1)
>>> assert (f0 @ f1)[::-1][::-1] == f0 @ f1
>>> assert (f0 @ f1)[::-1].interchange(0, 1) == f0[::-1] @ f1[::-1]

We can check the Eckmann-Hilton argument, up to interchanger.

>>> s0, s1 = Box('s0', Ty(), Ty()), Box('s1', Ty(), Ty())
>>> assert s0 @ s1 == s0 >> s1 == (s1 @ s0).interchange(0, 1)
>>> assert s1 @ s0 == s1 >> s0 == (s0 @ s1).interchange(0, 1)