cat

The free (dagger) category with formal sums, unary operators and symbolic variables.

Summary

Ob	An object with a string as name.
FreeCategory	A category whose arrows are paths of generating arrows.
Arrow	An arrow is a tuple of composable boxes inside with a pair of objects dom and cod as domain and codomain.
Box	A box is an arrow with a name and the tuple of just itself inside.
Id	The identity path on dom, with no generators inside.
Sum	A sum is a tuple of arrows terms with the same domain and codomain.
Bubble	A bubble is a box with arrow args inside and an optional pair of objects dom and cod.
Functor	A functor is a pair of maps ob_map and ar_map and an optional codomain category cod.
Transformation	A (not necessarily natural) transformation between two parallel functors.
Equation	An axioms.Equation between arrows, see its docstring for the parameters and axioms.Equation.modulo() for quotients.

Functions

factory	Allows the identity and composition of an Arrow subclass to remain within the subclass, by setting cls.factory = cls.
dumps	Serialise a DisCoPy object as JSON.
loads	Loads a serialised DisCoPy object.

Axioms

We can create boxes with objects as domain and codomain:

>>> x, y, z = Ob('x'), Ob('y'), Ob('z')
>>> f, g, h = Box('f', x, y), Box('g', y, z), Box('h', z, x)

We can create arbitrary arrows with identity and composition:

>>> arrow = Arrow.id(x).then(f, g, h)
>>> assert arrow == f >> g >> h == h << g << f

We can create dagger functors from the free category to itself:

>>> ob = {x: z, y: y, z: x}
>>> ar = {f: g[::-1], g: f[::-1], h: h[::-1]}
>>> F = Functor(ob, ar)
>>> assert F(arrow) == (h >> f >> g)[::-1]

We can check the axioms of dagger (i.e. a contravariant involutive identity-on-objects endofunctor):

>>> x, y, z = Ob('x'), Ob('y'), Ob('z')
>>> f, g = Box('f', x, y), Box('g', y, z)
>>> assert f[::-1][::-1] == f
>>> assert Id(x)[::-1] == Id(x)
>>> assert (f >> g)[::-1] == g[::-1] >> f[::-1]

We can check the axioms of dagger functors.

>>> assert F(Id(x)) == Id(F(x))
>>> assert F(f >> g) == F(f) >> F(g)
>>> assert F(f[::-1]) == F(f)[::-1]
>>> assert F(f.dom) == F(f).dom and F(f.cod) == F(f).cod

Functors are bubble-preserving.

>>> assert F(f.bubble()) == F(f).bubble()