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)
../_images/EckmannHilton.gif

discopy.monoidal.Ty(*objects)

Implements a type as a list of discopy.cat.Ob, used as domain and codomain for monoidal.Diagram.

discopy.monoidal.PRO([n])

Implements the objects of a PRO, i.e. a non-symmetric PROP.

discopy.monoidal.Layer(left, box, right)

Layer of a diagram, i.e. a box with wires to the left and right.

discopy.monoidal.Diagram(dom, cod, boxes, ...)

Defines a diagram given dom, cod, a list of boxes and offsets.

discopy.monoidal.Id([dom])

Implements the identity diagram of a given type.

discopy.monoidal.Box(name, dom, cod, **params)

A box is a diagram with boxes==[self] and offsets==[0].

discopy.monoidal.Sum(terms[, dom, cod])

Sum of monoidal diagrams.

discopy.monoidal.Swap(left, right)

Implements the symmetry of atomic types.

discopy.monoidal.Bubble(inside[, dom, cod])

Bubble in a monoidal diagram, i.e. a unary operator on homsets.

discopy.monoidal.Functor(ob, ar[, ...])

Implements a monoidal functor given its image on objects and arrows.