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