monoidal

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

Summary

Colour	A 0-cell, drawn using its matplotlib-compatible name, by default discopy.config.TRANSPARENT so that the page shows through.
Wire	A generating 1-cell with a colour on either side.
List	The free monoid on a generator_factory, i.e. lists of its instances with concatenation as tensor() and the empty list as unit.
Ty	A type is a composable path of objects with Ty.tensor() as concatenation.
Nat	Nat is a natural number n seen as a type with addition as tensor, i.e. the free monoid on one generator.
Dim	A dimension is a tuple of positive integers with product @ and unit Dim(1).
Layer	A layer is a tensor product of boxes and plumbing, i.e. non-empty types.
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 diagrams args inside and an optional pair of types dom and cod.
Functor	A monoidal functor is a functor that preserves the tensor product.
Equation	An cat.Equation of diagrams, i.e. with a draw() method.

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)