Wiring Diagrams for Monoidal Preorders

definition example theorem

Given a Symmetric Monoidal Preorder $(X,\le ,I,\otimes )$, a Wiring Diagram has wires labeled by elements of $X$ and boxes representing inequalities. Two parallel wires $x,y$ and one wire $x\otimes y$ mean the same thing; a wire labeled $I$ and “nothing” mean the same thing (the unit is the empty monoidal product). A diagram from wires $x_1,\dots ,x_m$ on the left to $y_1,\dots ,y_n$ on the right is valid if $x_1\otimes \cdots \otimes x_m\le y_1\otimes \cdots \otimes y_n$.

Sources: 7 Sketches §2.2.2, Eqs. (2.10)–(2.18), Examples 2.14, 2.19, Exercise 2.20.

Axioms as diagram rules

axiom	diagram
reflexivity $x\le x$	a bare wire is valid
transitivity	valid boxes may be connected in series
(a) monotonicity	valid boxes may be stacked in parallel
(b) unitality	blank space / $I$-wires can be ignored
(c) associativity	no distinction between building from top or bottom; $(x\otimes y)\otimes z$ and $x\otimes (y\otimes z)$ are the same three wires
(d) symmetry	wires may cross (a new icon)

Example 2.14. In $(\mathbb{R},\le ,0,+)$, parallel wires add: wires $3.14$ and $-1$ equal a single wire $2.14$; a wire $0$ equals no wire. The facts $4\le 7$ and $2+5\le -1+5+3$ are boxes.

Wiring diagrams as graphical proofs

A wiring diagram with interior boxes inside an exterior box is a proof: if all interior assertions hold, so does the exterior one. For the diagram (2.15) with interior boxes

$$t\le v\otimes w,w\otimes u\le x\otimes z,v\otimes x\le y(2.16)$$

the exterior assertion is $t\otimes u\le y\otimes z$ (2.17), proved by the chain of vertical slices

$$t\otimes u\le v\otimes w\otimes u\le v\otimes x\otimes z\le y\otimes z.(2.18)$$

Formally (7S Exercise 2.20) each step uses monotonicity with a reflexivity $u\le u$ on the untouched wire, associativity to re-bracket, and transitivity to chain; symmetry is needed only if wires cross. The lemon meringue pie diagram (Example 2.19) is a proof that if you can separate eggs, make filling, make meringue, fill the crust and add meringue, then you can prepare a pie.

Boxes in a monoidal preorder are anonymous (they merely assert $\le$); in a Monoidal Category they carry the names of morphisms and the diagrams denote morphisms rather than proofs of inequalities (§4.4.2).