drawing#
The category of labeled progressive plane graphs.
This was first defined in Joyal and Street [JS88].
Summary#
A point is a pair of floats for the x and y coordinates. |
|
A plane graph is a graph with a mapping from nodes to points. |
|
A drawing is a plane graph with designated input and output types. |
|
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")