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.
AxiomError	When arrows do not compose.

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()