cat

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

Summary

Ob	An object with a string as name.
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 arrow with the empty tuple inside, called with Id.
Sum	A sum is a tuple of arrows terms with the same domain and codomain.
Bubble	A bubble is a box with an arrow arg inside and an optional pair of objects dom and cod.
Category	A category is just a pair of Python types ob and ar with appropriate methods dom, cod, id and then.
Functor	A functor is a pair of maps ob and ar and an optional codomain category cod.
Composable	Abstract class implementing the syntactic sugar >> and << for forward and backward composition with some method then.

Functions

factory	Allows the identity and composition of an Arrow subclass to remain within the subclass.
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()