monoidal#
Implements the free dagger monoidal category and strong dagger monoidal functors.
The syntax for diagrams is given by the following grammar:
diagram ::= Box(name, dom=type, cod=type)
| diagram[::-1]
| diagram @ diagram
| diagram >> diagram
| Id(type)
where [::-1]
, @
and >>
denote the dagger, tensor and
composition respectively. The syntax for types is given by:
type ::= Ty(name) | type @ type | Ty()
Notes
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)
|
Implements a type as a list of |
|
Implements the objects of a PRO, i.e. a non-symmetric PROP. |
|
Layer of a diagram, i.e. a box with wires to the left and right. |
|
Defines a diagram given dom, cod, a list of boxes and offsets. |
|
Implements the identity diagram of a given type. |
|
A box is a diagram with |
|
Sum of monoidal diagrams. |
|
Implements the symmetry of atomic types. |
|
Bubble in a monoidal diagram, i.e. a unary operator on homsets. |
|
Implements a monoidal functor given its image on objects and arrows. |