drawing

The category of labeled progressive plane graphs.

This was first defined in Joyal and Street [JS88].

Summary

Point	A point is a pair of floats for the x and y coordinates.
PlaneGraph	A plane graph is a graph with a mapping from nodes to points.
Drawing	A drawing is a plane graph with designated input and output types.
Equation	An equation is a list of diagrams with a dedicated draw method.

Axioms

• Associativity and unit

>>> from discopy.monoidal import Ty, Box

>>> x, y, z, w = map(Ty, "xyzw")
>>> f = Box('f', x, y).to_drawing()
>>> g = Box('g', y, z).to_drawing()
>>> h = Box('h', z, w).to_drawing()

>>> assert (f >> g) >> h == f >> (g >> h)
>>> assert (f @ g) @ h == f @ (g @ h)

>>> assert f >> Drawing.id(f.cod) == f == Drawing.id(f.dom) >> f
>>> assert f @ Drawing.id() == f == Drawing.id() @ f

• Interchanger

>>> f0, f1 = (Box(f'f{i}', f'x{i}', f'y{i}').to_drawing() for i in (0, 1))
>>> g0, g1 = (Box(f'g{i}', f'y{i}', f'z{i}').to_drawing() for i in (0, 1))

>>> Equation(f0 @ f1 >> g0 @ g1, (f0 >> g0) @ (f1 >> g1)).draw(
...     path="docs/_static/drawing/interchanger-1.png")

>>> Equation(f @ g.dom >> f.cod @ g, f @ g, f.dom @ g >> f @ g.cod).draw(
...     path="docs/_static/drawing/interchanger-2.png")