\node (b') at (0,2) {$ L(e \times_{h} e') $};
\node (a') at (0,0) {$ Lb' $};
\node (wfz) at (3,4) {$ v $};
\node (v'e'y') at (3,2) {$ x \times_{z} x' $};
\node (u'd'z') at (3,0) {$ v' $};
\node (i) at (6,4) {$ Lc $};
\node (h') at (6,2) {$ L(f \times_{i} f') $};
\node (g') at (6,0) {$ Lc' $};
\draw [cd] (c) to (wfz);
\draw [cd] (i) to (wfz);
\draw [cd] (b') to (v'e'y');
\draw [cd] (h') to (v'e'y');
\draw [cd] (a') to (u'd'z');
\draw [cd] (g') to (u'd'z');
\draw [cd] (b') to node[left]{$ \iso $} (c);
\draw [cd] (b') to node[left]{$ \iso $} (a');
\draw [>->] (v'e'y') to (wfz);
\draw [>->] (v'e'y') to (u'd'z');
\draw [cd] (h') to node[right]{$ \iso $} (i);
\draw [cd] (h') to node[right]{$ \iso $} (g');
\end{scope}
\end{tikzpicture}
\]

Lemma <ref> ensures the
marked arrows are monic.  The horizontal
composition of these is

\[
\begin{tikzpicture}
\node at (0,2) {
$ ( \alpha \vcirc \beta )
\hcirc
( \alpha' \vcirc \beta' )
=  $};
\begin{scope}[shift={(3,0)}]
\node (a) at (0,4) {$ La $};
\node (bcb') at (0,2) {$ Ld \times_{Lg} Ld' $};
\node (a') at (0,0) {$ La' $};
\node (udx) at (4.5,4) {$ u +_{Lb} v $};
\node (middle) at (4.5,2)
{ $ ( w \times_{y} w' )
+_{L(e \times_{h} e')}
( x \times_{z} x') $ };
\node (u'd'z') at (4.5,0) {$ x' +_{Lb'} v' $};
\node (g) at (9,4) {$ Lc $};
\node (hih') at (9,2) {$ Lf +_{Li} Lf' $};
\node (g') at (9,0) {$ Lc' $};
\draw [cd] (a) to (udx);
\draw [cd] (g) to (udx);
\draw [cd] (bcb') to (middle);
\draw [cd] (hih') to (middle);
\draw [cd] (a') to (u'd'z');
\draw [cd] (g') to (u'd'z');
\draw [cd] (bcb') to node[left]{$ \iso $} (a);
\draw [cd] (bcb') to node[left]{$ \iso $} (a');
\draw [>->] (middle) to (udx);
\draw [>->] (middle) to (u'd'z');
\draw [cd] (hih') to node[right]{$ \iso $} (g);
\draw [cd] (hih') to node[right]{$ \iso $} (g');
\end{scope}
\end{tikzpicture}
\]

It follows that the proof of Theorem
<ref> comes down to finding an

\[
(w \times_{y} w') +_{L(e \times_h e')} (x \times_z x')
\to
(w +_{Le} x) \times_{(y +_{Lh} z)} (w' +_{Le'} x')
\]

To simplify our diagrams, we introduce new
notation. We write

\[
\begin{array}{ll}
p  \coloneqq
( w \times_y w' ) + ( x \times_z x' ), &
p'  \coloneqq
( w \times_y w' ) +_{L(e \times_h e')} ( x' \times_z x' ), \\
q  \coloneqq
( w + x ) \times_{ y + z } ( w' + x' ),  &
q'  \coloneqq
( w +_{Lg} x ) \times_{ y +_{Lh} z } ( w' +_{Li} x' ). \\
\end{array}
\]

In this notation, the isomorphism we
seek is

\begin{equation}
\label{eq:interchange-isomorphism}
\theta' \from p' \to q'
\end{equation}

Also, because $ Lb $, $ Le $, $ Lh $, $ Le' $, $ Lb' $, and
therefore $ L(e \times_{h} e') $ are all isomorphic, we
simply write $ L\ast $ to mean any of these.  Each are
interchangeable in the diagrams below, and adjusting this
notation will not cause any false reasoning. While we do lose
the ability to discern between these objects, context should
help the reader determine this.  Despite losing this ability, we gain
a breezier exposition and a more readable proof.

Apply Lemma <ref> to
the diagram

\[
\begin{tikzpicture}
\node (B) at (-4,2) {$ w \times_y w'$};
\node (A) at (0,2) {$ L\ast $};
\node (C) at (4,2) {$ x \times_z x'$};

\node (B') at (-4,0) {$ y $};
\node (A') at (0,0) {$ L\ast $};
\node (C') at (4,0) {$ z $};
\draw [cd] (A) edge (B);
\draw [cd] (A) edge node[right] {\scriptsize{$=$}} (A');
\draw [cd] (A) edge (C);
\draw [cd] (A') edge (B');
\draw [cd] (A') edge (C');
\draw [>->] (B) edge (B');
\draw [>->] (C) edge (C');
\end{tikzpicture}
\]

to get the pushout

\[
\begin{tikzpicture}
\node (BC) at (0,2) {$p$};
\node (BAC) at (4,2) {$p'$};
\node (BC') at (0,0) {$ y + z $};
\node (BAC') at (4,0) {$ y +_{L\ast} z $};
\draw [cd] (BC) edge (BAC);
\draw [>->] (BC) edge node[right]{$\psi$} (BC');
\draw [>->] (BAC) edge node[right]{$\psi'$} (BAC');
\draw [cd] (BC') edge (BAC');
\end{tikzpicture}
\]

Similarly, we get pushouts

\[
\begin{tikzpicture}
\begin{scope}
\node (BC) at (0,2) {$p$};
\node (BAC) at (3,2) {$p'$};
\node (BC') at (0,0) {$w+x$};
\node (BAC') at (3,0) {$w+_{L\ast}x$};
\draw [cd] (BC) edge (BAC);
\draw [>->] (BC) edge node[right]{$\sigma$} (BC');
\draw [>->] (BAC) edge node[right]{$\sigma'$} (BAC');
\draw [cd] (BC') edge (BAC');
\end{scope}
\node () at (4,1) {and};
\begin{scope}[shift={(5,0)}]
\node (BC) at (0,2) {$ p $};
\node (BAC) at (3,2) {$ p' $};
\node (BC') at (0,0) {$ w' + x' $};
\node (BAC') at (3,0) {$ w'+_{L\ast} x'$};
\draw [cd] (BC) edge (BAC);
\draw [>->] (BC) edge node[right]{$ \phi $} (BC');
\draw [>->] (BAC) edge node[right]{$ \phi' $} (BAC');
\draw [cd] (BC') edge (BAC');
\end{scope}
\end{tikzpicture}
\]

Now, $p$ forms a cone over the cospan
$ w+x \to y+z \gets w'+x' $ via the maps $ \psi $,
$ \sigma $, and $ \phi $.  And so, we get a
canonical map $ \theta \from p \to q $.

The commuting diagram

\[
\begin{tikzpicture}
\node (Lg) at (0,0) {$ Lg $};
\node (Lh) at (2,2) {$ L\ast $};
\node (t) at (2,0) {$ t $};
\node (Li) at (4,0) {$ Li $};
\draw [cd] (Lg) to (Lh);
\draw [cd] (Lg) to (t);
\draw [cd] (Li) to (Lh);
\draw [cd] (Li) to (t);
\draw [>->] (Lh) to (t);
\end{tikzpicture}
\]

induces a canonical isomorphism between $ Lg
\times_{L\ast} Li $ and $ Lg \times_{t} L\ast $.

Via the projection maps, $ Lg \times_{L\ast} Li $ forms a
cone over the cospan $ Lg \to t \gets Li $
and, also, $ Lg \times_{t} Li $ forms a cone over the
cospan $ Lg \to L\ast \gets Li $, though the
latter requires the monic
$ L\ast \rightarrowtail t $ to do so. Universality
implies that the induced maps are mutual
inverses and they are the only such pair.

The map $\theta \from p \to q $ is an

Because colimits are stable under pullback
we get an isomorphism

\[
\gamma \from
( w \times_{ y + z } w' ) +
( w \times_{ y + z } x' ) +
( x \times_{ y + z } w' ) +
( x \times_{ y + z } x' )
\to q.
\]

But $ w \times_{ y + z } x' $ and
$ w' \times_{ y + z } x $ are initial. To see
this, recall that in a topos, all maps to the
initial object are isomorphisms.  Now, consider
the diagram

\[
\begin{tikzpicture}
\node (STpb) at (0,4) {$w \times_{y+z} x'$};
\node (T'') at (4,4) {$z'$};
\node (0) at (2,2) {$0$};
\node (T) at (4,2) {$z$};
\node (S') at (0,0) {$w$};
\node (S) at (2,0) {$y$};
\node (ST) at (4,0) {$y+z$};
\draw [cd] (STpb) edge (S');
\draw [cd] (STpb) edge (T'');
\draw [cd] (STpb) edge[dashed] (0);
\draw [cd] (0) edge (S);
\draw [cd] (0) edge (T);
\draw [cd] (S) edge (ST);
\draw [cd] (T) edge (ST);
\draw [cd] (S') edge (S);
\draw [cd] (T'') edge (T);
\end{tikzpicture}
\]

whose lower right square is a pullback because
coproducts are disjoint in topoi.  Similarly,
$ x \times_{ y + z } w' $ is initial.  Hence
we get a canonical isomorphism

\begin{equation} \label{eq:B second iso}
\gamma'
\from ( w \times_{ y + z } w' ) +
( x \times_{ y + z } x' ) \to q
\end{equation}

that factors through $\gamma$. But Lemma
<ref> gives unique

\[
w \times_{ y } w' \cong
w \times_{ y + z } w'
\text{ and }
x \times_{ z } x' \cong x
\times_{ y + z } x'.
\]

This produces a canonical isomorphism

\[
\gamma'' \from p \to
( w \times_{ y + z } w' ) +
( x \times_{ y + z } x' ).
\]

One can show that
$ \theta  = \gamma' \circ \gamma'' $ using
universal properties.

Having shown that $ \theta \from p \to q $ is an
isomorphism, we can write $ p $ in place of
\[ (w+x)
\times_{(y+z)} ( w'+x' )\]
in the following diagram

\begin{equation} \label{diag.the big cube}
\begin{tikzpicture}
\node (A) at (2,3) {$p$};
\node (Ay) at (0,0) {$p'$};
\node (By) at (2,0) {$q'$};
\node (ST) at (8,3) {$y+z$};
\node (ST') at (6,3.75) {$w+x$};
\node (ST'') at (4,2.25) {$w'+x'$};
\node (SYT) at (8,0) {$y+_{L\ast}z$};
\node (SYT') at (6,0.75) {$w+_{Le} x$};
\node (SYT'') at (4,-0.75) {$w'+_{Le'} x'$};
\draw [->>] (A) edge (Ay);
\draw [font=\scriptsize,>->] (A) edge node[below] {$\phi$} (ST'');
\draw [font=\scriptsize,>->] (A) edge node[above] {$\sigma$} (ST');
\draw [font=\scriptsize,cd] (Ay) edge[bend left=20,pos=0.65] node[above] {$\sigma'$} (SYT');
\draw [font=\scriptsize,cd] (Ay) edge[dashed] node[above] {$\theta'$} (By);
\draw [font=\scriptsize,cd] (Ay) edge[bend right=20] node[below] {$\phi'$} (SYT'');
\draw [font=\scriptsize,>->] (By) edge node[above] {$\omega$} (SYT');
\draw [>->] (By) edge (SYT'');
\draw [->>] (ST') edge (SYT');
\draw [>->] (ST') edge (ST);
\draw [>->] (ST'') edge (ST);
\draw [->>] (ST) edge (SYT);
\draw [>->] (SYT') edge (SYT);
\draw [>->] (SYT'') edge (SYT);
\draw [cd] (A) edge[white,line width=4pt] (By);
\draw [font=\scriptsize,cd] (A) edge[dashed] node[right] {$\rho$} (By);
\draw [cd] (ST'') edge[white,line width=6pt] (ST);
\draw [>->] (ST'') edge (ST);
\draw [cd] (ST'') edge[white,line width=6pt] (SYT'');
\draw [->>] (ST'') edge (SYT'');
\end{tikzpicture}
\end{equation}

where $\theta'$ from Equation
(<ref>) finally appears. It and
$\rho$ are the canonical maps arising from the pullback on
the bottom.  Observe that $\rho$ factors through $\theta'$
in the above diagram.  This follows from the universal
property of pullbacks.

The map
$ \theta' \from p' \to q' $ is an

Because we are working in a topos, it suffices
to show that $\theta'$ is both monic and epic.
It is monic because $\sigma'$ is monic.

To see that $\theta'$ is epic, it suffices to
show that $\rho$ is epic.  The front and rear
right faces of (<ref>) are
pushouts by Lemma
<ref>.  Then
because the top and bottom squares of
(<ref>) are pullbacks
consisting of only monomorphisms, Lemma
<ref> implies that the front and
rear left faces are pushouts.  However, as
pushouts over monomorphisms, Lemma <ref> tells us they are pullbacks.  But
in a topos, regular epimorphisms are stable under
pullback, and so $\rho$ is epic.

It remains to show that $\theta'$ serves as an isomorphism
between fine rewrites. This amounts to showing that

\begin{equation} \label{diag.theta 2-cell iso}
\begin{tikzpicture}
\node (La) at (-1.5,2) {$ La $};
\node (X) at (-4,0) {$L(d \times_g d')$};
\node (La') at (-6.5,-2) {$ La $};
\node (LyR) at (2.5,2) {$u +_{L\ast} v$};
\node (Lc) at (6.5,2) {$ Lc $};
\node (Y) at (4,0) {$L(f \times_i f')$};
\node (Lc') at (1.5,-2) {$ Lc' $};
\node (LyR') at (-2.5,-2) {$x'+_{L\ast} v'$};
\node (Ay) at (0,1) {$p'$};
\node (By) at (0,-1) {$q'$};
\draw [cd] (X) edge[] node[above]{$ $} (La);
\draw [cd] (X) edge[] node[above]{$ $} (La');
\draw [cd] (X) edge node[above] {$g$} (Ay);
\draw [cd] (X) edge node[above] {$h$} (By);
\draw [cd] (La) edge[] node[above]{$j$} (LyR);
\draw [cd] (La') edge[] node[below]{$ $} (LyR');
\draw [cd] (Y) edge (Lc);
\draw [cd] (Y) edge (Lc');
\draw [cd] (Y) edge[] (By);
\draw [cd] (Lc) edge[] (LyR);
\draw [cd] (Lc') edge[] (LyR');
\draw [cd] (Ay) edge node[above] {$k$} (LyR);
\draw [cd] (Ay) edge node[right] {$\theta'$} (By);
\draw [font=\scriptsize,cd] (By) edge[pos=0.4] node[below] {$fp$} (LyR);
\draw [cd] (By) edge[] (LyR');
\draw [cd] (Y) edge[white,line width=3.5pt] (Ay);
\draw [cd] (Y) edge[] (Ay);
\draw [cd] (Ay) edge[white,line width=3.5pt] (LyR');
\draw [cd] (Ay) edge[] (LyR');
\end{tikzpicture}
\end{equation}

commutes. Here $g$ and $k$ are induced from
applying vertical composition before horizontal,
$h$ from applying horizontal composition before
vertical, $j$ is from composing in either order,
$f$ is from horizontal composition as given in
Definition <ref> and
$ \omega $ is from (<ref>).  The
top and bottom face commute by construction.

The inner triangles of diagram (<ref>) commute. That is, we have
$ k = f \rho \theta' $ and $ h = \theta' g $.

To see that $ k = f \omega \theta' $, consider the

\[
\begin{tikzpicture}
\node (Yt) at (0,2) {$L\ast$};
\node (Yb) at (0,0) {$L\ast$};
\node (Spb) at (2.5,1.25) {$w \times_{y} w'$};
\node (S') at (2.5,-0.75) {$w$};
\node (Tpb) at (5,2.75) {$x \times_zx'$};
\node (T') at (5,0.75) {$x$};
\node (Ay) at (7.5,2) {$p'$};
\node (SyT) at (7.5,0) {$y+_{L\ast}z$};
\node (LyR) at (10,0) {$u+_{L\ast}v$};
\draw [cd] (Yt) edge[] (Tpb);
\draw [cd] (Yt) edge[] (Spb);
\draw [font=\scriptsize,cd] (Yt) edge node[right] {$\iso$} (Yb);
\draw [cd] (Yb) edge[] (T');
\draw [cd] (Yb) edge[] (S');
\draw [cd] (Tpb) edge[] (Ay);
\draw [>->] (Tpb) edge[] (T');
\draw [font=\scriptsize,cd] (Ay) edge[dashed] node[above] {$k$} (LyR);
\draw [cd] (S') edge[] (SyT);
\draw [font=\scriptsize,cd] (S') edge[bend right=20] node[above] {$\iota_us$} (LyR);
\draw [font=\scriptsize,cd] (T') edge[bend left=20] node[above,pos=.2] {$\iota_vt$} (LyR);
\draw [cd] (T') edge[] (SyT);
\draw [font=\scriptsize,cd] (SyT) edge[dashed] node[above] {$f$} (LyR);
\draw [cd] (Spb) edge[white,line width=4pt] (Ay);
\draw [cd] (Spb) edge[] (Ay);
\draw [>->] (Spb) edge[white,line width=4pt] (S');
\draw [>->] (Spb) edge[] (S');
\draw [cd] (Ay) edge[white,line width=4pt] (SyT);
\draw [font=\scriptsize,cd] (Ay) edge[dashed] node[pos=0.75,left] {$\sigma'$} (SyT);
\end{tikzpicture}
\]

The bottom face is exactly the pushout diagram
from which $f$ was obtained.  Universality
implies that $ k = f \sigma' $ and, as seen in
(<ref>), $ \sigma' = \rho \theta' $.

That $ h = \theta' g $ follows from

\[
f \rho h = j = k g = f \rho \theta' g
\]

and the fact that $ f \rho $ is monic.

Of course, we have only shown that two of the four
inner triangles commute, but we can replicate our
arguments to show the remaining two commute as
well.  This lemma was the last step in proving
Theorem <ref>, the interchange

§ A SYMMETRIC MONOIDAL STRUCTURE

The double category $ _L\FFFineRewrite $ can be equipped
with a symmetric monoidal structure lifted from the
cocartesian structure on $ \A $ and $ \X $. Proving this
amounts to checking the axioms of Definition

$ _L\FFFineRewrite $ is a symmetric monoidal double category.

We denote $ _L\FFFineRewrite $ by $ \RRR $ for
convenience.  Let us first show that the category of
objects $\RRR_0$ and the category of arrows $\RRR_1$ are
symmetric monoidal categories.

We obtain the monoidal structure $ (\otimes_0, 0_{\A}) $ on $\RRR_{0}$ by lifting
the cocartesian structure on $\A$ to the objects and by

\[
(a \xgets{f} b \xto{g} c) \otimes_0 (a' \xgets{f'} b' \xto{g'} c')
\bydef
(a+a' \xgets{f+g} b+b' \xto{f'+g'} c+c')
\]

on morphisms.  Universal properties provide the associator
and unitors as well as the coherence axioms.  This
monoidal structure is clearly symmetric.

Next, we have the category $\RRR_1$ whose objects are the
structured cospans and morphisms are their fine rewrites.
We obtain a symmetric monoidal structure

\[ ( \otimes_1 , L0_{\A} \to L0_{\A} \gets L0_{\A} ) \]
the objects via

\[
(La \to x \gets La') \otimes_1 (Lb \to y \gets Lb')
\bydef
(L(a+b) \to x+y \gets L(a'+b'))
\]

and on the morphisms by

\[
\raisebox{-0.5\height}{
\begin{tikzpicture}
\node (A) at (0,4) {$La$};
\node (A') at (0,2) {$Lb$};
\node (A'') at (0,0) {$Lc$};
\node (B) at (2,4) {$v$};
\node (B') at (2,2) {$w$};
\node (B'') at (2,0) {$x$};
\node (C) at (4,4) {$La'$};
\node (C') at (4,2) {$Lb'$};
\node (C'') at (4,0) {$Lc'$};
\draw[cd]
% horizontal arrows
(A) edge node[above]{} (B)
(A') edge node[above]{} (B')
(A'') edge node[above]{} (B'')
(C) edge node[above]{} (B)
(C') edge node[above]{} (B')
(C'') edge node[above]{} (B'')
% vertical arrows
(A') edge node[left]{} (A)
(A') edge node[left]{} (A'')
(B') edge[>->] node[left]{} (B)
(B') edge[>->] node[left]{} (B'')
(C') edge node[left]{} (C)
(C') edge node[left]{} (C'');
\end{tikzpicture}
\quad \otimes_1 \quad
\raisebox{-0.5\height}{
\begin{tikzpicture}
\node (A) at (0,4) {$La''$};
\node (A') at (0,2) {$Lb''$};
\node (A'') at (0,0) {$Lc''$};
\node (B) at (2,4) {$v'$};
\node (B') at (2,2) {$w'$};
\node (B'') at (2,0) {$x'$};
\node (C) at (4,4) {$La'''$};
\node (C') at (4,2) {$Lb'''$};
\node (C'') at (4,0) {$Lc'''$};
\draw[cd]
% horizontal arrows
(A) edge node[above]{} (B)
(A') edge node[above]{} (B')
(A'') edge node[above]{} (B'')
(C) edge node[above]{} (B)
(C') edge node[above]{} (B')
(C'') edge node[above]{} (B'')
% vertical arrows
(A') edge node[left]{} (A)
(A') edge node[left]{} (A'')
(B') edge[>->] node[left]{} (B)
(B') edge[>->] node[left]{} (B'')
(C') edge node[left]{} (C)
(C') edge node[left]{} (C'');
\end{tikzpicture}
\quad \bydef \quad
\]

\[
\raisebox{-0.5\height}{
\begin{tikzpicture}
\node (A) at (0,4) {$L(a+a'')$};
\node (A') at (0,2) {$L(b+b'')$};
\node (A'') at (0,0) {$L(c+c'')$};
\node (B) at (3,4) {$v+v'$};
\node (B') at (3,2) {$w+w'$};
\node (B'') at (3,0) {$x+x'$};
\node (C) at (6,4) {$L(a'+a''')$};
\node (C') at (6,2) {$L(b'+b''')$};
\node (C'') at (6,0) {$\L(c'+c''')$};
\draw[cd]
% horizontal arrows
(A) edge node[above]{} (B)
(A') edge node[above]{} (B')
(A'') edge node[above]{} (B'')
(C) edge node[above]{} (B)
(C') edge node[above]{} (B')
(C'') edge node[above]{} (B'')
% vertical arrows
(A') edge node[left]{} (A)
(A') edge node[left]{} (A'')
(B') edge[>->] node[left]{} (B)
(B') edge[>->] node[left]{} (B'')
(C') edge node[left]{} (C)
(C') edge node[left]{} (C'');
\end{tikzpicture}
\]

Again, universal properties provide the associator,
unitors, and coherence axioms.  Hence both $\RRR_0$
and $\RRR_1$ are symmetric monoidal categories.

It remains to find globular isomorphisms $\mathfrak{x}$
and $\mathfrak{u}$ and their coherence. To find
$\mathfrak{x}$, fix horizontal 1-morphisms

\begin{align*}
La & \to x \gets La',   &   La' & \to x' \gets La'', \\
Lb & \to y \gets Lb',   &   Lb' & \to y' \gets Lb''.
\end{align*}

The globular isomorphism $\mathfrak{x}$ is an invertible 2-morphism with domain

\[
L(a+b) \to (x+y) +_{L(a'+b')} (x'+y') \gets L(a''+b'')
\]

and codomain

\[
L(a+b) \to (x+_{La'} y) + (x' +_{Lb'} y') \gets L(a''+b'')
\]

This comes down to finding an isomorphism in $\X$
between the apexes of the above cospans.  Such an
isomorphism exists, and is unique, because both apexes are
colimits of the non-connected diagram

\[
\begin{tikzpicture}
\node (a) at (0,0) {$La$};
\node (b) at (1,.5) {$x$};
\node (c) at (2,0) {$La'$};
\node (d) at (3,.5) {$x'$};
\node (e) at (4,0) {$La''$};
\node (v) at (5,0) {$Lb$};
\node (w) at (6,.5) {$y$};
\node (x) at (7,0) {$Lb'$};
\node (y) at (8,.5) {$y'$};
\node (z) at (9,0) {$Lb''$};
\path[cd,font=\scriptsize,>=angle 90]
(a) edge node[above]{$$} (b)
(c) edge node[above]{$$} (b)
(c) edge node[above]{$$} (d)
(e) edge node[above]{$$} (d)
(v) edge node[above]{$$} (w)
(x) edge node[above]{$$} (w)
(x) edge node[above]{$$} (y)
(z) edge node[above]{$$} (y);
\end{tikzpicture}
\]
Moreover, the resulting globular isomorphism is a fine
rewrite of structured cospans because the universal maps are
isomorphisms. The globular isomorphism $\mathfrak{u}$ is

Finally, we check that the coherence axioms, namely
(a)-(k) of Definition \ref{def:mndl-dbl-cats},
hold.  These are straightforward, though tedious, to
verify.  For instance, if we have
\[
\begin{tikzpicture}
\node (a) at (0,0) {$La$};
\node (b) at (1,.5) {$x$};
\node (c) at (2,0) {$La'$};
\node (M1) at (-1,.25) {$M_1 =$};
\node (M2) at (3,.25) {$M_2 =$};
\node (c2) at (4,0) {$La'$};
\node (d) at (5,.5) {$x'$};
\node (e) at (6,0) {$La''$};
\node (M3) at (7,.25) {$M_3 =$};
\node (e2) at (8,0) {$La''$};
\node (f) at (9,.5) {$x''$};
\node (g) at (10,0) {$La'''$};
\node (t) at (0,-2) {$Lb$};
\node (u) at (1,-1.5) {$y$};
\node (v) at (2,-2) {$Lb'$};
\node (N1) at (-1,-1.75) {$N_1 =$};
\node (N2) at (3,-1.75) {$N_2 =$};
\node (v2) at (4,-2) {$Lb'$};
\node (w) at (5,-1.5) {$y'$};
\node (x) at (6,-2) {$Lb''$};
\node (N3) at (7,-1.75) {$N_3 =$};
\node (x2) at (8,-2) {$Lb''$};
\node (y) at (9,-1.5) {$y''$};
\node (z) at (10,-2) {$Lb'''$};
\path[cd,font=\scriptsize,>=angle 90]
(a) edge node[above]{$$} (b)
(c) edge node[above]{$$} (b)
(c2) edge node[above]{$$} (d)
(e) edge node[above]{$$} (d)
(v2) edge node[above]{$$} (w)
(e2) edge node[above]{$$} (f)
(g) edge node[above]{$$} (f)
(t) edge node[above]{$$} (u)
(v) edge node[above]{$$} (u)
(x) edge node[above]{$$} (w)
(x2) edge node[above]{$$} (y)
(z) edge node[above]{$$} (y);
\end{tikzpicture}
\]
then following Diagram \eqref{diag:MonDblCat} around the
top right gives the sequence of cospans
\[
\begin{tikzpicture}
\node (a) at (-5,0) {$L(a+b)$};
\node (b) at (0,0.5) {
$((x+y) +_{ L( a' + b') } (x'+y'))
+_{ L (a'' + b'') } (x''+y'') $ };
\node (c) at (5,0) {$L(a''+b'')$};
\node (M1) at (-2,1.5) {
$((M_1 \otimes N_1) \odot
(M_2 \otimes N_2)) \odot
(M_3 \otimes N_3) = $ };
\path[cd,font=\scriptsize]
(a) edge[in=180,out=45] node[above]{$$} (b)
(c) edge[in=0,out=135] node[above]{$$} (b);
\end{tikzpicture}
\]
\[
\begin{tikzpicture}
\node (a) at (-5,0) {$L(a+b)$};
\node (b) at (0,0.5) {
$ ( (x +_{La'} x') +
( y +_{Lb'} y')) +_{ L(a''+b'') }
(x''+y'') $ };
\node (c) at (5,0) {$ L(a''+b'') $};
\node (M1) at (-2,1.5) {
$((M_1 \odot M_2) \otimes
(N_1 \odot N_2)) \odot
(M_3 \otimes N_3) = $ };
\path[cd,font=\scriptsize]
(a) edge[in=180,out=45] node[above]{$$} (b)
(c) edge[in=0,out=135] node[above]{$$} (b);
\end{tikzpicture}
\]
\[
\begin{tikzpicture}
\node (a) at (-5,0) { $ L(a+b) $ };
\node (b) at (0,0.5) {
$ ( ( x +_{La'} x') +_{La''} x'' ) +
( ( y +_{Lb'} y' ) +_{Lb''} y'' ) $ };
\node (c) at (5,0) {$ L(a''+b'') $};
\node (M1) at (-2,1.5) {
$((M_1 \odot M_2) \odot M_3) \otimes
((N_1 \odot N_2) \odot N_3) = $};
\path[cd,font=\scriptsize]
(a) edge[in=180,out=45] node[above]{$$} (b)
(c) edge[in=0,out=135] node[above]{$$} (b);
\end{tikzpicture}
\]
\[
\begin{tikzpicture}
\node (a) at (-5,0) {$L(a+b)$};
\node (b) at (0,0.5) {
$ ( x +_{La'} ( x' +_{La''} x'' )) +
( y +_{Lb'} ( y' +_{Lb''} y'' ) ) $ };
\node (c) at (5,0) {$ L(a''+b'') $};
\node (M1) at (-2,1.5) {
$( M_1 \odot (M_2 \odot M_3)) \otimes
(N_1 \odot (N_2 \odot N_3)) = $ };
\path[cd,font=\scriptsize]
(a) edge[in=180,out=45] node[above]{$$} (b)
(c) edge[in=0,out=135] node[above]{$$} (b);
\end{tikzpicture}
\]
Following the diagram \eqref{diag:MonDblCat} around the
bottom left gives another sequence of cospans
\[
\begin{tikzpicture}
\node (a) at (-5,0) {$ L(a + b) $};
\node (b) at (0,0.5) {
$ ( (x + y) +_{L (a'+b')} (x'+y'))
+_{L(a''+b'')} (x'' + y'' ) $ };
\node (c) at (5,0) {$ L(a'' + b'') $};
\node (M1) at (-2,1.5) {
$ ((M_1 \otimes N_1) \odot
(M_2 \otimes N_2)) \odot
(M_3 \otimes N_3) = $ };
\path[cd,font=\scriptsize]
(a) edge[in=180,out=45] node[above]{$$} (b)
(c) edge[in=0,out=135] node[above]{$$} (b);
\end{tikzpicture}
\]
\[
\begin{tikzpicture}
\node (a) at (-5,0) {$L(a+b)$};
\node (b) at (0,0.5) {
$ (x + y) +_{L(a'+b')}
( (x' + y') +_{ L(a''+b'') } (x'' + y'') )$};
\node (c) at (5,0) {$L(a'''+b''')$};
\node (M1) at (-2,1.5) {
$(M_1 \otimes N_1) \odot
((M_2 \otimes N_2) \odot
(M_3 \otimes N_3)) = $ };
\path[cd,font=\scriptsize]
(a) edge[in=180,out=45] node[above]{$$} (b)
(c) edge[in=0,out=135] node[above]{$$} (b);
\end{tikzpicture}
\]
\[
\begin{tikzpicture}
\node (a) at (-5,0) {$ L(a+b) $};
\node (b) at (0,0.5) {
$ (x+y) +_{L(a'+b')}
( (x' +_{La''} x'') + ( y' +_{Lb''} y'') ) $};
\node (c) at (5,0) {$ L(a'''+b''') $};
\node (M1) at (-2,1.5) {
$(M_1 \otimes N_1) \odot
((M_2 \odot M_3) \otimes
(N_2 \odot N_3)) = $};
\path[cd,font=\scriptsize]
(a) edge[in=180,out=45] node[above]{$$} (b)
(c) edge[in=0,out=135] node[above]{$$} (b);
\end{tikzpicture}
\]
\[
\begin{tikzpicture}
\node (a) at (-5,0) {$ L(a+b) $};
\node (b) at (0,.5) {
$ ( x +_{La'} ( x' +_{La''} x'' )) +
( y +_{Lb'} ( y' +_{Lb''} y'' ) )$};
\node (c) at (5,0) {$ L(a'''+b''') $};
\node (M1) at (-2,1.5) {
$(M_1 \odot (M_2 \odot M_3))
\otimes (N_1 \odot (N_2 \odot N_3)) = $};
\path[cd,font=\scriptsize]
(a) edge[in=180,out=45] node[above]{$$} (b)
(c) edge[in=0,out=135] node[above]{$$} (b);
\end{tikzpicture}
\]
Putting these together gives the following commutative diagram.
\[
\begin{tikzpicture}
\node (a) at (-6,0) {$ L(a+b) $};
\node (b) at (0,0) {
$ ( (x+y) +_{L(a'+b')} (x'+y')) +_{L(a''+b'')} (x''+y'')$};
\node (c) at (6,0) {$L(a'''+b''')$};
\node (a2) at (-6,1.5) {$L(a+b)$};
\node (b2) at (0,1.5) {
$ (( x +_{La'} x')+ ( y+_{Lb'} y')) +_{L(a''+b'')} (x''+y'')$};
\node (c2) at (6,1.5) {$L(a'''+b''')$};
\node (a3) at (-6,3) {$L(a+b)$};
\node (b3) at (0,3) {
$ (( x +_{La'} x') +_{La''} x'')+ (( y +_{Lb'} y') +_{Lb''} y'')$};
\node (c3) at (6,3) {$L(a'''+b''')$};
\node (a4) at (-6,4.5) {$L(a+b)$};
\node (b4) at (0,4.5) {
$ ( x +_{La'} (x'+_{La''} x'')) + ( y +_{Lb'} ( y'+_{Lb''} y''))$};
\node (c4) at (6,4.5) {$L(a'''+b''')$};
\node (a5) at (-6,-1.5) {$L(a+b)$};
\node (b5) at (0,-1.5) {
$ (x+y) +_{L(a'+b')} ( (x'+y') +_{L(a''+b'')} (x''+y''))$};
\node (c5) at (6,-1.5) {$L(a'''+b''')$};
\node (a6) at (-6,-3) {$L(a+b)$};
\node (b6) at (0,-3) {
$(x+y)+_{L(a'+b')} ( (x' +_{la''} x'') + ( y' +_{La''} y''))$};
\node (c6) at (6,-3) {$L(a'''+b''')$};
\node (a7) at (-6,-4.5) {$L(a+b)$};
\node (b7) at (0,-4.5) {
$( x +_{La'} (x' +_{La''} x'')) + ( y +_{Lb'} (y'+_{Lb''} y''))$};
\node (c7) at (6,-4.5) {$L(a'''+b''')$};
\path[cd,font=\scriptsize,>=angle 90]
(a) edge node[above]{$$} (b)
(c) edge node[above]{$$} (b)
(a2) edge node[above]{$$} (b2)
(c2) edge node[above]{$$} (b2)
(a) edge node[above]{$$} (a2)
(b) edge node[above]{$$} (b2)
(c) edge node[above]{$$} (c2)
(a3) edge node[above]{$$} (b3)
(c3) edge node[above]{$$} (b3)
(a2) edge node[above]{$$} (a3)
(b2) edge node[above]{$$} (b3)
(c2) edge node[above]{$$} (c3)
(a4) edge node[above]{$$} (b4)
(c4) edge node[above]{$$} (b4)
(a3) edge node[above]{$$} (a4)
(b3) edge node[above]{$$} (b4)
(c3) edge node[above]{$$} (c4)
(a5) edge node[above]{$$} (b5)
(c5) edge node[above]{$$} (b5)
(a) edge node[above]{$$} (a5)
(b) edge node[above]{$$} (b5)
(c) edge node[above]{$$} (c5)
(a6) edge node[above]{$$} (b6)
(c6) edge node[above]{$$} (b6)
(a5) edge node[above]{$$} (a6)
(b5) edge node[above]{$$} (b6)
(c5) edge node[above]{$$} (c6)
(a7) edge node[above]{$$} (b7)
(c7) edge node[above]{$$} (b7)
(a6) edge node[above]{$$} (a7)
(b6) edge node[above]{$$} (b7)
(c6) edge node[above]{$$} (c7);
\end{tikzpicture}
\]
The vertical 1-morphisms on the left and right are the the
respective identity spans on $L(a+b)$ and $L(a'''+b''')$.  The
vertical 1-morphisms in the center are isomorphism classes
of monic spans where each leg is given by a universal map
between two colimits of the same diagram.  The horizontal
1-morphisms are given by universal maps into coproducts
and pushouts.  The top cospan is the same as the bottom
cospan, making a bracelet-like figure in which all faces
commute.  The other diagrams witnessing coherence are
given in a similar fashion.
\end{proof}

% =====================================================
% CHAPTER: spans of cospans
% SECTION: a compact closed bicategory
% =====================================================

\section{A compact closed bicategory of spans of cospans}
\label{sec:compact-closed-bicategory-spans-of-cospans}

Double categories have many nice features yet are not as
established in the world of higher categories as
bicategories. For those who more comfortable with
bicategories, we write this section to discuss a bicategory
of fine rewrites of structured cospans. Intuitively, it is
straightforward to pass from the double category
$ _L\FFFineRewrite $ to a bicategory of fine rewrites. By
only accepting the squares of $ _L\FFFineRewrite $ that fix
the inputs and outputs, that is disallow permutations, then
the only vertical arrows left are identities.  But a double
category with only identity vertical arrows is virtually a
bicategory. Care is needed, though, because to actually
remove a bicategory of fine rewrites from
$ _L\FFFineRewrite $ requires more rigor than simply picking
out only the vertical arrows that are the identity.

More than a bicategory, we can actually extract a compact closed
bicategory from the symmetric monoidal double category
$ _L\FFFineRewrite $. To obtain a symmetric monoidal
bicategory from $ _L\FFFineRewrite $, we use machinery
developed by Shulman [58]. To show
that this bicategory is also compact closed, we use work by
Stay [59].

First, let us extract the `horizontal bicategory' of
$ _L\FFFineRewrite $, so named because we remove the
vertical arrows.

\begin{definition}
Define $ _L\FFineRewrite $ to be the bicategory whose
objects are the objects of $ \A $, 1-arrows are structured
cospans, and 2-arrows are fine rewrite rules of form
\begin{center}
\begin{tikzpicture}
\node (La) at (0,4) {$ La $};
\node (x) at (2,4) {$ x $};
\node (Lb) at (4,4) {$ Lb $};
\node (La') at (0,2) {$ La $};
\node (y) at (2,2) {$ y $};
\node (Lb') at (4,2) {$ Lb $};
\node (La'') at (0,0) {$ La $};
\node (z) at (2,0) {$ z $};
\node (Lb'') at (4,0) {$ Lb $};
\draw [cd]
(La) edge[] (x)
(Lb) edge[] (x)
(La') edge[] (y)
(Lb') edge[] (y)
(La'') edge[] (z)
(Lb'') edge[] (z)
(La') edge[] node[left]{$ \id $} (La)
(La) edge[] node[left]{$ \id $} (La'')
(y) edge[>->] (x)
(y) edge[>->] (z)
(Lb') edge[] node[right]{$ \id $} (Lb)
(Lb') edge[] node[right]{$ \id $} (Lb'');
\end{tikzpicture}
\end{center}
\end{definition}

That this is a double category follows from Shulman's
construction mentioned in Definition
\ref{def:horiz-bicat}. Had we used the same notation as that
definition, we would let $ _L\FFineRewrite \bydef
\mathcal{H} ( _L\FFFineRewrite ) $.

Shulman's construction continues to be useful, as we use it
to show that the double category $ _L\FFineRewrite $ is
symmetric monoidal.  The first step towards this is showing
that $ _L\FFFineRewrite $ is isofibrant (see Definition
\ref{def:Fibrant}).

% DOUBLE CATEGORIES ARE ISOFIBRANT
\begin{lemma}
\label{lem:SpanCospanIsofibrant}
The symmetric monoidal double category $ _L\FFFineRewrite $
is isofibrant.
\end{lemma}

\begin{proof}
The companion of a vertical 1-morphism
\[
f = (a \xgets{\theta} b \xto{\psi} c)
\]
is given by
\[
\widehat{f} =
( La \xto{ L\theta^{-1} } Lb \xgets{ L\psi^{-1} } Lc )
\]
The required 2-arrows are given by
\[
\raisebox{-0.5\height}{
\begin{tikzpicture}
\node (A) at (0,4) {$La$};
\node (A') at (0,2) {$Lb$};
\node (A'') at (0,0) {$Lc$};
\node (B) at (2,4) {$Lb$};
\node (B') at (2,2) {$Lc$};
\node (B'') at (2,0) {$Lc$};
\node (C) at (4,4) {$Lc$};
\node (C') at (4,2) {$Lc$};
\node (C'') at (4,0) {$Lc$};
\draw[cd]
% horizontal arrows
(A) edge node[above]{} (B)
(A') edge node[above]{} (B')
(A'') edge node[above]{} (B'')
(C) edge node[above]{} (B)
(C') edge node[above]{} (B')
(C'') edge node[above]{} (B'')
% vertical arrows
(A') edge node[left]{} (A)
(A') edge node[left]{} (A'')
(B') edge node[left]{} (B)
(B') edge node[left]{} (B'')
(C') edge node[left]{} (C)
(C') edge node[left]{} (C'');
\end{tikzpicture}
\quad \text{ and } \quad
\raisebox{-0.5\height}{
\begin{tikzpicture}
\node (A) at (0,4) {$La$};
\node (A') at (0,2) {$La$};
\node (A'') at (0,0) {$La$};
\node (B) at (2,4) {$La$};
\node (B') at (2,2) {$La$};
\node (B'') at (2,0) {$Lb$};
\node (C) at (4,4) {$La$};
\node (C') at (4,2) {$Lb$};
\node (C'') at (4,0) {$Lc$};
\path[cd,font=\scriptsize,>=angle 90]
% horizontal arrows
(A) edge node[above]{} (B)
(A') edge node[above]{} (B')
(A'') edge node[above]{} (B'')
(C) edge node[above]{} (B)
(C') edge node[above]{} (B')
(C'') edge node[above]{} (B'')
% vertical arrows
(A') edge node[left]{} (A)
(A') edge node[left]{} (A'')
(B') edge node[left]{} (B)
(B') edge node[left]{} (B'')
(C') edge node[left]{} (C)
(C') edge node[left]{} (C'');
\end{tikzpicture}
\]
The conjoint of $f$ is given by $\check{f} = \widehat{f}^{\text{op}}$.
\end{proof}

Because the symmetric monoidal double category
$ _L\FFFineRewrite $ is isofibrant, Theorem \ref{thm:horz-bicat}
extracts a symmetric monoidal bicategory $ _L\FFineRewrite $
comprised of the same objects, structured cospans as arrows,
and isomorphism classes of fine rewrites of structured
cospans with form
\[
\begin{tikzpicture}
\node (A) at (0,4) {$La$};
\node (A') at (0,2) {$La$};
\node (A'') at (0,0) {$La$};
\node (B) at (2,4) {$v$};
\node (B') at (2,2) {$w$};
\node (B'') at (2,0) {$x$};
\node (C) at (4,4) {$La'$};
\node (C') at (4,2) {$La'$};
\node (C'') at (4,0) {$La'$};
\path[cd,font=\scriptsize,>=angle 90]
% horizontal arrows
(A) edge node[above]{} (B)
(A') edge node[above]{} (B')
(A'') edge node[above]{} (B'')
(C) edge node[above]{} (B)
(C') edge node[above]{} (B')
(C'') edge node[above]{} (B'')
% vertical arrows
(A') edge node[left]{\scriptsize{$ \id  $}} (A)
(A') edge node[left]{\scriptsize{$ \id  $}} (A'')
(B') edge[>->] node[left]{} (B)
(B') edge[>->] node[left]{} (B'')
(C') edge node[right]{\scriptsize{$ \id  $}} (C)
(C') edge node[right]{\scriptsize{$ \id  $}} (C'');
\end{tikzpicture}
\]
The difference between these fine rewrites and the squares
of $ _L\FFFineRewrite $ is that the vertical arrows are
identities. This is necessary given that bicategories have
no vertical arrows.  However, the isofibrancy condition
ensures that information carried by the vertical arrows is
encoded the horizontal arrows.

\begin{theorem}
\label{thm:SpansCospasAreSMBicat}
$ _L\FFineRewrite$ is a symmetric monoidal bicategory.
\end{theorem}

\begin{proof}
Lemma \ref{lem:SpanCospanIsofibrant} states that $
_L\FFFineRewrite $ is isofibrant. The result then follows
from Theorem \ref{thm:horz-bicat}.
\end{proof}

It remains to show that this bicategory is compact
closed. This structure of $ _L\FFineRewrite $ is another
benefit of bicategories over double categories.  Currently,
there is no notion of compact closedness for double
categories.  However, it is a nice feature to have in a
category that serves as the syntax for open systems with
inputs and outputs.  Here, we mention again that the terms
`inputs' and `outputs' do not imply a causal structure.
Instead, they partition the interface of an open system into
two parts, the purpose of which manifests when composing a
pair of systems. If we connect an open system, considered as
an structured cospan $ La \to x \gets La' $, to another
system, then $ La $ is parts of the connection and $ La' $
is not or vice versa.  That is, partitioning an interface
into inputs and outputs allows a portion of the interface to
be part of a connection and the remain portion to be left
out of the connection. Compact closedness formalizes the
viewpoint that \emph{how} an interface is partitioned is
arbitrary.  Indeed, every possible partition of the
interface exists as an arrow in $ _L\FFineRewrite $. That
is, given a system $ x $ with interface $ i $, then for any
two subobjects $ a $, $ a' $ of $ i $ such that
$ a+a' \cong i $, there is an an arrow
$ La \to x \gets La' $ in $ _L\FFineRewrite $.

\begin{example}
Denote by $ x $ the graph
\[
\begin{tikzpicture}
\node (1) at (0,0) {$ \bullet_a $};
\node (2) at (0,2) {$ \bullet_b $};
\node (3) at (2,0) {$ \bullet_c $};
\node (4) at (2,2) {$ \bullet_d$};
\draw[graph]
(1) edge (2)
(1) edge (3)
(3) edge[loop right] (3)
(4) edge (2)
(1) edge (4);
\end{tikzpicture}
\]
with interface $ \{a,c,d\} $.  Then $ x $ appears as
an arrow in $ _L\FFineRewrite $ where $ L $ is from
\[
\adjunction{\Set}{\RGraph}{L}{R}{4}
\]
as all of the following
\begin{align*}
\{ a,c,d \} & \to x \gets 0     &
\{ a,c \}   & \to x \gets \{ d \}       \\
\{ a,d \}   & \to x \gets \{ c \}       &
\{ c,d \}   & \to x \gets \{ a \}       \\
\{ a \}     & \to x \gets \{ c,d \}     &
\{ c \}     & \to x \gets \{ a,d \}     \\
\{ d \}     & \to x \gets \{ a,c \}     &
0   & \to x \gets \{ a,b,c\}
\end{align*}
\end{example}

The ability to change an input to an output and vice versa
comes from the compact closed structure. We take the
remainder of this section to show that $ _L\FFineRewrite $
is compact closed.

We start with the following lemma. For this lemma, we
introduce the notation $ \nabla \from a+a \to a $ for the
folding map, which arises from the coproduct diagram
\[
\begin{tikzpicture}
\node (x1) at (-3,2) {$ a $};
\node (xx) at (0,2) {$ a+a $};
\node (x2) at (3,2) {$ a $};
\node (x)  at (0,0) {$ a $};
\draw [cd] (x1) to
node [above] {\scriptsize{$ \iota $}} (xx);
\draw [cd] (x2)
to node [above] {\scriptsize{$ \iota $}} (xx);
\draw [cd] (x1) to
node [left] {\scriptsize{$ \id $}} (x);
\draw [cd] (x2) to
node [right] {\scriptsize{$ \id $}} (x);
\draw [cd,dashed] (xx) to node [left] {\scriptsize{$ \nabla $}} (x);
\end{tikzpicture}
\]

\begin{lemma}
\label{lem:PushoutDiagram}
In a category with coproducts, the diagram
\[
\begin{tikzpicture}
\node (UL) at (0,2) {$a+a+a$};
\node (LL) at (0,0) {$a+a$};
\node (UR) at (4,2) {$a+a$};
\node (LR) at (4,0) {$a$};
\path[cd,font=\scriptsize,>=angle 90]
(UL) edge node[above] {$\id + \nabla$} (UR)
(UL) edge node[left] {$\nabla + \id$} (LL)
(UR) edge node[right] {$\nabla$} (LR)
(LL) edge node[above] {$\nabla$} (LR);
\end{tikzpicture}
\]
is a pushout square.
\end{lemma}

\begin{proof}
Suppose that we have two maps $ f,g \from a+a \to b$
forming a cocone over the span inside the above diagram.
Let the arrow $\iota_{\text{m}} \from a \to a+a+a$ include
$a$ into the middle copy.  Observe that
$\iota_{\text{l}} \coloneqq (\nabla + a) \circ \iota_{\text{m}}
$ and $\iota_r \coloneqq (a + \nabla) \circ \iota_{\text{m}} $ are,
respectively, the left and right inclusions $a \to a+a$.
Then $f \circ \iota_{\text{l}} = g \circ \iota_{\text{r}}$ is a
map $a \to b$, which we claim is the unique map making
\begin{center}
\begin{tikzpicture}
\node (UL) at (0,2) {$a+a+a$};
\node (LL) at (0,0) {$a+a$};
\node (UR) at (4,2) {$a+a$};
\node (LR) at (4,0) {$a$};
\node (b) at (6,-2) {$ b $};
\draw [cd]
(LR) edge[dashed] (b)
(LL) edge[bend right] (b)
(UR) edge[bend left] (b)
(UL) edge node[above] {$\id + \nabla$} (UR)
(UL) edge node[left] {$\nabla + \id$} (LL)
(UR) edge node[right] {$\nabla$} (LR)
(LL) edge node[above] {$\nabla$} (LR);
\end{tikzpicture}
\end{center}
commute.  Indeed, given $h \from a \to b$ such that
$f = h \circ \nabla = g$, then
$g \circ \iota_
{ \text{r} } = f \circ \iota_{ \text{l} } = h \circ
\nabla \circ \iota_{ \text{l} } = h$.
\end{proof}

In the following theorem, we will make a slight abuse of
notation by writing $ \nabla $ to mean
\[
L(a+a) \to La + La \xto{\nabla} La.
\]
Here, $ L(a+a) \to La+La $ is the structure map which is
invertible because, as a left adjoint, $ L $ preserves coproducts.

\begin{theorem}
\label{thm:SpansMapsAreCCBicat}
The symmetric monoidal bicategory $ _L\FFineRewrite $ is compact closed.
\end{theorem}

\begin{proof}
First we show that each object is its own dual.
For an object $a$, define the counit
$\epsilon \from a + a \to 0$ and unit
$\eta \from 0 \to a+a$ to be the following cospans:
\[
\epsilon \bydef (L(a+a) \xto{\nabla} La \gets 0),
\quad \quad
\eta \bydef (0 \to La \xgets{\nabla} L(a+a)).
\]
Next we define the cusp isomorphisms, $\alpha$
and $\beta$.  Note that $\alpha$ is a 2-morphism
whose domain is the composite
\[
a \xto{ \iota_{ \text{l} } }
a+a \xgets{ \id +\nabla }
a+a+a \xto{ \nabla + \id }
a+a \xgets{ \iota_{ \text{r} } }
\]
and whose codomain is the identity cospan on $a$.  From
Lemma \ref{lem:PushoutDiagram} we have the equations
$\nabla+\id = \iota_{\text{l}} \circ \nabla$ and
$\id + \nabla = \iota_{\text{r}} \circ \nabla$ from which it
follows that the domain of $\alpha$ is the identity cospan
on $a$, and the codomain of $\beta$ is also the identity
cospan on $a$ obtained as the composite
\[
a \xto{\iota_{\text{r}}}
a+a \xgets{\nabla+ \id}
a+a+a \xto{X+\nabla}
a+a \xgets{\iota_{\text{l}}}
\]
Take $\alpha$ and $\beta$ each to be the
isomorphism class determined by the identity
2-morphism on $a$, which in particular is a
monic span of cospans.  Thus we have a dual pair
$(a,a,\epsilon,\eta,\alpha,\beta)$.  By Theorem
\ref{thm:StrictingDualPairs}, there exists a
cusp isomorphism $\beta'$ such that the tuple
$(a,a,\epsilon,\eta,\alpha,\beta')$ is a coherent dual
pair, and thus $  _L \FFineRewrite $ is
compact closed.
\end{proof}

%%%%%%%%%%%%%%%%%%%                %%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%    CHAPTER     %%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%% BOLD REWRITING %%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%                %%%%%%%%%%%%%%

\chapter{Bold rewriting and structured cospans}
\label{sec:bold-rewriting}

We contrast this section with the previous section on fine
rewriting with an example.  In the fine rewriting of
structured cospans, we ask for rewrite rules with the monic
arrows as in the diagram
\[
\begin{tikzpicture}
\node (1) at (0,4) {$ La $};
\node (2) at (2,4) {$ x $};
\node (3) at (4,4) {$ La' $};
\node (4) at (0,2) {$ Lb $};
\node (5) at (2,2) {$ y $};
\node (6) at (4,2) {$ Lb' $};
\node (7) at (0,0) {$ Lc $};
\node (8) at (2,0) {$ z $};
\node (9) at (4,0) {$ Lc' $};
\path[cd,font=\scriptsize]
(1) edge node[]{$  $} (2)
(3) edge node[]{$  $} (2)
(4) edge node[]{$  $} (5)
(6) edge node[]{$  $} (5)
(7) edge node[]{$  $} (8)
(9) edge node[]{$  $} (8)
(4) edge node[left]{$ \iso $} (1)
(4) edge node[left]{$ \iso $} (7)
(6) edge node[right]{$ \iso $} (3)
(6) edge node[right]{$ \iso $} (9);
\path[>->,font=\scriptsize]
(5) edge node[]{$  $} (2)
(5) edge node[]{$  $} (8);
\end{tikzpicture}
\]
There are situations, however, where requiring those monic
arrows is untenable. Consider, for instance, the string calculi
so frequently use to reason in monoidal categories. For
this example, we permit ourselves to ignore details and
subtleties so that we do not muddy the point we mean to
illustrate.  For a detailed and complete look at string
calculi, Selinger's survey [57] provides an
excellent overview.

Given a monoidal category $ ( \C ,\otimes, I ) $, objects
are represented by certain isotopy classes of strings and
arrows are represented by nodes. This is illustrated in
Figure \ref{fig:string-diagrams}. The diagrams read from
left to right.  Now, to draw a string for an identity arrow,
we do not include the node, giving the diagram
\[
\begin{tikzpicture}
\node (1) at (0,0) {$ a $};
\node (2) at (2,0) {$ a $};
\draw [-] (1) to (2);
\end{tikzpicture}
\]
to represent $ \id \from a \to a $. Composing with $ \id $
another arrow should result in nothing changing, as captured
in this equation
\begin{center}
\begin{tikzpicture}
\node (1) at (0,0) {$ a $};
\node[circle,draw=black] (2) at (4,0) {$ f $};
\node (3) at (6,0) {$ b $};
\path[-,font=\scriptsize]
(1) edge[] (2)
(2) edge node[]{$  $} (3);
\node () at (7,0) {$ = $};
\node (1) at (8,0) {$ a $};
\node[circle,draw=black] (2) at (10,0) {$ f $};
\node (3) at (12,0) {$ b $};
\path[-,font=\scriptsize]
(1) edge node[]{$ $} (2)
(2) edge node[]{$ $} (3);
\end{tikzpicture}
\end{center}
From this, we observe that the length of the string does not
matter.  This accords with defining strings up to
isotopy. In particular, we want to have a string be
equivalent to a point.  In the parlance of this thesis, we
want to be able to rewrite a string, with two distinct
endpoints, into a single point.  Yet, this is not possible
to do with a fine rewrite rule.

\begin{figure}[h]
\centering
\fbox{
\begin{minipage}{1.0\linewidth}
\[
\begin{tikzpicture}
\node[circle,draw=black] (1) at (0,0) {$ f $};
\node (2) at (-2,0) {$ a $};
\node (3) at (2,0) {$ b $};
\path[-,font=\scriptsize]
(2) edge node[]{$  $} (1)
(1) edge node[]{$  $} (3);
\node () at (0,-1) {\scriptsize{A string representing
an arrow $ f \from a \to b $}};
\end{tikzpicture}
\quad \quad
\begin{tikzpicture}
\node[circle,draw=black] (1) at (0,0) {$ g $};
\node (2) at (-2,0.5) {$ a $};
\node (3) at (-2,-0.5) {$ b $};
\node (4) at (2,0.5) {$ a $};
\node (5) at (2,-0.5) {$ b' $};
% \draw (0,0) circle (0.5cm);
\path[-,font=\scriptsize]
(2.0) edge [bend left=10] (1.150)
(3.0) edge [bend right=10] (1.210)
(1.30) edge [bend left=10] (4.180)
(1.-30) edge [bend right=10] (5.180);
\node () at (0,-1) {\scriptsize{
A string representing an arrow
$ g \from a \otimes b \to a' \otimes b' $}};
\end{tikzpicture}
\]
\end{minipage}
\caption{String diagrams}
\label{fig:string-diagrams}
\end{figure}

Indeed, suppose we are working with strings in some topos of
spaces and we want to finely rewrite a string into a
point. Such a rewrite rule would be a span
\begin{equation} \label{eq:string-to-point}
\begin{tikzpicture}
\begin{scope}
\node (1) at (0,1) {$ \bullet $};
\node (2) at (0,0) {$ \bullet $};
\draw (1.center) -- (2.center);
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\node (l) at (0.6,0.5) {};
\end{scope}
\begin{scope}[shift={(3,0)}]
\node () at (0,0.5) {?};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\node (ml) at (-0.6,0.5) {};
\node (mr) at (0.6,0.5)  {};
\end{scope}
\begin{scope}[shift={(6,0)}]
\node (1) at (0,0.5) {$ \bullet $};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\node (r) at (-0.6,0.5) {};
\end{scope}
\draw[cd]
(ml) edge[] (l)
(mr) edge[] (r);
\end{tikzpicture}
\end{equation}
with `?' replaced by a subobject of both the string on the
left and point on the right.  Thus, `?' must either be empty
or a point. Choosing the empty string does not scale.  A
simple counter example is
\[
\begin{tikzpicture}
\begin{scope}
\node (a) at (0,0) {$ \bullet $};
\node (b) at (1,0) {$ \bullet  $};
\draw (a.center) -- (b.center);
\draw [rounded corners] (-0.5,-0.5) rectangle (2.5,0.5);
\node (01b) at (1,-0.6) {$  $};
\node (01r) at (2.6,0)  {$  $};
\end{scope}
\begin{scope}[shift={(4,0)}]
\node (c) at (1,0) {$ 0 $};
\draw [rounded corners] (-0.5,-0.5) rectangle (2.5,0.5);
\node (11l) at (-0.6,0) {$  $};
\node (11b) at (1,-0.6) {$  $};
\node (11r) at (2.6,0)  {$  $};
\end{scope}
\begin{scope}[shift={(8,0)}]
\node (c) at (1,0) {$ \bullet $};
\draw [rounded corners] (-0.5,-0.5) rectangle (2.5,0.5);
\node (21l) at (-0.6,0) {$  $};
\node (21b) at (1,-0.6) {$  $};
\end{scope}
\begin{scope}[shift={(0,-3)}]
\node (a) at (0,0)  {$ \bullet $};
\node (b) at (1,0)  {$ \bullet $};
\node (c) at (2,1)  {$ \bullet $};
\node (d) at (2,-1) {$ \bullet $};
\draw
(a.center) -- (b.center)
(b.center) -- (c.center)
(b.center) -- (d.center);
\draw [rounded corners]
(-0.5,-1.5) rectangle (2.5,1.5);
\node (00l) at (-0.6,0) {$  $};
\node (00t) at (1,1.6) {$  $};
\node (00r) at (2.6,0)  {$  $};
\end{scope}
\begin{scope}[shift={(4,-3)}]
\node () at (1,0) {?};
\draw [rounded corners]
(-0.5,-1.5) rectangle (2.5,1.5);
\node (10l) at (-0.6,0) {$  $};
\node (10t) at (1,1.6) {$  $};
\node (10r) at (2.6,0)  {$  $};
\end{scope}
\begin{scope}[shift={(8,-3)}]
\node (b) at (1,0)  {$ \bullet $};
\node (c) at (2,1)  {$ \bullet $};
\node (d) at (2,-1) {$ \bullet $};
\draw
(b.center) -- (c.center)
(b.center) -- (d.center);
\draw [rounded corners]
(-0.5,-1.5) rectangle (2.5,1.5);
\node (20l) at (-0.6,0) {$  $};
\node (20t) at (1,1.6) {$  $};
\node (20r) at (2.6,0)  {$  $};
\end{scope}
\draw[cd]
(11l) edge node[]{$  $} (01r)
(11r) edge node[]{$  $} (21l)
(10l) edge node[]{$  $} (00r)
(10r) edge node[]{$  $} (20l)
(01b) edge node[]{$  $} (00t)
(11b) edge node[]{$  $} (10t)
(21b) edge node[]{$  $} (20t);
\end{tikzpicture}
\]
To see this more clearly, we reframe the question to take
advantage of the fact that pushing out over $ 0 $ is
the same as taking a disjoint union. So we can ask whether
\begin{center}
\begin{tikzpicture}
\node (a) at (0,0)  {$ \bullet $};
\node (b) at (1,0)  {$ \bullet $};
\node (c) at (2,1)  {$ \bullet $};
\node (d) at (2,-1) {$ \bullet $};
\draw
(a.center) -- (b.center)
(b.center) -- (c.center)
(b.center) -- (d.center);
\draw [rounded corners]
(-0.5,-1.5) rectangle (2.5,1.5);
\node (00l) at (-0.6,0) {$  $};
\node (00t) at (1,1.6) {$  $};
\node (00r) at (2.6,0)  {$  $};
\end{tikzpicture}
\end{center}
is the disjoint union of
\begin{center}
\begin{tikzpicture}
\node (a) at (0,0) {$ \bullet $};
\node (b) at (1,0) {$ \bullet  $};
\draw (a.center) -- (b.center);
\draw [rounded corners] (-0.5,-0.5) rectangle (2.5,0.5);
\node (01b) at (1,-0.6) {$  $};
\node (01r) at (2.6,0)  {$  $};
\end{tikzpicture}
\end{center}
and something else. Of course, it is not.

But maybe the issue was pushing out over $ 0 $ in
the first place.  What about replacing $ 0 $ with a
point? A simple counter example to illustrate the failure of
this idea is
\[
\begin{tikzpicture}
\begin{scope}
\node (a) at (0,0) {$ \bullet $};
\node (b) at (1,0) {$ \bullet  $};
\draw (a.center) -- (b.center);
\draw [rounded corners]
(-1.5,-0.5) rectangle (2.5,0.5);
\node (01l) at (-1.6,0) {$  $};
\node (01b) at (0.5,-0.6) {$  $};
\node (01r) at (2.6,0) {$  $};
\end{scope}
\begin{scope}[shift={(5,0)}]
\node (c) at (0.5,0) {$ \bullet $};
\draw [rounded corners]
(-1.5,-0.5) rectangle (2.5,0.5);
\node (11l) at (-1.6,0) {$  $};
\node (11b) at (0.5,-0.6) {$  $};
\node (11r) at (2.6,0) {$  $};
\end{scope}
\begin{scope}[shift={(10,0)}]
\node (c) at (0.5,0) {$ \bullet $};
\draw [rounded corners]
(-1.5,-0.5) rectangle (2.5,0.5);
\node (21l) at (-1.6,0) {$  $};
\node (21b) at (0.5,-0.6) {$  $};
\node (21r) at (2.6,0) {$  $};
\end{scope}
\begin{scope}[shift={(0,-3)}]
\node (0) at (-1,1)  {$ \bullet $};
\node (1) at (-1,-1) {$ \bullet $};
\node (a) at (0,0)   {$ \bullet $};
\node (b) at (1,0)   {$ \bullet $};
\node (c) at (2,1)   {$ \bullet $};
\node (d) at (2,-1)  {$ \bullet $};
\draw
(a.center) -- (b.center)
(b.center) -- (c.center)
(b.center) -- (d.center)
(0.center) -- (a.center)
(1.center) -- (a.center);
\draw [rounded corners]
(-1.5,-1.5) rectangle (2.5,1.5);
\node (00l) at (-1.6,0) {$  $};
\node (00t) at (0.5,1.6) {$  $};
\node (00r) at (2.6,0) {$  $};
\end{scope}
\begin{scope}[shift={(5,-3)}]
\node () at (0.5,0) {?};
\draw [rounded corners]
(-1.5,-1.5) rectangle (2.5,1.5);
\node (10l) at (-1.6,0) {$  $};
\node (10t) at (0.5,1.6) {$  $};
\node (10r) at (2.6,0) {$  $};
\end{scope}
\begin{scope}[shift={(10,-3)}]
\node (0) at (-0.5,1)  {$ \bullet $};
\node (1) at (-0.5,-1) {$ \bullet $};
\node (b) at (0.5,0)  {$ \bullet $};
\node (c) at (1.5,1)  {$ \bullet $};
\node (d) at (1.5,-1) {$ \bullet $};
\draw (0.center) -- (b.center);
\draw (1.center) -- (b.center);
\draw (b.center) -- (c.center);
\draw (b.center) -- (d.center);
\draw [rounded corners]
(-1.5,-1.5) rectangle (2.5,1.5);
\node (20l) at (-1.6,0)  {$  $};
\node (20t) at (0.5,1.6) {$  $};
\node (20r) at (2.6,0)  {$  $};
\end{scope}
\draw[cd]
(11l) edge node[above]{$ \theta $} (01r)
(11r) edge node[]{$  $} (21l)
(10l) edge node[]{$  $} (00r)
(10r) edge node[]{$  $} (20l)
(01b) edge node[]{$  $} (00t)
(11b) edge node[]{$  $} (10t)
(21b) edge node[]{$  $} (20t);
\end{tikzpicture}
\]
where we define $ \theta $ to choose the left or the right
point; the failure will occur regardless of the choice.
Again, there is nothing that we can place into the center,
bottom square to give a double pushout diagram. To see why,
we use the fact that if we could fill in `?', we already
know what it must be. The right square must also be a
pushout. This forces us to fill the blank with the graph
\begin{center}
\begin{tikzpicture}
\node (0) at (-0.5,1)  {$ \bullet $};
\node (1) at (-0.5,-1) {$ \bullet $};
\node (b) at (0.5,0)  {$ \bullet $};
\node (c) at (1.5,1)  {$ \bullet $};
\node (d) at (1.5,-1) {$ \bullet $};
\draw (0.center) -- (b.center);
\draw (1.center) -- (b.center);
\draw (b.center) -- (c.center);
\draw (b.center) -- (d.center);
\draw [rounded corners]
(-1.5,-1.5) rectangle (2.5,1.5);
\node (20l) at (-1.6,0)  {$  $};
\node (20t) at (0.5,1.6) {$  $};
\node (20r) at (2.6,0)  {$  $};
\end{tikzpicture}
\end{center}
But then the left square is not a pushout.

And so, fine rewriting can be insufficient.  In this
chapter, we define bold rewriting of structured cospans
to handle situations like this one found in string
calculi. We see that, though it largely mirrors the fine
rewriting of structured cospans, it has its own character:
the bicategory we extract is a bicategory of relations.  At
the end of the chapter, we illustrate bold rewriting using
the string calculus from quantum computer science known as
the ZX-calculus.

% ===========================================================
\section{A double category of bold rewrites of structured
\label{sec:bold-rewrites}
% ===========================================================

In this section, we define a double category
$ _L\BBBoldRewrite $ whose objects are interface types,
whose vertical arrows are spans of interface types with
invertible legs, whose horizontal arrows are structured
cospans, and whose squares are bold rewrites of structured
cospans. The only difference between the definitions of
$ _L\FFFineRewrite $ and $ _L\BBBoldRewrite $ is in the
squares. The objects, horizontal arrows, and vertical arrows
are the same in each case. This winds up having an
interesting effect on the horizontal bicategory of
$ _L\BBBoldRewrite $ which we explore in Section
\ref{sec:cartesian-bicategory-spans-of-cospans}. Before
turning to that, we need to properly define
$ _L\BBBoldRewrite $, Fortunately, most of the work has been
done when constructing $ _L\FFFineRewrite $, so we
begin by defining the squares.

Recall from Definition \ref{def:span-str-cospan} that a
morphism of spans of structured cospans is an arrow
$ \theta $ that fits into a commuting diagram
\[
\begin{tikzpicture}
\node (La) at (0,4) {$ La $};
\node (Lb) at (1,2) {$ Lb $};
\node (Lc) at (2,0) {$ Lc $};
\node (x) at (3,4) {$ x $};
\node (y) at (4,3.5) {$ y $};
\node (y') at (4,0.5) {$ y' $};
\node (z) at (5,0) {$ z $};
\node (La') at (6,4) {$ La' $};
\node (Lb') at (7,2) {$ Lb' $};
\node (Lc') at (8,0) {$ Lc' $};
\draw[cd]
(Lb) edge node[]{$  $} (La)
(Lb) edge node[]{$  $} (Lc)
(Lb') edge node[]{$  $} (La')
(Lb') edge node[]{$  $} (Lc')
(y) edge node[]{$  $} (x)
(y') edge node[]{$  $} (x)
(y') edge node[]{$  $} (z)
(La) edge node[]{$  $} (x)
(La') edge node[]{$  $} (x)
(Lb) edge node[]{$  $} (y')
(Lb') edge node[]{$  $} (y');
\path[line width=0.5em,draw=white]
(Lb) edge node[]{$  $} (y)
(Lb') edge node[]{$  $} (y)
(Lc) edge node[]{$  $} (z)
(Lc') edge node[]{$  $} (z)
(y) edge node[]{$  $} (z)
(y) edge node[]{$  $} (y');
\path[cd,font=\scriptsize]
(Lb) edge node[]{$  $} (y)
(Lb') edge node[]{$  $} (y)
(Lc) edge node[]{$  $} (z)
(Lc') edge node[]{$  $} (z)
(y) edge node[]{$  $} (z)
(y) edge node[left] {$ \theta $} (y');
\end{tikzpicture}
\]

Using a morphism of structured cospans, we can define the
connected components of structured cospans.  We first define
a relation $ \sim $ setting
\[
\begin{tikzpicture}
\begin{scope}
\node (La) at (0,4) {$ La $};
\node (x) at (2,4) {$ x $};
\node (La') at (4,4) {$ La' $};
\node (Lb) at (0,2) {$ Lb $};
\node (y) at (2,2) {$ y $};
\node (Lb') at (4,2) {$ Lb' $};
\node (Lc) at (0,0) {$ Lc $};
\node (z) at (2,0) {$ z $};
\node (Lc') at (4,0) {$ Lc' $};
\draw[cd]
(La) edge node[]{$  $} (x)
(La') edge node[]{$  $} (x)
(Lb) edge node[]{$  $} (y)
(Lb') edge node[]{$  $} (y)
(Lc) edge node[]{$  $} (z)
(Lc') edge node[]{$  $} (z)
(Lb) edge node[]{$  $} (La)
(Lb) edge node[]{$  $} (Lc)
(y) edge node[]{$  $} (x)
(y) edge node[]{$  $} (z)
(Lb') edge node[]{$  $} (La')
(Lb') edge node[]{$  $} (Lc');
\end{scope}
\node () at (5,2) {$ \sim $};
\begin{scope}[shift={(6,0)}]
\node (La) at (0,4) {$ La $};
\node (x) at (2,4) {$ x $};
\node (La') at (4,4) {$ La' $};
\node (Lb) at (0,2) {$ Lb $};
\node (y) at (2,2) {$ y' $};
\node (Lb') at (4,2) {$ Lb' $};
\node (Lc) at (0,0) {$ Lc $};
\node (z) at (2,0) {$ z $};
\node (Lc') at (4,0) {$ Lc' $};
\draw[cd]
(La) edge node[]{$  $} (x)
(La') edge node[]{$  $} (x)
(Lb) edge node[]{$  $} (y)
(Lb') edge node[]{$  $} (y)
(Lc) edge node[]{$  $} (z)
(Lc') edge node[]{$  $} (z)
(Lb) edge node[]{$  $} (La)
(Lb) edge node[]{$  $} (Lc)
(y) edge node[]{$  $} (x)
(y) edge node[]{$  $} (z)
(Lb') edge node[]{$  $} (La')
(Lb') edge node[]{$  $} (Lc');
\end{scope}
\end{tikzpicture}
\]
if there is a morphism from the rewriting on the left side
of $ \sim $ to that on the right.  A \defn{connected component of
structured cospans} is an equivalence class generated by
$ \sim $. The coarseness of the classes of squares is the
most important distinction between fine and bold rewriting.

\begin{definition}[Bold rewrite]
\label{def:bold-rewrite-str-cospans}
A \defn{bold rewrite of structured cospans} is a connected
component of structured cospans whose representative has
the form
\[
\begin{tikzpicture}
\begin{scope}
\node (La)  at (0,4) {$ La $};
\node (x)   at (2,4) {$ x $};
\node (La') at (4,4) {$ La' $};
\node (Lb)  at (0,2) {$ Lb $};
\node (y)   at (2,2) {$ y $};
\node (Lb') at (4,2) {$ Lb' $};
\node (Lc)  at (0,0) {$ Lc $};
\node (z)   at (2,0) {$ z $};
\node (Lc') at (4,0) {$ Lc' $};
\draw[cd]
(La)  edge node[]{$  $} (x)
(La') edge node[]{$  $} (x)
(Lb)  edge node[]{$  $} (y)
(Lb') edge node[]{$  $} (y)
(Lc)  edge node[]{$  $} (z)
(Lc') edge node[]{$  $} (z)
(Lb)  edge node[left]{$ \iso  $} (La)
(Lb)  edge node[left]{$ \iso  $} (Lc)
(y)   edge node[]{$  $} (x)
(y)   edge node[]{$  $} (z)
(Lb') edge node[right]{$ \iso $} (La')
(Lb') edge node[right]{$ \iso $} (Lc');
\end{scope}
\end{tikzpicture}
\]
\end{definition}

The horizontal and vertical compositions for bold rewrites
of structured cospans are defined in the same way as for
fine rewrites. The classes are different, but the operation
on the class representatives work in the same way.

\begin{definition}
\label{def:composition-bold-rewrites}
The \defn{horizontal composition} $ \hcirc $ of bold
rewrites of structured cospans are defined by
the operation
\[
\begin{tikzpicture}
\begin{scope}
\node (La)  at (0,4) {$ La $};
\node (x)   at (2,4) {$ x $};
\node (La') at (4,4) {$ La' $};
\node (Lb)  at (0,2) {$ Lb $};
\node (y)   at (2,2) {$ y $};
\node (Lb') at (4,2) {$ Lb' $};
\node (Lc)  at (0,0) {$ Lc $};
\node (z)   at (2,0) {$ z $};
\node (Lc') at (4,0) {$ Lc' $};
\draw[cd]
(La)  edge node[]{$  $} (x)
(La') edge node[]{$  $} (x)
(Lb)  edge node[]{$  $} (y)
(Lb') edge node[]{$  $} (y)
(Lc)  edge node[]{$  $} (z)
(Lc') edge node[]{$  $} (z)
(Lb)  edge node[]{$  $} (La)
(Lb)  edge node[]{$  $} (Lc)
(y)   edge node[]{$  $} (x)
(y)   edge node[]{$  $} (z)
(Lb') edge node[]{$  $} (La')
(Lb') edge node[]{$  $} (Lc');
\end{scope}
\node () at (5,2) {$ \hcirc $};
\begin{scope}[shift={(6,0)}]
\node (La)  at (0,4) {$ La' $};
\node (x)   at (2,4) {$ x' $};
\node (La') at (4,4) {$ La'' $};
\node (Lb)  at (0,2) {$ Lb' $};
\node (y)   at (2,2) {$ y' $};
\node (Lb') at (4,2) {$ Lb'' $};
\node (Lc)  at (0,0) {$ Lc' $};
\node (z)   at (2,0) {$ z' $};
\node (Lc') at (4,0) {$ Lc'' $};
\draw[cd]
(La)  edge node[]{$  $} (x)
(La') edge node[]{$  $} (x)
(Lb)  edge node[]{$  $} (y)
(Lb') edge node[]{$  $} (y)
(Lc)  edge node[]{$  $} (z)
(Lc') edge node[]{$  $} (z)
(Lb)  edge node[]{$  $} (La)
(Lb)  edge node[]{$  $} (Lc)
(y)   edge node[]{$  $} (x)
(y)   edge node[]{$  $} (z)
(Lb') edge node[]{$  $} (La')
(Lb') edge node[]{$  $} (Lc');
\end{scope}
\node () at (11,2) {$ \bydef  $};
\end{tikzpicture}
\]
\[
\begin{tikzpicture}
\begin{scope}[shift={(0,0)}]
\node (La)  at (0,4) {$ La $};
\node (x)   at (3,4) {$ x +_{La'} x' $};
\node (La') at (6,4) {$ La'' $};
\node (Lb)  at (0,2) {$ Lb $};
\node (y)   at (3,2) {$ y +_{Lb'} y' $};
\node (Lb') at (6,2) {$ Lb'' $};
\node (Lc)  at (0,0) {$ Lc $};
\node (z)   at (3,0) {$ z +_{Lc'} z' $};
\node (Lc') at (6,0) {$ Lc'' $};
\draw[cd]
(La)  edge node[]{$  $} (x)
(La') edge node[]{$  $} (x)
(Lb)  edge node[]{$  $} (y)
(Lb') edge node[]{$  $} (y)
(Lc)  edge node[]{$  $} (z)
(Lc') edge node[]{$  $} (z)
(Lb)  edge node[]{$  $} (La)
(Lb)  edge node[]{$  $} (Lc)
(y)   edge node[]{$  $} (x)
(y)   edge node[]{$  $} (z)
(Lb') edge node[]{$  $} (La')
(Lb') edge node[]{$  $} (Lc');
\end{scope}
\end{tikzpicture}
\]
The \defn{vertical composition} of bold rewrites of structured
cospans is defined by
\[
\begin{tikzpicture}
\begin{scope}
\node (La)  at (0,4) {$ La $};
\node (x)   at (2,4) {$ v $};
\node (La') at (4,4) {$ La' $};
\node (Lb)  at (0,2) {$ Lb $};
\node (y)   at (2,2) {$ w $};
\node (Lb') at (4,2) {$ Lb' $};
\node (Lc)  at (0,0) {$ Lc $};
\node (z)   at (2,0) {$ x $};
\node (Lc') at (4,0) {$ Lc' $};
\draw[cd]
(La)  edge node[]{$  $} (x)
(La') edge node[]{$  $} (x)
(Lb)  edge node[]{$  $} (y)
(Lb') edge node[]{$  $} (y)
(Lc)  edge node[]{$  $} (z)
(Lc') edge node[]{$  $} (z)
(Lb)  edge node[]{$  $} (La)
(Lb)  edge node[]{$  $} (Lc)
(y)   edge node[]{$  $} (x)
(y)   edge node[]{$  $} (z)
(Lb') edge node[]{$  $} (La')
(Lb') edge node[]{$  $} (Lc');
\end{scope}
\node () at (5,2) {$ \hcirc $};
\begin{scope}[shift={(6,0)}]
\node (La)  at (0,4) {$ Lc $};
\node (x)   at (2,4) {$ x $};
\node (La') at (4,4) {$ Lc' $};
\node (Lb)  at (0,2) {$ Ld $};
\node (y)   at (2,2) {$ y $};
\node (Lb') at (4,2) {$ Ld' $};
\node (Lc)  at (0,0) {$ Le $};
\node (z)   at (2,0) {$ z $};
\node (Lc') at (4,0) {$ Le' $};
\draw[cd]
(La)  edge node[]{$  $} (x)
(La') edge node[]{$  $} (x)
(Lb)  edge node[]{$  $} (y)
(Lb') edge node[]{$  $} (y)
(Lc)  edge node[]{$  $} (z)
(Lc') edge node[]{$  $} (z)
(Lb)  edge node[]{$  $} (La)
(Lb)  edge node[]{$  $} (Lc)
(y)   edge node[]{$  $} (x)
(y)   edge node[]{$  $} (z)
(Lb') edge node[]{$  $} (La')
(Lb') edge node[]{$  $} (Lc');
\end{scope}
\node () at (11,2) {$ \bydef  $};
\end{tikzpicture}
\]
\[
\begin{tikzpicture}
\begin{scope}[shift={(0,0)}]
\node (La)  at (0,4) {$ La $};
\node (x)   at (3,4) {$ v $};
\node (La') at (6,4) {$ La' $};
\node (Lb)  at (0,2) {$ Lb \times_{Lc} Ld $};
\node (y)   at (3,2) {$ w \times_{x} y $};
\node (Lb') at (6,2) {$ Lb' \times_{Lc'} Ld' $};
\node (Lc)  at (0,0) {$ Le $};
\node (z)   at (3,0) {$ z $};
\node (Lc') at (6,0) {$ Le' $};
\draw[cd]
(La)  edge node[]{$  $} (x)
(La') edge node[]{$  $} (x)
(Lb)  edge node[]{$  $} (y)
(Lb') edge node[]{$  $} (y)
(Lc)  edge node[]{$  $} (z)
(Lc') edge node[]{$  $} (z)
(Lb)  edge node[]{$  $} (La)
(Lb)  edge node[]{$  $} (Lc)
(y)   edge node[]{$  $} (x)
(y)   edge node[]{$  $} (z)
(Lb') edge node[]{$  $} (La')
(Lb') edge node[]{$  $} (Lc');
\end{scope}
\end{tikzpicture}
\]
\end{definition}

Unlike for fine rewrites of structured cospans, the
interchange law is straightforward to prove. The coarser
classes of rewrites of structured cospans vastly simplifies
concocting the isomorphism.

\begin{lemma}
\label{thm:bold-interchange}
\[
\begin{tikzpicture}
\node ()    at (-1,2) {$ \alpha \bydef $};
\node (La)  at (0,4) {$ La $};
\node (x)   at (2,4) {$ v $};
\node (La') at (4,4) {$ La' $};
\node (Lb)  at (0,2) {$ Lb $};
\node (y)   at (2,2) {$ w $};
\node (Lb') at (4,2) {$ Lb' $};
\node (Lc)  at (0,0) {$ Lc $};
\node (z)   at (2,0) {$ x $};
\node (Lc') at (4,0) {$ Lc' $};
\draw [cd]
(La)  edge node[]{$  $} (x)
(La') edge node[]{$  $} (x)
(Lb)  edge node[]{$  $} (y)
(Lb') edge node[]{$  $} (y)
(Lc)  edge node[]{$  $} (z)
(Lc') edge node[]{$  $} (z)
(Lb)  edge node[]{$  $} (La)
(Lb)  edge node[]{$  $} (Lc)
(y)   edge node[]{$  $} (x)
(y)   edge node[]{$  $} (z)
(Lb') edge node[]{$  $} (La')
(Lb') edge node[]{$  $} (Lc');
\end{tikzpicture}
\quad \quad \quad \quad
\begin{tikzpicture}
\node ()    at (-1,2) {$ \alpha' \bydef $};
\node (La)  at (0,4) {$ La' $};
\node (x)   at (2,4) {$ v' $};
\node (La') at (4,4) {$ La'' $};
\node (Lb)  at (0,2) {$ Lb' $};
\node (y)   at (2,2) {$ w' $};
\node (Lb') at (4,2) {$ Lb'' $};
\node (Lc)  at (0,0) {$ Lc' $};
\node (z)   at (2,0) {$ x' $};
\node (Lc') at (4,0) {$ Lc'' $};
\draw[cd]
(La)  edge node[]{$  $} (x)
(La') edge node[]{$  $} (x)
(Lb)  edge node[]{$  $} (y)
(Lb') edge node[]{$  $} (y)
(Lc)  edge node[]{$  $} (z)
(Lc') edge node[]{$  $} (z)
(Lb)  edge node[]{$  $} (La)
(Lb)  edge node[]{$  $} (Lc)
(y)   edge node[]{$  $} (x)
(y)   edge node[]{$  $} (z)
(Lb') edge node[]{$  $} (La')
(Lb') edge node[]{$  $} (Lc');
\end{tikzpicture}
\]
\[
\begin{tikzpicture}
\node ()    at (-1,2) {$ \beta \bydef $};
\node (La)  at (0,4) {$ Lc $};
\node (x)   at (2,4) {$ x $};
\node (La') at (4,4) {$ Lc' $};
\node (Lb)  at (0,2) {$ Ld $};
\node (y)   at (2,2) {$ y $};
\node (Lb') at (4,2) {$ Ld' $};
\node (Lc)  at (0,0) {$ Le $};
\node (z)   at (2,0) {$ z $};
\node (Lc') at (4,0) {$ Le' $};
\draw[cd]
(La)  edge node[]{$  $} (x)
(La') edge node[]{$  $} (x)
(Lb)  edge node[]{$  $} (y)
(Lb') edge node[]{$  $} (y)
(Lc)  edge node[]{$  $} (z)
(Lc') edge node[]{$  $} (z)
(Lb)  edge node[]{$  $} (La)
(Lb)  edge node[]{$  $} (Lc)
(y)   edge node[]{$  $} (x)
(y)   edge node[]{$  $} (z)
(Lb') edge node[]{$  $} (La')
(Lb') edge node[]{$  $} (Lc');
\end{tikzpicture}
\quad \quad \quad \quad
\begin{tikzpicture}
\node ()    at (-1,2) {$ \beta' \bydef $};
\node (La)  at (0,4) {$ Lc' $};
\node (x)   at (2,4) {$ x' $};
\node (La') at (4,4) {$ Lc'' $};
\node (Lb)  at (0,2) {$ Ld' $};
\node (y)   at (2,2) {$ y' $};
\node (Lb') at (4,2) {$ Ld'' $};
\node (Lc)  at (0,0) {$ Le' $};
\node (z)   at (2,0) {$ z' $};
\node (Lc') at (4,0) {$ Le'' $};
\draw[cd]
(La)  edge node[]{$  $} (x)
(La') edge node[]{$  $} (x)
(Lb)  edge node[]{$  $} (y)
(Lb') edge node[]{$  $} (y)
(Lc)  edge node[]{$  $} (z)
(Lc') edge node[]{$  $} (z)
(Lb)  edge node[]{$  $} (La)
(Lb)  edge node[]{$  $} (Lc)
(y)   edge node[]{$  $} (x)
(y)   edge node[]{$  $} (z)
(Lb') edge node[]{$  $} (La')
(Lb') edge node[]{$  $} (Lc');
\end{tikzpicture}
\]
be bold rewrites of structured cospans. Then
\[
( \alpha \hcirc \alpha' ) \vcirc ( \beta \hcirc \beta' )
( \alpha \vcirc \beta ) \hcirc ( \alpha' \vcirc \beta' ).
\]
That is, the interchange law holds.
\end{lemma}

\begin{proof}
The left hand side of the equation is the bold rewrite of
structured cospans
\[
\begin{tikzpicture}
\begin{scope}
\node (La)  at (0,4) {$ La $};
\node (x)   at (5,4) {$ v +_{La'} v' $};
\node (La') at (10,4) {$ La'' $};
\node (Lb)  at (0,2) {$ Lb \times_{Lc} Ld $};
\node (y)   at (5,2)
{$ ( w +_{Lb'} w' )
\times_{( x +_{Lc'} x' )}
( y \times_{Ld'} y') $};
\node (Lb') at (10,2) {$ Lb \times_{Lc'} Ld' $};
\node (Lc)  at (0,0) {$ Le $};
\node (z)   at (5,0) {$ z +_{Le'} z' $};
\node (Lc') at (10,0) {$ Le'' $};
\draw[cd]
(La)  edge node[]{$  $} (x)
(La') edge node[]{$  $} (x)
(Lb)  edge node[]{$  $} (y)
(Lb') edge node[]{$  $} (y)
(Lc)  edge node[]{$  $} (z)
(Lc') edge node[]{$  $} (z)
(Lb)  edge node[]{$  $} (La)
(Lb)  edge node[]{$  $} (Lc)
(y)   edge node[]{$  $} (x)
(y)   edge node[]{$  $} (z)
(Lb') edge node[]{$  $} (La')
(Lb') edge node[]{$  $} (Lc');
\end{scope}
\end{tikzpicture}
\]
while the right hand side is
\[
\begin{tikzpicture}
\begin{scope}
\node (La)  at (0,4) {$ La $};
\node (x)   at (5,4) {$ v +_{La'} v' $};
\node (La') at (10,4) {$ La'' $};
\node (Lb)  at (0,2) {$ Lb \times_{Lc} Ld $};
\node (y)   at (5,2)
{$ ( w \times_{x} y)
+_{(Lb' \times_{Lc'} Ld')}
( w' \times_{x'} y' ) $};
\node (Lb') at (10,2) {$ Lb \times_{Lc'} Ld' $};
\node (Lc)  at (0,0) {$ Le $};
\node (z)   at (5,0) {$ z +_{Le'} z' $};
\node (Lc') at (10,0) {$ Le'' $};
\draw[cd]
(La)  edge node[]{$  $} (x)
(La') edge node[]{$  $} (x)
(Lb)  edge node[]{$  $} (y)
(Lb') edge node[]{$  $} (y)
(Lc)  edge node[]{$  $} (z)
(Lc') edge node[]{$  $} (z)
(Lb)  edge node[]{$  $} (La)
(Lb)  edge node[]{$  $} (Lc)
(y)   edge node[]{$  $} (x)
(y)   edge node[]{$  $} (z)
(Lb') edge node[]{$  $} (La')
(Lb') edge node[]{$  $} (Lc');
\end{scope}
\end{tikzpicture}
\]
To show that these are equal as bold rewrites of
structured cospans, it suffices to find a \emph{morphism} between
them. Precisely, we need a morphism
\[
( w\times_{x}y )
+_{( Lb'\times_{Lc'}Ld')}
(w'\times_{x'}y' )
\to
( w+_{Lb'}w' )
\times_{(x+_{Lc'}x')}
( y\times_{Ld'}y')
\]

We can obtain the two objects as follows. Let $ \C $ be
the walking cospan category $ \{ \bullet \to \bullet \gets
\bullet \} $ and let $ \S $ be the walking span category $
\{ \bullet \gets \bullet \to \bullet \} $.  Then $ \C
\times \S $ is the walking cospan of spans category
\[
\begin{tikzpicture}
\begin{scope}
\node (1) at (0,4) {$ \bullet $};
\node (2) at (2,4) {$ \bullet $};
\node (3) at (4,4) {$ \bullet $};
\node (4) at (0,2) {$ \bullet $};
\node (5) at (2,2) {$ \bullet $};
\node (6) at (4,2) { $ \bullet $};
\node (7) at (0,0) {$ \bullet $};
\node (8) at (2,0) {$ \bullet $};
\node (9) at (4,0) {$ \bullet $};
\draw[cd]
(1) edge node[]{$  $} (4)
(7) edge node[]{$  $} (4)
(2) edge node[]{$  $} (5)
(8) edge node[]{$  $} (5)
(3) edge node[]{$  $} (6)
(9) edge node[]{$  $} (6)
(2) edge node[]{$  $} (1)
(2) edge node[]{$  $} (3)
(5) edge node[]{$  $} (4)
(5) edge node[]{$  $} (6)
(8) edge node[]{$  $} (7)
(8) edge node[]{$  $} (9);
\end{scope}
\draw [rounded corners]
(-1,-1) rectangle (5,5);
\end{tikzpicture}
\]
Let $ F \from \C \times \S \to \X $ be the functor that
returns the diagram
\[
\begin{tikzpicture}
\begin{scope}
\node (1) at (0,4) {$ w $};
\node (2) at (2,4) {$ Lb' $};
\node (3) at (4,4) {$ w' $};
\node (4) at (0,2) {$ x $};
\node (5) at (2,2) {$ Lc' $};
\node (6) at (4,2) { $ x' $};
\node (7) at (0,0) {$ y $};
\node (8) at (2,0) {$ Ld' $};
\node (9') at (4,0) {$ y' $};
\draw[cd]
(1) edge node[]{$  $} (4)
(7) edge node[]{$  $} (4)
(2) edge node[]{$  $} (5)
(8) edge node[]{$  $} (5)
(3) edge node[]{$  $} (6)
(9) edge node[]{$  $} (6)
(2) edge node[]{$  $} (1)
(2) edge node[]{$  $} (3)
(5) edge node[]{$  $} (4)
(5) edge node[]{$  $} (6)
(8) edge node[]{$  $} (7)
(8) edge node[]{$  $} (9);
\end{scope}
\end{tikzpicture}
\]
which is the middle of the diagram obtained by gluing $
\alpha$, $ \beta $, $ \alpha' $, and $ \beta' $ together
along their coinciding edges.  There is a canonical
morphism of type
\[
\colim\limits_\S \lim_\C F \to
\lim_\C \colim\limits_\S F
\]
where the domain is the image of $ F $ under the composite functor
\[
\X^{\C \times \S} \xto{\iso}
( \X^\C )^\S \xto{\lim_\C}
\X^\S \xto{\colim_\S} \X
\]
and the domain is the image of $ F $ under the composite
\[
\X^{\C \times \S} \xto{\iso}
( \X^\S )^\C \xto{\colim_\S}
\X^\C \xto{\lim_\C} \X.
\]
One can check that this canonical morphism gives the
morphism of bold rewrites of structured cospans we need.
\end{proof}

% ===================================================

\section{A bicategory of relations for bold
rewriting of structured cospans}
\label{sec:cartesian-bicategory-spans-of-cospans}
% ==================================================

There are two philosophies in rewriting. One is that we care
about how one object is rewritten into another, and so we
keep track of certain data to describe the rewriting.  The
other perspective is that we do not care about \emph{how} an
object is rewritten into another, only that the rewriting is
possible.  Bold rewriting of structured cospans belongs to
the latter philosophy. This is realized explicitly through
the fact that the horizontal bicategory forms a bicategory
of relations, specifically that it is locally posetal.
Appendix \ref{sec:cartesian-bicategories} discusses the
theory of such bicategories.

The first goal of this section is to define the bicategory
in question.  We take the same approach as finding the
horizontal bicategory of fine rewrites of structured cospans
in Section
\ref{sec:compact-closed-bicategory-spans-of-cospans}.  After
extracting the bicategory, we show that it is a bicategory
of relations (see Definition \ref{def:bicat-relations}).

This next theorem is proved with virtually the same argument
as Lemma \ref{lem:SpanCospanSM}.

\begin{theorem}
$ _L \BBBoldRewrite $ is a symmetric monoidal double
\end{theorem}

From here, we prove a series of lemmas that, when put
together, prove that the horizontal bicategory
$ _L \BBoldRewrite $ of $ _L \BBBoldRewrite $ is a
bicategory of relations. The first lemma in this string is
proved by replicating the proof of Lemma
\ref{lem:SpanCospanIsofibrant} and the second follows
from Theorem \ref{thm:horz-bicat}.

\begin{lemma}
$ _L \BBBoldRewrite $ is isofibrant.
\end{lemma}

\begin{lemma}
$ _L \BBoldRewrite $ is a symmetric monoidal bicategory.
\end{lemma}

In the following lemma, we use
$ \nabla \bydef [ \id,\id] \from a + a \to a $ to
denote the codiagonal map and $ ! $ to denote a canonical
arrow from the initial object.

\begin{lemma}
For each object $ a $ of $ _L \BBoldRewrite $, define
\[
\Delta_a \from a \to a + a
\quad \text{and} \quad
\varepsilon_a \from a \to 0
\]
to be the structured cospans
\[
La \xto{\id} La \xgets{L\nabla_a} L(a+a)
\quad \text{and} \quad
La \xto{\id} La \xgets{!} L0
\]
respectively. Then $ (a , \Delta_a , \varepsilon_a ) $ is
a cocommutative comonoid.
\end{lemma}

\begin{proof}
Proving this amounts to showing that the
coassociativity, counitality, and
cocommutativity diagrams commute.
The coassociativity diagram
\[
\begin{tikzpicture}
\node (01) at (0,2) {$ a $};
\node (21) at (6,2) {$ a+a $};
\node (00) at (0,0) {$ a+a $};
\node (10) at (3,0) {$ a+(a+a) $};
\node (20) at (6,0) {$ (a+a)+a $};
\draw[cd]
(01) edge node[above]{$ \nabla $} (21)
(01) edge node[left]{$ \nabla $} (00)
(00) edge node[below]{$ \alpha $} (10)
(10) edge node[below]{$ \id \otimes \nabla $} (20)
(21) edge node[right]{$ \nabla \otimes \id $} (20);
\end{tikzpicture}
\]
commutes because the top path, which is the composite
\[
\begin{tikzpicture}
\node (00) at (0,0) {$ La $};
\node (10) at (4,0) {$ L(a+a) $};
\node (20) at (8,0) {$ L((a+a)+a) $};
\node (01) at (2,2) {$ La $};
\node (11) at (6,2) {$ L((a+a)+a $};
\node (12) at (4,4) {$ La $};
\draw[cd]
(00) edge node[above,left]{$ \id $} (01)
(10) edge node[above,right]{$ L\nabla $} (01)
(10) edge node[above,left]{$ \id $} (11)
(20) edge node[above,right]{$ L(\nabla + \id) $} (11)
(01) edge node[above,left]{$ \id $} (12)
(11) edge node[above,right]{$ L\nabla $} (12);
\draw (3.9,3.5) -- (4,3.4) -- (4.1,3.5);
\end{tikzpicture}
\]
equals the bottom path, which is the composite
\[
\begin{tikzpicture}
\node (00) at (0,0) {$ La $};
\node (10) at (4,0) {$ L(a+a) $};
\node (20) at (8,0) {$ L(a+(a+a)) $};
\node (30) at (12,0) {$ L((a+a)+a $};
\node (01) at (2,2) {$ La $};
\node (11) at (6,2) {$ L(a+a) $};
\node (21) at (10,2) {$ L(a+(a+a)) $};
\node (02) at (4,4) {$ La $};
\node (12) at (8,4) {$ L(a+a) $};
\node (03) at (6,6) {$ La $};
\draw[cd]
(00) edge node[above,left]{$ \id $} (01)
(10) edge node[above,right]{$ L\nabla $} (01)
(10) edge node[above,left]{$ \id $} (11)
(20) edge node[above,right]{$ L(\id + \nabla) $} (11)
(20) edge node[above,left]{$ \id  $} (21)
(30) edge node[above,right]{$ L(\alpha) $} (21)
(01) edge node[above,left]{$ \id $} (02)
(11) edge node[above,right]{$ L\nabla $} (02)
(11) edge node[above,left]{$ \id $} (12)
(21) edge node[above,right]{$ L(\id + \nabla) $} (12)
(02) edge node[above,left]{$ \id $} (03)
(12) edge node[above,right]{$ L\nabla $} (03);
\draw (3.9,3.5) -- (4,3.4) -- (4.1,3.5);
\draw (7.9,3.5) -- (8,3.4) -- (8.1,3.5);
\draw (5.9,5.5) -- (6,5.4) -- (6.1,5.5);
\end{tikzpicture}
\]
The counitality diagram
\[
\begin{tikzpicture}
\node (11) at (0,0) {$ 0 \otimes a $};
\node (21) at (3,0) {$ a \otimes a $};
\node (31) at (6,0) {$ a \otimes 0 $};
\node (12) at (3,2) {$ a $};
\draw[cd]
(12) edge node[left]{$ \lambda $} (11)
(12) edge node[right]{$ \nabla $} (21)
(12) edge node[right]{$ \rho $} (31)
(21) edge node[below]{$ \epsilon \otimes \id $} (11)
(21) edge node[below]{$ \id \otimes \epsilon $} (31);
\end{tikzpicture}
\]
commutes because the composite
\[
\begin{tikzpicture}
\node (11) at (0,0)   {$ La $};
\node (21) at (4,0)   {$ L(a+a) $};
\node (31) at (8,0)   {$ La $};
\node (12) at (2,2) {$ La $};
\node (22) at (6,2) {$ L(a+a) $};
\node (13) at (4,4)   {$ L(0+a) $};
\draw[cd]
(11) edge node[above,left]{$ \id $} (12)
(21) edge node[above,right]{$ L\nabla $} (12)
(21) edge node[above,left]{$ \id $} (22)
(31) edge node[above,right]{$ L(!+\id) $} (22)
(12) edge node[above,left]{$ \id $} (13)
(22) edge node[above,right]{$ L\nabla $} (13);
\draw (3.9,3.5) -- (4,3.4) -- (4.1,3.5);
\end{tikzpicture}
\]
is equal to the left unitor and
\[
\begin{tikzpicture}
\node (11) at (0,0)   {$ La $};
\node (21) at (4,0)   {$ L(a+a) $};
\node (31) at (8,0)   {$ La $};
\node (12) at (2,2) {$ La $};
\node (22) at (6,2) {$ L(a+a) $};
\node (13) at (4,4)   {$ La $};
\draw[cd]
(11) edge node[above,left]{$ \id $} (12)
(21) edge node[above,right]{$ L\nabla $} (12)
(21) edge node[above,left]{$ \id $} (22)
(31) edge node[above,right]{$ L(\id+!) $} (22)
(12) edge node[above,left]{$ \id $} (13)
(22) edge node[above,right]{$ L\nabla $} (13);
\draw (3.9,3.5) -- (4,3.4) -- (4.1,3.5);
\end{tikzpicture}
\]
is the right unitor. Finally, the cocommutative
\[
\begin{tikzpicture}
\node (11) at (0,0) {$ a \otimes a $};
\node (21) at (4,0) {$ a \otimes a $};
\node (12) at (2,2) {$ a $};
\draw[cd]
(12) edge node[above,left]{$ \nabla $} (11)
(12) edge node[above,right]{$ \nabla $} (21)
(11) edge node[below]{$ \beta $} (21);
\end{tikzpicture}
\]
commutes because the composite $ \nabla \beta $
is given by
\[
\begin{tikzpicture}
\node (11) at (0,0) {$ La $};
\node (21) at (4,0) {$ L(a+a) $};
\node (31) at (8,0) {$ L(a+a) $};
\node (12) at (2,2) {$ La $};
\node (22) at (6,2) {$ L(a+a) $};
\node (13) at (4,4) {$ La $};
\draw[cd]
(11) edge node[above,left]{$ \id $} (12)
(21) edge node[above,right]{$ L\nabla $} (12)
(21) edge node[above,left]{$ \beta $} (22)
(31) edge node[above,right]{$ \id $} (22)
(12) edge node[above,left]{$ \id $} (13)
(22) edge node[above,right]{$ L\nabla $}
\draw (3.9,3.5) -- (4,3.4) -- (4.1,3.5);
\end{tikzpicture}
\]
which is exactly the comuliplication.
\end{proof}

In the following lemma, we follow the convention of writing
$ f \leq g $ to represent a 2-arrow from $ f $ to $ g $ in a
locally posetal bicategory.  This notation is faithful to
the fact that the hom-categories are actually hom-posets.  This
is discussed further in Section
\ref{sec:cartesian-bicategories}.

\begin{lemma}
Let $ (a,\Delta_a,\varepsilon_a) $ and
$ ( b,\Delta_b,\varepsilon_b ) $ be cocommutative comonoid
objects in the double category $ _L \BBoldRewrite $. Every structured cospan $
La \to x \gets Lb $ in $ _L \BBoldRewrite $ is a lax comonoid
homomorphism. That is,
\[
\Delta_b x \leq (x + x) \Delta_a
\quad \text{and} \quad
\varepsilon_b x \leq \varepsilon a
\]
\end{lemma}

\begin{proof}
The first 2-arrow is
\[
\begin{tikzpicture}
\node (11) at (3,0) {$ La +_{L(a+a)} (x+x) $};
\node (12) at (0,2) {$ La $};
\node (22) at (3,2) {$ La +_{L(a+a)} (x+x) $};
\node (32) at (9,2) {$ L(b+b) $};
\node (13) at (3,4) {$ x $};
\node (3'2) at (6,2) {$ x+x $};
\draw[cd]
(12) edge node[above,left]{$ f $} (13)
(12) edge node[above]{$ \psi $} (22)
(12) edge node[left]{$ \psi $} (11)
(32) edge node[above]{$ \langle g,g \rangle $} (13)
(32) edge node[above]{$ g+g $} (3'2)
(3'2) edge node[above]{$ \theta $} (22)
(3'2) edge node[right]{$ \nabla $} (13)
(32) edge node[right]{$ \theta (g+g) $} (11)
(22) edge [dashed] node[left]{$  $} (13)
(22) edge node[left]{$ \id $} (11);
\end{tikzpicture}
\]
where the dashed line is the universal arrow
formed in reference to $ f $ and $ \nabla
$. The source of this 2-arrow is the composite
\[
\begin{tikzpicture}
\node (11) at (0,0) {$ La $};
\node (21) at (4,0) {$ Lb $};
\node (31) at (8,0) {$ L(b+b) $};
\node (12) at (2,2) {$ x $};
\node (22) at (6,2) {$ Lb $};
\node (13) at (4,4) {$ x $};
\draw[cd]
(11) edge node[above,left]{$ f $} (12)
(21) edge node[above,right]{$ g $} (12)
(21) edge node[above,left]{$ \id $} (22)
(31) edge node[above,right]{$ L\nabla $} (22)
(12) edge node[above,left]{$ \id $} (13)
(22) edge node[above,right]{$ g $} (13);
\draw (3.9,3.5) -- (4,3.4) -- (4.1,3.5);
\end{tikzpicture}
\]
and the target is the composite
\[
\begin{tikzpicture}
\node (11) at (0,0)   {$ La $};
\node (21) at (4,0)   {$ L(a+a) $};
\node (31) at (8,0)   {$ L(b+b) $};
\node (12) at (2,2) {$ La $};
\node (22) at (6,2) {$ x+x $};
\node (13) at (4,4)   {$ La +_{L(a+a)} (x+x) $};
\draw[cd]
(11) edge node[above,left]{$ \id $} (12)
(21) edge node[above,right]{$ L\nabla $} (12)
(21) edge node[above,left]{$ f+f $} (22)
(31) edge node[above,right]{$ g+g $} (22)
(12) edge node[above,left]{$ \psi $} (13)
(22) edge node[above,right]{$ \theta $} (13);
\draw (3.9,3.5) -- (4,3.4) -- (4.1,3.5);
\end{tikzpicture}
\]
The second is witnessed by the 2-arrow
\[
\begin{tikzpicture}
\node (11) at (2,0) {$ x $};
\node (12) at (0,2) {$ La $};
\node (22) at (2,2) {$ La $};
\node (32) at (4,2) {$ L0 $};
\node (13) at (2,4) {$ La $};
\draw[cd]
(12) edge node[above]{$ \id $} (13)
(12) edge node[above]{$ \id $} (22)
(12) edge node[below]{$ f $} (11)
(32) edge node[above]{$ ! $} (13)
(32) edge node[above]{$ ! $} (22)
(32) edge node[below]{$ ! $} (11)
(22) edge node[left]{$ \id $} (13)
(22) edge node[left]{$ f $} (11);
\end{tikzpicture}
\]
where target 2-arrow is the composite
\[
\begin{tikzpicture}
\node (11) at (0,0)   {$ La $};
\node (21) at (4,0)   {$ Lb $};
\node (31) at (8,0)   {$ L0 $};
\node (12) at (2,2) {$ x $};
\node (22) at (6,2) {$ Lb $};
\node (13) at (4,4)   {$ x $};
\draw[cd]
(11) edge node[above]{$ f $} (12)
(21) edge node[above]{$ g $} (12)
(21) edge node[above]{$ \id $} (22)
(31) edge node[above]{$ ! $} (22)
(12) edge node[above]{$ \id $} (13)
(22) edge node[above]{$ g $} (13);
\draw (3.9,3.5) -- (4,3.4) -- (4.1,3.5);
\end{tikzpicture}
\qedhere
\]
\end{proof}

\begin{lemma}
For any object $ a $ in $ _L \BBoldRewrite $, each
cocommutative comonoid structure map
\[
\nabla \bydef
\left(
La \xto{\id} La \xgets{L\nabla_a} L(a+a)
\right)
\quad \text{ and } \quad
\epsilon \bydef
\left(
La \xto{\id} La \xgets{!} L0
\right)
\]
has a right adjoint (see Definition
\ref{def:adjoint-in-bicat}), respectively,
\[
\nabla^\ast \bydef
\left(
L(a+a) \xto{L\nabla_a} La \xgets{\id} La
\right)
\quad \text{ and } \quad
\epsilon^\ast \bydef
\left(
L0 \xto{!} La \xgets{\id} La \right).
\]
\end{lemma}

\begin{proof}
The unit of the adjunction
$ \nabla \dashv \nabla^\ast $ is
\[
\begin{tikzpicture}
\node (11) at (4,0) {$ La $};
\node (12) at (0,2) {$ La $};
\node (22) at (4,2) {$ La $};
\node (32) at (8,2) {$ La $};
\node (13) at (4,4) {$ La $};
\draw[cd]
(12) edge node[above,left]{$ \id $} (13)
(12) edge node[above]{$ \id $} (22)
(12) edge node[below,left]{$ \id $} (11)
(32) edge node[above,right]{$ \id $} (13)
(32) edge node[above]{$ \id $} (22)
(32) edge node[below,left]{$ \id $} (11)
(22) edge node[left]{$ \id $} (13)
(22) edge node[left]{$ \id $} (11);
\end{tikzpicture}
\]
where the target is the composite 1-arrow
\[
\begin{tikzpicture}
\node (11) at (0,0)   {$ La $};
\node (21) at (4,0)   {$ L(a+a) $};
\node (31) at (8,0)   {$ La $};
\node (12) at (2,2) {$ La $};
\node (22) at (6,2) {$ La $};
\node (13) at (4,4)   {$ La $};
\draw[cd]
(11) edge node[above,left]{$ \id $} (12)
(21) edge node[above,right]{$ \nabla $} (12)
(21) edge node[above,left]{$ \nabla $} (22)
(31) edge node[above,right]{$ \id $} (22)
(12) edge node[above,left]{$ \id $} (13)
(22) edge node[above,right]{$ \id $} (13);
\draw (3.9,3.5) -- (4,3.4) -- (4.1,3.5);
\end{tikzpicture}
\]
The counit of $ \nabla \dashv \nabla^\ast $ is
the 2-arrow
\[
\begin{tikzpicture}
\node (11) at (4,0) {$ L(a+a) $};
\node (12) at (0,2) {$ L(a+a) $};
\node (22) at (4,2) {$ L(a+a) $};
\node (32) at (8,2) {$ L(a+a) $};
\node (13) at (4,4) {$ La $};
\draw[cd]
(12) edge node[above,left]{$ \nabla $} (13)
(12) edge node[above]{$ \id $} (22)
(12) edge node[below,left]{$ \id $} (11)
(32) edge node[above,right]{$ \nabla $} (13)
(32) edge node[above]{$ \id $} (22)
(32) edge node[below,left]{$ \id $} (11)
(22) edge node[left]{$ \nabla $} (13)
(22) edge node[left]{$ \id $} (11);
\end{tikzpicture}
\]
where the source is the composite 1-arrow
\[
\begin{tikzpicture}
\node (11) at (0,0) {$ L(a+a) $};
\node (21) at (4,0) {$ La $};
\node (31) at (8,0) {$ L(a+a) $};
\node (12) at (2,2) {$ La $};
\node (22) at (6,2) {$ La $};
\node (13) at (4,4) {$ La $};
\draw[cd]
(11) edge node[above,left]{$ \nabla $} (12)
(21) edge node[above,right]{$ \id $} (12)
(21) edge node[above,left]{$ \id $} (22)
(31) edge node[above,right]{$ \nabla $} (22)
(12) edge node[above,left]{$ \id $} (13)
(22) edge node[above,right]{$ \id $} (13);
\draw (3.9,3.5) -- (4,3.4) -- (4.1,3.5);
\end{tikzpicture}
\]
Checking the triangle identities is

The unit of the adjunction $ \epsilon \dashv
\epsilon^\ast $ is the 2-arrow
\[
\begin{tikzpicture}
\node (11) at (4,0) {$ L(a+a) $};
\node (12) at (0,2) {$ La $};
\node (22) at (4,2) {$ L(a+a) $};
\node (32) at (8,2) {$ La $};
\node (13) at (4,4) {$ La $};
\draw[cd]
(12) edge node[above,left]{$ \id $} (13)
(12) edge node[above]{$ \lambda $} (22)
(12) edge node[left]{$ \lambda $} (11)
(32) edge node[right]{$ \id $} (13)
(32) edge node[above]{$ \rho $} (22)
(32) edge node[right]{$ \rho $} (11)
(22) edge node[left]{$ \nabla $} (13)
(22) edge node[left]{$ \id $} (11);
\end{tikzpicture}
\]
where the target is the composite 1-arrow
\[
\begin{tikzpicture}
\node (11) at (0,0) {$ La $};
\node (21) at (4,0) {$ L0 $};
\node (31) at (8,0) {$ La $};
\node (12) at (2,2) {$ La $};
\node (22) at (6,2) {$ La $};
\node (13) at (4,4) {$ L(a+a) $};
\draw[cd]
(11) edge node[above,left]{$ \id $} (12)
(21) edge node[above,right]{$ ! $} (12)
(21) edge node[above,left]{$ ! $} (22)
(31) edge node[above,right]{$ \id $} (22)
(12) edge node[above,left]{$ \lambda $} (13)
(22) edge node[above,right]{$ \rho $} (13);
\draw (3.9,3.5) -- (4,3.4) -- (4.1,3.5);
\end{tikzpicture}
\]
the counit of $ \epsilon \dashv \epsilon^\ast $
is the 2-arrow
\[
\begin{tikzpicture}
\node (11) at (4,0) {$ La $};
\node (12) at (0,2) {$ L0 $};
\node (22) at (4,2) {$ La $};
\node (32) at (8,2) {$ L0 $};
\node (13) at (4,4) {$ La $};
\draw[cd]
(12) edge node[above]{$ ! $} (13)
(12) edge node[above]{$ ! $} (22)
(12) edge node[below]{$ ! $} (11)
(32) edge node[above]{$ ! $} (13)
(32) edge node[above]{$ ! $} (22)
(32) edge node[below]{$ ! $} (11)
(22) edge node[left]{$ \id $} (13)
(22) edge node[left]{$ \id $} (11);
\end{tikzpicture}
\]
where the source is the composite 1-arrow
\[
\begin{tikzpicture}
\node (11) at (0,0) {$ L0 $};
\node (21) at (4,0) {$ La $};
\node (31) at (8,0) {$ L0 $};
\node (12) at (2,2) {$ La $};
\node (22) at (6,2) {$ La $};
\node (13) at (4,4) {$ La $};
\draw[cd]
(11) edge node[above,left]{$ ! $} (12)
(21) edge node[above,right]{$ \id $} (12)
(21) edge node[above,left]{$ \id $} (22)
(31) edge node[above,right]{$ ! $} (22)
(12) edge node[above,left]{$ \id $} (13)
(22) edge node[above,right]{$ \id $} (13);
\draw (3.9,3.5) -- (4,3.4) -- (4.1,3.5);
\end{tikzpicture}
\]
Again, the triangle equations are straightforward to
\end{proof}

The following lemma refers to a `Frobenius monoid', a monoid
and comonoid that satisfy some nice properties that we spell
out in Definition \ref{def:frobenius-monoid}.

\begin{lemma} \label{thm:frobenius}
For any object $ a $ of $ _L \BBoldRewrite $,
$ ( a , \nabla^\ast , \epsilon^\ast , \nabla ,
\epsilon ) $ is a Frobenius monoid. In particular,
\begin{equation} \label{eq:frobenius}
\nabla \nabla^\ast =
\left( \nabla^\ast \otimes \id \right)
\left( \id \otimes \nabla \right)
\end{equation}
\end{lemma}

\begin{proof}
The left-hand side of Equation
\ref{eq:frobenius} is given by the composite
\[
\begin{tikzpicture}
\node (11) at (0,0) {$ L(a+a) $};
\node (21) at (4,0) {$ La $};
\node (31) at (8,0) {$ L(a+a) $};
\node (12) at (2,2) {$ La $};
\node (22) at (6,2) {$ La $};
\node (13) at (4,4) {$ La $};
\draw[cd]
(11) edge node[above]{$ \nabla $} (12)
(21) edge node[above]{$ \id $} (12)
(21) edge node[above]{$ \id $} (22)
(31) edge node[above]{$ \nabla $} (22)
(12) edge node[above]{$ \id $} (13)
(22) edge node[above]{$ \id $} (13);
\draw (3.9,3.5) -- (4,3.4) -- (4.1,3.5);
\end{tikzpicture}
\]
The right-hand side is given by
\[
\begin{tikzpicture}
\node (11) at (0,0) {$ L(a+a) $};
\node (21) at (4,0) {$ L(a+a+a) $};
\node (31) at (8,0) {$ L(a+a) $};
\node (12) at (2,2) {$ L(a+a) $};
\node (22) at (6,2) {$ L(a+a) $};
\node (13) at (4,4) {$ La $};
\draw[cd]
(11) edge node[above]{$ \id $} (12)
(21) edge node[above,right]{$ L(\id +\nabla ) $} (12)
(21) edge node[below,right]{$ L(\nabla + \id) $} (22)
(31) edge node[above]{$ \id $} (22)
(12) edge node[above]{$ L\nabla $} (13)
(22) edge node[above,right]{$ L\nabla $} (13);
\draw (3.9,3.5) -- (4,3.4) -- (4.1,3.5);
\end{tikzpicture}
\]
These both compose to $ L(a+a) \xto{L\nabla} La
\xgets{L\nabla} L(a+a) $.
\end{proof}

The following structure theorem follows from this
string of lemmas.

\begin{theorem} \label{thm:bold-rewrite-bicat-rels}
$ _L \BBoldRewrite $ is a bicategory of relations.
\end{theorem}

% ===================================================
\section{The ZX-calculus}
\label{sec:zx-calculus}
% ===================================================

Perhaps one of the most interesting features of quantum
mechanics is the incompatibility of observables.  Roughly,
an observable is a measurable quantity of some system, for
instance the spin of a photon.  In classical physics,
measureable quantities are comparable, meaning that we can
obtain arbitrarily precise values at the same time.  For
example, given a Porsche speeding down the highway, we can
simultaneously measure its velocity and its mass with
arbitrary precision.  Knowledge about its velocity does not
preclude us from obtain information about its mass. The
situation is quite different in quantum mechanics. Given two
measurable quantities, knowledge of one may prevent us from
obtaining knowledge about the other. This is illustrated by
the famous Heisenberg uncertainty principle which quantifies
the limits of precision to which one can simultaneously
measure the position and momentum of a particle. In general,
the strength of this restriction depends on the
situation. The most extreme case is that knowing one
quantity with total precision implies total uncertainty
about the other quantity. Such a pair of observables are
called \defn{complementary}.

Historically, a quantum physicist would reason about
observables, complementary or otherwise, using Hilbert
spaces. Given the rapid progress of quantum physics in the
twentieth century, this framework seems to have worked quite
well for scientists. Working with Hilbert spaces, however,
is challenging even for skilled researchers. But the
language of quantum physics is now relevant to a wider
audience since the dawn of quantum computing. Given the
challenge of working with Hilbert spaces, perhaps developing
a simpler language is worth pursuing.

Such a high-level language was invented by Coecke and Duncan
[24].  This language, called the
ZX-calculus, was immediately used to generalize both quantum
circuits [51] and the measurement
calculus [26].  Its
validity was further justified when Duncan and Perdrix
presented a non-trivial method of verifying
measurement-based quantum computations
[31].  At its core, the
ZX-calculus is an intuitive graphical language in which to
reason about complementary observables.

In this section, we illustrate our framework with the
ZX-calculus.  The backstory of the ZX-calculus dates to
Penrose's tensor networks [54] and, more recently,
to the relationship between graphical languages and monoidal
categories [39, 57]. Abramsky and Coecke
capitalized on this relationship when inventing a
categorical framework for quantum physics
[1].  Soon after, Coecke and Duncan
introduced a diagrammatic language in which to reason about
complementary quantum observables
[19].  After a fruitful period
of development [20, 23, 30, 31, 29, 53], a full presentation of the
ZX-calculus was published [24].
The completeness of the ZX-calculus for stabilizer quantum
mechanics was later proved by Backens

The ZX-calculus begins with the five diagrams depicted in
Figure \ref{fig:zx-generators}. On each diagram, the
dangling wires on the left are \defn{inputs} and those on
the right are \defn{outputs}.  By connecting inputs to
outputs, we can form larger diagrams, which we call
\defn{ZX-diagrams}.  These diagrams generate the arrows of a
dagger compact category $\ZX$ whose objects, the
non-negative integers, count the inputs and outputs of a
diagram.  Below, we give a presentation of $\ZX$ along with
a brief discussion on the origins of its generating arrows
(Figure \ref{fig:zx-generators}) and relations (Figure
\ref{fig:zx-equations}).

\begin{figure}
\fbox{%
\centering
\begin{minipage}{1\textwidth}
% ~~~~~~~~~~~~~
\begin{minipage}{0.2\linewidth}
\centering
\includegraphics{InclGrphx--generater--wire} \\
\vspace{0.5em}
\textsc{Wire}
\end{minipage}
\begin{minipage}{0.2\linewidth}
\centering
\includegraphics{InclGrphx--generater--green_spider} \\
\vspace{0em}
\textsc{Green Spider}
\end{minipage}%
\begin{minipage}{0.2\linewidth}
\centering
\includegraphics{InclGrphx--generater--red_spider} \\
\vspace{0em}
\textsc{Red Spider}
\end{minipage}%
\begin{minipage}{0.2\linewidth}
\centering
\includegraphics{InclGrphx--generater--hadamard} \\
\vspace{0.5em}
\textsc{Hadamard}
\end{minipage}%
\begin{minipage}{0.2\linewidth}
\centering
\includegraphics{InclGrphx--generater--diamond} \\
\vspace{0.5em}
\textsc{Diamond}
\end{minipage}%
\end{minipage}
\caption{Generators for the ZX-calculus diagrams}
\label{fig:zx-generators}
\end{figure}

Our goal with this example is to generate, using the
machinery laid out in this chapter, a bicategory of
relations $\ZZX$ to provide a syntax for the ZX-calculus. We
show that $ \ZZX $ extends $ \ZX $ in a way we make precise below.

The five \defn{basic diagrams} in the ZX-calculus
are depicted in Figure \ref{fig:zx-generators} and
are to be read from left to right. They are
\begin{itemize}
\item a \defn{wire} with a single input and
\item \defn{green spiders} with a non-negative
integer number of inputs and outputs and paired
with a phase $\alpha \in [-\pi,\pi)$,
\item \defn{red spiders} with a non-negative
integer number inputs and outputs and paired
with a phase $\beta \in [-\pi,\pi)$,
\item the \defn{Hadamard node} with a single input
and output, and
\item a \defn{diamond node} with no inputs or
\end{itemize}
The wire plays the role of an identity, much like a wire
without resistance in an electrical circuit, or straight
pipe in a plumbing system.  The green and red spiders each
arise from a pair of complementary observables.  In
categorical quantum mechanics [1],
observables correspond to certain commutative Frobenius
algebras $A$ living in a dagger symmetric monoidal category
$(\C , \otimes , I)$, the classic example
$ \C \bydef \FinHilb $ being the category of finite
dimensional Hilbert spaces and linear maps.  A pair of
complementary observables gives a pair of Frobenius
algebras whose operations interact via laws like those of a
Hopf algebra
[21, 22].
This is particularly nice because Frobenius algebras have
beautiful string diagram representations.  There is an
morphism $\C(I,A) \to \C(A,A)$ of commutative monoids that
gives rise to a group structure on $A$ known as the
\defn{phase group}, which Coecke and Duncan detail
\cite[Def.~7.5]{coecke-duncan_quant-full}.  The phases on
the green and red spider diagrams arise from this group.
The Hadamard node embodies the Hadamard gate.  The diamond
is a scalar obtained when connecting a green and red node
together.  A deeper exploration of these notions goes beyond
the scope of this paper.  For those interested, the original
paper on the topic
[24]
is an excellent place learn more.

In the spirit of compositionality, we present a category
$ \ZX $ whose arrows are generated by the five
basic diagrams. We sketched $ \ZX $ at the beginning of this
section, but we now detail the construction.

We start by allowing the basic ZX-diagrams from Figure
\ref{fig:zx-generators} generate the arrows of a free dagger
compact category whose objects are the non-negative
integers. We then subject the arrows (ZX-diagrams) to the
relations given in Figure \ref{fig:zx-equations}, to which
we add equations obtained by exchanging red and green nodes,
daggering, and taking diagrams up to ambient isotopy in
$4$-space.  These listed relations are called \defn{basic}.
Spiders with no phase indicated have a phase of $0$.

This category, denoted as $ \ZX $, was introduced by Coecke
and Duncan
[24]
and further studied by Backens
To compose in $\ZX$, connect compatible diagrams
along a bijection between inputs and the outputs. For
\begin{center}
\begin{tikzpicture}
\node            (1) at (0,2) {$  $};
\node            (2) at (0,0) {$  $};
\node [zxgreen]  (3) at (2,1) {$  $};
\node            (4) at (4,1) {$  $};
\node            ( ) at (5,1) {$ \circ $};
\node            (5) at (6,1) {$  $};
\node [zxyellow] (6) at (8,1) {$  $};
\node            (7) at (10,1) {$  $};
\node            ( ) at (11,1) {$ = $};
\draw
(1.60) --(3.120)
(2.-60) -- (3.-120)
(3) -- (4)
(5) -- (6)
(6) -- (7);
\end{tikzpicture}
\end{center}
\begin{center}
\begin{tikzpicture}
\node            (1) at (0,2) {$  $};
\node            (2) at (0,0) {$  $};
\node [zxgreen]  (3) at (2,1) {$  $};
\node            (4) at (4,1) {$  $};
\node [zxyellow] (5) at (6,1) {$  $};
\node            (6) at (8,1) {$  $};
\draw
(1.60) -- (3.120)
(2.-60) -- (3.-120)
(3) -- (4.center)
(4.center) -- (5)
(5) -- (6);
\end{tikzpicture}
\end{center}
A monoidal structure is given by adding numbers and taking
the disjoint union of ZX-diagrams.  The identity on $n$ is
the disjoint union of $n$ wires:
\begin{center}
\begin{tikzpicture}
\node (1) at (0,0) {$  $};
\node (2) at (0,0.25) {$  $};
\node ( ) at (1.5,0.6) {$ \vdots $};
\node (3) at (0,0.75) {$  $};
\node (1') at (3,0) {$  $};
\node (2') at (3,0.25) {$  $};
\node (3') at (3,0.75) {$  $};
\draw
(1) -- (1')
(2) -- (2')
(3) -- (3');
\end{tikzpicture}
\end{center}
The symmetry and compactness of the monoidal product provide
a braiding, evaluation, and coevaluation morphisms:
\[
\includegraphics{InclGrphx--morphism--zx_braiding}
\quad \quad \quad \quad
\raisebox{-0.25\height}{%
\includegraphics[scale=0.75]{InclGrphx--morphism--zx_evaluation}
\quad \quad \quad \quad
\raisebox{-0.25\height}{%
\includegraphics[scale=0.75]{InclGrphx--morphism--zx_coevaluation}
\]
The evaluation and coevalutation arrows are of type
$2n \to 0$ and $0 \to 2n$ for each object
$n \geq 1$ and the empty diagram for $n=0$.  On
the spider diagrams, the dagger structure swaps
inputs and outputs then multiplies the phase by
\[
\includegraphics{InclGrphx--functor--dagger}
\]
The dagger acts trivially on the wire, Hadamard,
and diamond elements.

\begin{figure}
\fbox{
\begin{minipage}{\textwidth}
\centering
\begin{minipage}{0.5\linewidth}
\centering
\includegraphics{InclGrphx--equation--spider} \\
\textsc{Spider}
\end{minipage}%
\begin{minipage}{0.5\linewidth}
\centering
\includegraphics{InclGrphx--equation--bialgebra} \\
\textsc{Bialgebra}
\end{minipage}
\vspace{1em}
\linebreak
\begin{minipage}{0.3\linewidth}
\centering
\includegraphics{InclGrphx--equation--copy} \\
\textsc{Copy}
\end{minipage}%
\begin{minipage}{0.3\linewidth}
\centering
\includegraphics{InclGrphx--equation--pi_copy} \\
\textsc{$ \pi $-Copy}
\end{minipage}%
\begin{minipage}{0.3\linewidth}
\centering
\includegraphics{InclGrphx--equation--cup} \\
\textsc{Cup}
\end{minipage}
\vspace{1em}
\linebreak
\begin{minipage}{0.5\linewidth}
\centering
\includegraphics{InclGrphx--equation--trivial_spider} \\
\textsc{Trivial Spider}
\end{minipage}%
\begin{minipage}{0.5\linewidth}
\centering
\includegraphics{InclGrphx--equation--pi_commutation} \\
\textsc{$\pi$-Commutation}
\end{minipage}%
\linebreak
\begin{minipage}{0.3\linewidth}
\centering
\includegraphics{InclGrphx--equation--color_change} \\
\textsc{Color Change}
\end{minipage}%
\begin{minipage}{0.3\linewidth}
\centering
\includegraphics{InclGrphx--equation--loop} \\
\textsc{Loop}
\end{minipage}%
\begin{minipage}{0.3\linewidth}
\centering
\includegraphics{InclGrphx--equation--diamond} \\
\textsc{Diamond}
\end{minipage}%
\end{minipage}
\caption{Relations in the category $\ZX$}
\label{fig:zx-equations}
\end{figure}

A major advantage of using string diagrams, apart
from their intuitive nature, is that computations
are more easily programmed into computers.
Indeed, graphical proof assistants like
[10, 28]
and Globular
[10]
were made for such graphical reasoning.  The logic
of these programs are encapsulated by double
pushout rewrite rules.  However, the algebraic
structure of $\ZX $ and other graphical calculi do
not contain the rewrite rules as explicit
elements. On the other hand, the framework developed in this thesis
explicitly includes the rewrite rules.

To model the ZX-calculus using structured cospans, we need
an appropriate adjunction $ L \from \A \lrto \X \from R $.
Determining the correct pieces to fill in requires some
discussion. Before providing the details, we sketch the
process.  Let $ \A \bydef \FinSet $ be the topos of finite
sets and functions. Let $ \X \bydef \FinGraphGamma $ be the
over-category where we chose a graph $ \Gamma $ to provide
the objects of $ \X \bydef \FinGraph / \Gamma $ with the
same type information as the ZX-diagrams. The functor $ L $
turns a finite set $ a $ into a certain discrete graph over
$ \Gamma $ so that $ La $ can serve as inputs or outputs. To
unpack what this all means, we start with the over-category.

\begin{definition}
Let $g$ be a graph.  By a \defn{graph over $g$},
we mean a graph morphism $x \to g$. A morphism
between graphs over $g$ is a graph morphism
$x \to y$ such that
\[
\begin{tikzpicture}
\node (1) at (-1,2) {$x$};
\node (2) at (1,2) {$y$};
\node (3) at (0,0) {$g$};
\draw[cd]
(1) edge (2)
(1) edge (3)
(2) edge (3);
\end{tikzpicture}
\]
\end{definition}

One way to think of a graph over $ g $ is as
a $ g $-typed graph. Consider the following simple

\begin{example}
\label{ex:graph-over-g}
Let $ g $ be the graph
\[
\begin{tikzpicture}
\node (a) at (0,0) {$ A $};
\node (b) at (3,0) {$ B  $};
\draw[graph]
(a) edge[bend left] node[above]{$F$} (b)
(b) edge[bend left] node[below]{$G$} (a);
\end{tikzpicture}
\]
Let $ x $ be the graph
\[
\begin{tikzpicture}
\node (a) at (0,0)  {$ a $};
\node (b) at (4,0)  {$ b $};
\node (c) at (2,2)  {$ c $};
\node (d) at (2,-2) {$ d $};
\draw[graph]
(a) edge node[above,left]{$ e $} (c)
(a) edge node[below,left]{$ f $} (d)
(c) edge node[above,right]{$ g $} (b)
(d) edge node[below,right]{$ h $} (b);
\end{tikzpicture}
\]
that lies over $ g $ via the map
\begin{align*}
a,b & \mapsto A  &    e,f & \mapsto F \\
c,d & \mapsto B  &    g,h & \mapsto G
\end{align*}
If we think of the nodes and edges of $ g $ as
types, then these types are transported to $ x $
along the fibers of this map.  Thus $ x $ is a
graph with the following type-assignment:
\begin{center}
\begin{tabular}{ccccc}
$ a : A $ && $ b : A $ && $ c : B $ \\
$ d : B $ && $ e : F $ && $ f : F $ \\
$ g : G $ && $ h : G $ &&           \\
\end{tabular}
\end{center}
where `$ : $' should be read `is type'.  Any graph over
$ g $ can have two node types $ A,B $ and two edge types
$ F,G $.  Edges can only go from an $ A $-type
node to a $ B $-type node or vice versa.  Edges cannot
traverse nodes of the same type simply because there are
no looped edges in $ g $.

A compact way to draw a graph over $ g $ is to
label its nodes and edges with their types.
Thus, the over-graph $ x \to g $ can be drawn as
\[
\begin{tikzpicture}
\node (a) at (0,0)  {$ (a,A) $};
\node (b) at (4,0)  {$ (b,A) $};
\node (c) at (2,2)  {$ (c,B) $};
\node (d) at (2,-2) {$ (d,B) $};
\draw[graph]
(a) edge node[above,left]{$ (e,F) $} (c)
(a) edge node[below,left]{$ (f,F) $} (d)
(c) edge node[above,right]{$ (g,G) $} (b)
(d) edge node[below,right]{$ (h,G) $} (b);
\end{tikzpicture}
\]

One might recognize the class of graphs over $ g $ as
something like a bipartite graph.  The difference between
graphs over $ g $ and bipartite graphs is that bipartite
graphs are usually defined by graph theorists to satisfy
\emph{the property} that the nodes can be partitioned into
two classes and the source and target of each edge must
belong to different classes.  On the other hand, graphs
over $ g $ are graphs equipped with extra structure,
namely the type information. This distinction does not
appear in the graphs themselves, so we look at their

A morphism of graphs over $ g $ must respect the type
information. So if $ x \to g $ and $ y \to g $ are graphs
over $ g $, then a morphism between them is a graph
morphism $ x \to y $ such that the diagram
\[
\begin{tikzpicture}
\node (x) at (0,0) {$ x $};
\node (y) at (4,0) {$ y $};
\node (g) at (2,-2) {$ g $};
\draw [cd]
(x) edge (y)
(x) edge (g)
(y) edge (g);
\end{tikzpicture}
\]
commutes. Suppose that $ x $ is a single node typed $ A $
and $ y $ is a single node typed $ B $. There is no
morphism between them because the node in $ x $ must be
sent to a node of type $ A $.  However, any two bipartite
graphs with a single node and no edges are isomorphic. The
moral of this example is by adding the type information, we
added structure instead of imposing a property.  We denote by
$ \Graph \downarrow g $ the category of graphs over $ g $
and their morphisms.
\end{example}

We exploit this method of defining
`typed graphs' to transform typical combinatorial
graphs into ZX-diagrams. The types needed to make
ZX-diagrams from graphs encoded into the graph $ \Gamma $
that we define now.

\begin{definition}
\label{ex:basic-graph-over-g}
Let $ \Gamma $ be the graph
\begin{equation}
\label{eq:gamma}
\begin{tikzpicture}
\node [zxwhite]  (w) at (0,0)    {$ $};
\node [zxgreen]  (g) at (-1,1)   {};
\node            ()  at (-1.33,1) {\scriptsize{$\alpha$}};
\node [zxred]    (r) at (1,1)    {};
\node            ()  at (1.33,1)  {\scriptsize{$\beta$}};
\node [zxblack]  (b) at (-1,-1)  {$$};
\node [zxyellow] (y) at (1,-1)   {$$};
\path[graph]
(w) edge [loop below]   (w)
(w) edge [bend left=10] (g)
(w) edge [bend left=10] (r)
(w) edge [bend left=10] (b)
(w) edge [bend left=10] (y)
(g) edge [bend left=10] (w)
(r) edge [bend left=10] (w)
(b) edge [bend left=10] (w)
(y) edge [bend left=10] (w);
\node () at (3,0) {$ \alpha,\beta \in [ -\pi , \pi ) $};
\end{tikzpicture}.
\end{equation}

We have not drawn the entirety of $ \Gamma $. In
actuality, the green and red nodes run through
$ [ -\pi , \pi ) $ and each of them have a single
arrow to and from the white node
\end{definition}

Note that the graphs over $ \Gamma $ are completely
determined by the function's behavior on the nodes.  This is
because there is at most one arrow between any two
nodes. When comparing the $ \Gamma $-types to the types
appearing in the basic ZX-diagrams of Figure
\ref{fig:zx-generators}, there is a clear correlation
except, perhaps, for the white node.  To explain the white
node, first observe that ZX-diagrams have dangling wires on
either end. Dangling edges are not permitted in our
definition of graphs, so the white node anchors them.

To draw graphs over $ \Gamma $, we attach the type
information to the nodes by rendering the nodes as
red, greed, white, black, or yellow.  This manner
of drawing is more economical than drawing a graph
and describing its map to $ \Gamma $.  For
example, consider the graph
\[
\begin{tikzpicture}
\node (0) at (0,0) {$ \bullet_a $};
\node (1) at (2,0) {$ \bullet_b $};
\node (2) at (4,0) {$ \bullet_c  $};
\draw[graph]
(0) edge (1)
(1) edge (2);
\end{tikzpicture}
\]
with the map to $ \Gamma $ determined by
\[
\begin{tikzpicture}
\node           at (0,1) {$ a,c \mapsto $};
\node [zxwhite] at (1,1) {$  $};
\node           at (0,0) {$ b \mapsto $};
\node [zxgreen] at (1,0) {$ \beta $};
\end{tikzpicture}
\]
We draw this as
\[
\begin{tikzpicture}
\node [zxwhite] (1) at (0,0) {$  $};
\node [zxgreen] (2) at (2,0) {$ \beta $};
\node [zxwhite] (3) at (4,0) {$  $};
\draw[graph]
(1) edge (2)
(2) edge (3);
\end{tikzpicture}
\]

In our adjunction $ L \from \A \lrto \X \from R $, we let
$ \X $ be $ \FinGraphGamma $. This is a topos by the
fundamental theorem of topos theory, which we present in
Theorem \ref{thm:fund-thm-topos}.

The most important objects in $ \FinGraphGamma $ are those
corresponding to the basic ZX-diagrams. These are displaying
in Figure \ref{fig:basic-diagrams-over-gamma}. To choose a
category $ \A $ of interface types, we want to faithfully
represent the fact that ZX-diagrams have a non-negative
integer number of inputs and outputs. Therefore, we let
$ \A $ be the topos $\FinSet $ of finite sets and functions.

\begin{figure}
\fbox{
\begin{minipage}{\textwidth}
\centering
\begin{minipage}{0.3\linewidth}
\centering
\[
\begin{tikzpicture}
\node [zxwhite] (a) at (0,0) {};
\node [zxwhite] (b) at (2,0) {};
\draw [graph]
(a) to (b);
\end{tikzpicture}
\]
\textsc{Wire}
\end{minipage}%
\begin{minipage}{0.3\linewidth}
\centering
\[
\begin{tikzpicture}
\node [zxwhite] (a) at (0,0)   {$ $};
\node           ( ) at (0,0.66) {$ \vdots $};
\node [zxwhite] (b) at (0,1)   {$  $};
\node [zxgreen] (c) at (1,0.5) {$ $};
\node           ( ) at (1,1.25) {$\alpha$};
\node [zxwhite] (d) at (2,0)   {$ $};
\node           ( ) at (2,0.66) {$ \vdots $};
\node [zxwhite] (e) at (2,1)   {$  $};
\draw[graph]
(a) edge [bend right=10]  (c)
(b) edge [bend left=10]   (c)
(c) edge [bend right=10]  (d)
(c) edge [bend left=10]   (e);
\end{tikzpicture}
\]
\textsc{Green Spider}
\end{minipage}
\begin{minipage}{0.3\linewidth}
\centering
\[
\begin{tikzpicture}
\node [zxwhite] (a) at (0,0)   {$ $};
\node           ( ) at (0,0.66) {$ \vdots $};
\node [zxwhite] (b) at (0,1)   {$  $};
\node [zxred] (c) at (1,0.5) {$ $};
\node           ( ) at (1,1.25) {$\alpha$};
\node [zxwhite] (d) at (2,0)   {$ $};
\node           ( ) at (2,0.66) {$ \vdots $};
\node [zxwhite] (e) at (2,1)   {$  $};
\draw[graph]
(a) edge [bend right=10]  (c)
(b) edge [bend left=10]   (c)
(c) edge [bend right=10]  (d)
(c) edge [bend left=10]   (e);
\end{tikzpicture}
\]
\textsc{Red Spider}
\end{minipage}
\vspace{1em}
\linebreak
\begin{minipage}{0.5\linewidth}
\centering
\[
\begin{tikzpicture}
\node [zxwhite]  (a) at (0,0) {$$};
\node [zxyellow] (b) at (1,0) {$$};
\node [zxwhite]  (c) at (2,0) {$$};
\draw[graph]
(a) edge (b)
(b) edge (c);
\end{tikzpicture}
\]
\textsc{Hadamard}
\end{minipage}%
\begin{minipage}{0.5\linewidth}
\centering
\[
\begin{tikzpicture}
\node [zxblack] () at (0,0) {$$};
\end{tikzpicture}
\]
\textsc{Diamond}
\end{minipage}%
\end{minipage}
\caption{Basic ZX-diagrams as graphs over $ \Gamma $}
\label{fig:basic-diagrams-over-gamma}
\end{figure}

We still need to define $ L $ and $ R $ in the adjunction
\[
\adjunction{\FinSet}{\FinGraphGamma}{L}{R}{4}
\]
\[
L \from \FinSet \to \FinGraphGamma
\]
by letting $ La $ be the edgeless graph with node
set $ a $ that is constant over the whites
node in $ \Gamma $. A function $ f \from a \to b $ of finite
sets becomes of morphism $ Lf $ of graphs over $
\Gamma $ that simply reinterprets the action of $
f $ on elements of a set to white nodes in a
graph.  Define
\[
R \from \FinGraphGamma \to \FinSet
\]
by defining $ R ( x \to \Gamma ) $ as the fiber in
$ x $ of the white node. Given a morphism of
graphs over $ \Gamma $, $ R $ restricts it to the
function on only the white nodes.

\begin{lemma}
The functor pair
\[
\adjunction{\FinSet}{\FinGraphGamma}{L}{R}{4}
\]
forms an adjunction and $ L $ preserves pullbacks.
\end{lemma}

\begin{proof}
Observe that the composite $ RL $ is the
identity functor. So the unit
$ \eta \from a \to RLa $ is the identity which
is natural in $ a $. The
counit $ \epsilon \from LRx \to x $ is the
inclusion of the white nodes of $ x $ into
$ x $. Given an arrow $ f \from x \to y $ in $
\FinGraphGamma $, the diagram
\[
\begin{tikzpicture}
\node (LRx) at (0,2) {$ LRx $};
\node (x) at (2,2) {$ x $};
\node (LRy) at (0,0) {$ LRy $};
\node (y) at (2,0) {$ y $};
\draw[cd]
(LRx) edge node[above]{$ \epsilon_x $} (x)
(LRy) edge node[below]{$ \epsilon_y $} (y)
(LRx) edge node[left]{$ LRf $}         (LRy)
(x)   edge node[right]{$ f $}          (y);
\end{tikzpicture}
\]
commutes since $ LRf $ is a restriction of $ f $. To show
that $ L $ preserves pullbacks, take a cospan
\[ a \to b \gets c \] in $ \Set $ with pullback
$ a \times_b c $ and apply $ L $ to get the diagram
\[
\begin{tikzpicture}
\node (La) at (-2,0) {$ La $};
\node (Lb) at (0,0) {$ Lb $};
\node (Lc) at (0,2) {$ Lc $};
\node (Gamma) at (2,-2) {$ \Gamma $};
\path [cd]
(La) edge (Lb)
(Lc) edge (Lb)
(La.-90) edge[bend right] (Gamma.180)
(Lb) edge (Gamma)
(Lc.0) edge[bend left] (Gamma.90);
\end{tikzpicture}
\]
comprised of edgeless graphs $ La $, $ Lb $, and $ Lc $
that are constant over the white node in $ \Gamma $.  The
pullback of this diagram is
$ La \times_{Lb} Lc \to \Gamma $ which is constant over
the white node. This is isomorphic to $ L(a \times_b c)
\to \Gamma $ which is constant over the white node.
\end{proof}

With our adjunction established, we can define structured
cospans of graphs over $ \Gamma $ and therefore also the
symmetric monoidal double category of bold rewrites
$ _L \BBBoldRewrite $ for the functor
$ L \from \FinSet \to \FinGraphGamma $ defined above.  This
double category has as objects the finite sets, as
horizontal 1-arrows the structured cospans of graphs over
$ \Gamma $, as vertical 1-arrows the spans of finite sets
with invertible legs, and as squares all possible
bold rewrites of structured cospans.  Clearly,
$ _L \BBBoldRewrite $ is far bigger than the ZX-calculus
because it contains graphs over $ \Gamma $ with no
corresponding ZX-diagram. This does not mean, however, that
$ _L \BBBoldRewrite $ serves no purpose.  It plays the role
of an ambient space in which we chisel out a sub-double
category that \emph{does} correspond to the ZX-calculus.

To begin the process of constructing this sub-double
category of $ _L \BBBoldRewrite $, we identify structured
cospans to capture the basic ZX-diagrams and identify bold
rewrites of structured cospans for the basic
ZX-relations. We also include some additional structured
cospans to give the desired structure.  Figure
\ref{fig:basic-diagrams-as-str-csps}
depicts the basic ZX-diagrams as structured

\begin{figure}
\fbox{
\scalebox{0.9}{
\begin{minipage}{\textwidth}
\centering
\begin{minipage}{\textwidth}
\centering
\[
\begin{tikzpicture}
\begin{scope}
\node [zxwhite] (a) at (0,0) {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,0.5);
\node (l) at (0.6,0) {};
\end{scope}
\begin{scope}[shift={(2,0)}]
\node [zxwhite] (a) at (0,0) {};
\node [zxwhite] (b) at (2,0) {};
\draw [graph]
(a) to (b);
\draw [rounded corners]
(-0.5,-0.5) rectangle (2.5,0.5);
\node (cr) at (2.6,0) {};
\node (cl) at (-0.6,0) {};
\node () at (1,-1) {\textsc{Wire}};
\end{scope}
\begin{scope}[shift={(6,0)}]
\node [zxwhite] (a) at (0,0) {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,0.5);
\node (r) at (-0.6,0) {};
\end{scope}
\draw[cd]
(l) edge (cl)
(r) edge (cr);
\end{tikzpicture}
\]
\end{minipage}%
\vspace{1em}
\linebreak
% ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
\begin{minipage}{0.40\linewidth}
\[
\begin{tikzpicture}
\begin{scope}
\node [zxwhite] (a) at (0,0)    {};
\node           ( ) at (0,0.66) {$ \vdots $};
\node [zxwhite] (b) at (0,1)    {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\node (l) at (0.6,0.5) {};
\end{scope}
\begin{scope}[shift={(2,0)}]
\node [zxwhite] (a) at (0,0)   {$ $};
\node           ( ) at (0,0.66) {$ \vdots $};
\node [zxwhite] (b) at (0,1)   {$  $};
\node [zxgreen] (c) at (1,0.5) {$ $};
\node           ( ) at (1,1) {$\alpha$};
\node [zxwhite] (d) at (2,0)   {$ $};
\node           ( ) at (2,0.66) {$ \vdots $};
\node [zxwhite] (e) at (2,1)   {$  $};
\draw[graph]
(a) edge[bend right=10] (c)
(b) edge[bend left=10]  (c)
(c) edge[bend right=10] (d)
(c) edge[bend left=10]  (e);
\draw [rounded corners]
(-0.5,-0.5) rectangle (2.5,1.5);
\node (cl) at (-0.6,0.5) {};
\node (cr) at (2.6,0.5)  {};
\node () at (1,-1) {\textsc{Green Spider}};
\end{scope}
\begin{scope}[shift={(6,0)}]
\node [zxwhite] (a) at (0,0)    {};
\node           ( ) at (0,0.66) {$ \vdots $};
\node [zxwhite] (b) at (0,1)    {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\node (r) at (-0.6,0.5) {};
\end{scope}
\path[cd]
(l) edge (cl)
(r) edge (cr);
\end{tikzpicture}
\]
\end{minipage}
\hspace{3em}
\begin{minipage}{0.45\linewidth}
\[
\begin{tikzpicture}
\begin{scope}
\node [zxwhite] (a) at (0,0)    {};
\node           ( ) at (0,0.66) {$ \vdots $};
\node [zxwhite] (b) at (0,1)    {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\node (l) at (0.6,0.5) {};
\end{scope}
\begin{scope}[shift={(2,0)}]
\node [zxwhite] (a) at (0,0)   {$ $};
\node           ( ) at (0,0.66) {$ \vdots $};
\node [zxwhite] (b) at (0,1)   {$  $};
\node [zxred] (c) at (1,0.5) {$ $};
\node           ( ) at (1,1) {$\alpha$};
\node [zxwhite] (d) at (2,0)   {$ $};
\node           ( ) at (2,0.66) {$ \vdots $};
\node [zxwhite] (e) at (2,1)   {$  $};
\draw[graph]
(a) edge[bend right=10] (c)
(b) edge[bend left=10]  (c)
(c) edge[bend right=10] (d)
(c) edge[bend left=10]  (e);
\draw [rounded corners]
(-0.5,-0.5) rectangle (2.5,1.5);
\node (cl) at (-0.6,0.5) {};
\node (cr) at (2.6,0.5)  {};
\node () at (1,-1) {\textsc{Red Spider}};
\end{scope}
\begin{scope}[shift={(6,0)}]
\node [zxwhite] (a) at (0,0)    {};
\node           ( ) at (0,0.66) {$ \vdots $};
\node [zxwhite] (b) at (0,1)    {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\node (r) at (-0.6,0.5) {};
\end{scope}
\path[cd]
(l) edge (cl)
(r) edge (cr);
\end{tikzpicture}
\]
\end{minipage}
\vspace{1em}
\linebreak
% ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
\begin{minipage}{0.5\linewidth}
\centering
\[
\begin{tikzpicture}
\begin{scope}
\node [zxwhite] (a) at (0,0) {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,0.5);
\node (l) at (0.6,0) {};
\end{scope}
\begin{scope}[shift={(2,0)}]
\node [zxwhite]  (a) at (0,0) {$$};
\node [zxyellow] (b) at (1,0) {$$};
\node [zxwhite]  (c) at (2,0) {$$};
\draw [graph]
(a) edge (b)
(b) edge (c);
\draw [rounded corners]
(-0.5,-0.5) rectangle (2.5,0.5);
\node (cl) at (-0.6,0) {};
\node (cr) at (2.6,0)  {};
\node () at (1,-1) {\textsc{Hadamard}};
\end{scope}
\begin{scope}[shift={(6,0)}]
\node [zxwhite] (a) at (0,0) {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,0.5);
\node (r) at (-0.6,0) {};
\end{scope}
\path[cd]
(l) edge (cl)
(r) edge (cr);
\end{tikzpicture}
\]
\end{minipage}%
\begin{minipage}{0.5\linewidth}
\centering
\[
\begin{tikzpicture}
\begin{scope}[shift={(0,0)}]
\node () at (0,0) {$ \emptyset $};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,0.5);
\node (l) at (0.6,0) {};
\end{scope}
\begin{scope}[shift={(2,0)}]
\node [zxblack] () at (0,0) {$$};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,0.5);
\node (cl) at (-0.6,0) {};
\node (cr) at (0.6,0) {};
\node () at (0,-1) {\textsc{Diamond}};
\end{scope}
\begin{scope}[shift={(4,0)}]
\node (a) at (0,0) {$ \emptyset $};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,0.5);
\node (r) at (-0.6,0) {};
\end{scope}
\draw[cd]
(l) edge (cl)
(r) edge (cr);
\end{tikzpicture}
\]
\end{minipage}
\vspace{1em}
\linebreak
% ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
\begin{minipage}{0.45\linewidth}
\centering
\[
\begin{tikzpicture} % CUP
\begin{scope} % LEFT
\node [zxwhite] (b) at (0,1)    {$  $};
\node           ( ) at (0,0.5) {$\vdots$};
\node [zxwhite] (d) at (0,0)    {$  $};
\node (0r) at (0.6,0.5) {$  $};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\end{scope}
% ~~~~
\begin{scope}[shift={(2,0)}] % MID
\node [zxwhite] (a) at (0,1)   {$  $};
\node           ( ) at (0,0.5) {$\vdots$};
\node [zxwhite] (b) at (0,0)   {$  $};
\node [zxwhite] (c) at (1,0.5) {$  $};
\draw [graph]
(a) edge[bend left=10]  (c)
(b) edge[bend right=10] (c);
\node (1l) at (-0.6,0.5) {$  $};
\node (1r) at (1.6,0.5)  {$  $};
\node () at (0,-1) {\textsc{Cup}};
\draw [rounded corners]
(-0.5,-0.5) rectangle (1.5,1.5);
\end{scope}
% ~~~
\begin{scope}[shift={(5,0)}] % RIGHT
\node (a) at (0,0.5) {$ \emptyset $};
\node (2l) at (-0.6,0.5) {$  $};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\end{scope}
% ~~~~~~~~ ARROWS
\draw[cd]
(0r) edge (1l)
(2l) edge (1r);
\end{tikzpicture}
\]
\end{minipage}
\begin{minipage}{0.45\linewidth} % CAP
\centering
\[
\begin{tikzpicture}
\begin{scope} % LEFT
\node (a) at (0,0.5) {$ \emptyset $};
\node (0r) at (0.6,0.5) {$  $};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\end{scope}
% ~~~~
\begin{scope}[shift={(2,0)}] % MID
\node [zxwhite] (a) at (1,1)   {$  $};
\node           ( ) at (1,0.5) {$\vdots$};
\node [zxwhite] (b) at (1,0)   {$  $};
\node [zxwhite] (c) at (0,0.5) {$  $};
\draw [graph]
(c) edge [bend left=10]  (a)
(c) edge [bend right=10] (b);
\node (1l) at (-0.6,0.5) {$  $};
\node (1r) at (1.6,0.5)  {$  $};
\node () at (0,-1) {\textsc{Cap}};
\draw [rounded corners]
(-0.5,-0.5) rectangle (1.5,1.5);
\end{scope}
% ~~~~~~~~
\begin{scope}[shift={(5,0)}] % RIGHT
\node [zxwhite] (b) at (0,1)    {$  $};
\node           ( ) at (0,0.5) {$\vdots$};
\node [zxwhite] (d) at (0,0)    {$  $};
\node (2l) at (-0.6,0.5) {$  $};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\end{scope}
% ~~~~~~~~
\path[cd]
(0r) edge (1l)
(2l) edge (1r);
\end{tikzpicture}
\]
\end{minipage}
\linebreak
\vspace{1em}
% ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
\begin{minipage}{0.45\linewidth}
\centering
\[
\begin{tikzpicture} % MULTIPLICATION
\begin{scope} % LEFT
\node [zxwhite] () at (0,1) {$ $};
\node [zxwhite] () at (0,0) {$ $};
\node (0r) at (0.6,0.5) {$  $};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\end{scope}
% ~~~~
\begin{scope}[shift={(2,0)}] % MID
\node [zxwhite] (b) at (0.5,0.5) {$  $};
\node (1l) at (-0.6,0.5) {$  $};
\node (1r) at (1.6,0.5)  {$  $};
\node () at (0,-1) {\textsc{Multiplication}};
\draw [rounded corners]
(-0.5,-0.5) rectangle (1.5,1.5);
\end{scope}
% ~~~
\begin{scope}[shift={(5,0)}] % RIGHT
\node [zxwhite] (a) at (0,0.5) {};
\node (2l) at (-0.6,0.5) {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\end{scope}
% ~~~~~~~~ ARROWS
\draw[cd]
(0r) edge (1l)
(2l) edge (1r);
\end{tikzpicture}
\]
\end{minipage}
\begin{minipage}{0.45\linewidth} % COMULTIPLICATION
\centering
\[
\begin{tikzpicture}
\begin{scope} % LEFT
\node [zxwhite] () at (0,0.5) {};
\node (0r) at (0.6,0.5) {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\end{scope}
% ~~~~
\begin{scope}[shift={(2,0)}] % MID
\node [zxwhite] (a) at (0.5,0.5) {};
\node (1l) at (-0.6,0.5) {$  $};
\node (1r) at (1.6,0.5)  {$  $};
\node () at (0,-1) {\textsc{Comultiplication}};
\draw [rounded corners]
(-0.5,-0.5) rectangle (1.5,1.5);
\end{scope}
% ~~~~~~~~
\begin{scope}[shift={(5,0)}] % RIGHT
\node [zxwhite] () at (0,1)    {$  $};
\node [zxwhite] () at (0,0)    {$  $};
\node (2l) at (-0.6,0.5) {$  $};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\end{scope}
% ~~~~~~~~
\path[cd]
(0r) edge (1l)
(2l) edge (1r);
\end{tikzpicture}
\]
\end{minipage}
\linebreak
\vspace{1em}
% ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
\begin{minipage}{0.45\linewidth}
\centering
\[
\begin{tikzpicture} % UNIT
\begin{scope} % LEFT
\node () at (0,0.5) {$ \emptyset $};
\node (0r) at (0.6,0.5) {$  $};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\end{scope}
% ~~~~
\begin{scope}[shift={(2,0)}] % MID
\node [zxwhite] (b) at (0.5,0.5) {$  $};
\node (1l) at (-0.6,0.5) {$  $};
\node (1r) at (1.6,0.5)  {$  $};
\node () at (0,-1) {\textsc{Unit}};
\draw [rounded corners]
(-0.5,-0.5) rectangle (1.5,1.5);
\end{scope}
% ~~~
\begin{scope}[shift={(5,0)}] % RIGHT
\node [zxwhite] (a) at (0,0.5) {};
\node (2l) at (-0.6,0.5) {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\end{scope}
% ~~~~~~~~ ARROWS
\draw[cd]
(0r) edge (1l)
(2l) edge (1r);
\end{tikzpicture}
\]
\end{minipage}
\begin{minipage}{0.45\linewidth} % COUNIT
\centering
\[
\begin{tikzpicture}
\begin{scope} % LEFT
\node [zxwhite] () at (0,0.5) {};
\node (0r) at (0.6,0.5) {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\end{scope}
% ~~~~
\begin{scope}[shift={(2,0)}] % MID
\node [zxwhite] (a) at (0.5,0.5) {};
\node (1l) at (-0.6,0.5) {$  $};
\node (1r) at (1.6,0.5)  {$  $};
\node () at (0,-1) {\textsc{Counit}};
\draw [rounded corners]
(-0.5,-0.5) rectangle (1.5,1.5);
\end{scope}
% ~~~~~~~~
\begin{scope}[shift={(5,0)}] % RIGHT
\node () at (0,0.5) {$ \emptyset $};
\node (2l) at (-0.6,0.5) {$  $};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\end{scope}
% ~~~~~~~~
\path[cd]
(0r) edge (1l)
(2l) edge (1r);
\end{tikzpicture}
\]
\end{minipage}
\linebreak
\vspace{1em}
% ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
\begin{minipage}{1.0\linewidth}
\centering
\[
\begin{tikzpicture}
\begin{scope}[shift={(0,0)}]
\node [zxwhite] () at (0,0) {};
\node [zxwhite] () at (0,1) {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\node (l) at (0.6,0.5) {};
\end{scope}
\begin{scope}[shift={(2,0)}]
\node [zxwhite] (00) at (0,0) {};
\node [zxwhite] (01) at (0,1) {};
\node [zxwhite] (10) at (1,0) {};
\node [zxwhite] (11) at (1,1) {};
\draw [graph]
(00) edge (11)
(01) edge[draw=white,line width=2pt] (10)
(01) edge (10);
\draw [rounded corners]
(-0.5,-0.5) rectangle (1.5,1.5);
\node (cl) at (-0.6,0.5) {};
\node (cr) at (1.6,0.5) {};
\node () at (0.5,-1) {\textsc{Braid}};
\end{scope}
\begin{scope}[shift={(5,0)}]
\node [zxwhite](a) at (0,0) {};
\node [zxwhite](a) at (0,1) {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\node (r) at (-0.6,0.5) {};
\end{scope}
\draw[cd]
(l) edge (cl)
(r) edge (cr);
\end{tikzpicture}
\]
\end{minipage}
\end{minipage}
\caption{Basic ZX-diagrams as structured cospans}
\label{fig:basic-diagrams-as-str-csps}
\end{figure}

Translating the relations between ZX-diagrams to
structured cospans is quite straightforward.  We
provide several examples.

\[
\begin{tikzpicture}
\node () at (-3,-2.5) {\textsc{Spider Relations}};
\begin{scope}[shift={(0,0)}]
\node [zxwhite] at (0,3) {};
\node        () at (0,2.5) {$ \vdots $};
\node [zxwhite] at (0,2) {};
\node [zxwhite] at (0,1) {};
\node        () at (0,0.5) {$ \vdots $};
\node [zxwhite] at (0,0) {};
\node (00b) at (0,-0.6)  {};
\node (00r) at (0.6,1.5) {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,3.5);
\end{scope}
\begin{scope}[shift={(2,0)}] % top mid
\node [zxwhite] (i3) at (0,3)   {};
\node           ()   at (0,2.5) {$\vdots$};
\node [zxwhite] (i2) at (0,2)   {};
\node [zxwhite] (i1) at (0,1)   {};
\node           ()   at (0,0.5) {$\vdots$};
\node [zxwhite] (i0) at (0,0)   {};
\node [zxgreen] (m1) at (1,2.5) {};
\node [zxwhite] (w0) at (0.5,1.5) {};
\node [zxwhite] (w1) at (1.5,1.5) {};
\node [zxgreen] (m0) at (1,0.5) {};
\node [zxwhite] (o3) at (2,3)   {};
\node           ()   at (2,2.5) {$\vdots$};
\node [zxwhite] (o2) at (2,2)   {};
\node [zxwhite] (o1) at (2,1)   {};
\node           ()   at (2,0.5) {$\vdots$};
\node [zxwhite] (o0) at (2,0)   {};
\node           ()   at (1,1.5) {$\cdots$};
\draw [graph]
(i0) edge[bend right=10] (m0)
(i1) edge[bend left=10]  (m0)
(i2) edge[bend right=10] (m1)
(i3) edge[bend left=10]  (m1)
(m0) edge[bend right=10] (w1)
(w1) edge[bend right=10] (m1)
(m0) edge[bend left=10]  (w0)
(w0) edge[bend left=10]  (m1)
(m0) edge[bend right=10] (o0)
(m0) edge[bend left=10]  (o1)
(m1) edge[bend right=10] (o2)
(m1) edge[bend left=10]  (o3);
\draw [rounded corners]
(-0.5,-0.5) rectangle (2.5,3.5);
\node (01l) at (-0.6,1.5) {};
\node (01r) at (2.6,1.5)  {};
\node (01b) at (1,-0.6)   {};
\end{scope}
\begin{scope}[shift={(6,0)}] % top right
\node [zxwhite] at (0,3)   {};
\node        () at (0,2.5) {$\vdots$};
\node [zxwhite] at (0,2)   {};
\node [zxwhite] at (0,1)   {};
\node        () at (0,0.5) {$\vdots$};
\node [zxwhite] at (0,0)   {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,3.5);
\node (02l) at (-0.6,1.5) {};
\node (02b) at (0,-0.6)   {};
\end{scope}
%   %
\begin{scope}[shift={(0,-3)}] % mid left
\node [zxwhite] () at (0,1)   {};
\node           () at (0,0.5) {$\vdots$};
\node [zxwhite] () at (0,0)   {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\node (10t) at (0,1.6)   {};
\node (10r) at (0.6,0.5) {};
\node (10b) at (0,-0.6)  {};
\end{scope}
%   %
\begin{scope}[shift={(2,-3)}] % mid mid
\node [zxwhite] (i1) at (0,1)   {};
\node           ()   at (0,0.5) {$\vdots$};
\node [zxwhite] (i0) at (0,0)   {};
\node [zxwhite] (o1) at (2,1)   {};
\node           ()   at (2,0.5) {$\vdots$};
\node [zxwhite] (o0) at (2,0)   {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (2.5,1.5);
\node (11t) at (1,1.6)    {};
\node (11l) at (-0.6,0.5) {};
\node (11r) at (2.6,0.5)  {};
\node (11b) at (1,-0.6)   {};
\end{scope}
%   %
\begin{scope}[shift={(6,-3)}] % mide right
\node [zxwhite] () at (0,1)   {};
\node           () at (0,0.5) {$\vdots$};
\node [zxwhite] () at (0,0)   {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\node (12t) at (0,1.6)    {};
\node (12l) at (-0.6,0.5) {};
\node (12b) at (0,-0.6)   {};
\end{scope}
%   %
\begin{scope}[shift={(0,-6)}] % bottom left
\node [zxwhite] () at (0,1)   {};
\node           () at (0,0.5) {$\vdots$};
\node [zxwhite] () at (0,0)   {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\node (20t) at (0,1.6)   {};
\node (20r) at (0.6,0.5) {};
\node (20b) at (0,-0.6)  {};
\end{scope}
%   %
\begin{scope}[shift={(2,-6)}] % bottom mid
\node [zxwhite] (i1) at (0,1)   {};
\node           ()   at (0,0.5) {$\vdots$};
\node [zxwhite] (i0) at (0,0)   {};
\node [zxgreen] (m0) at (1,0.5) {};
\node [zxwhite] (o1) at (2,1)   {};
\node           ()   at (2,0.5) {$\vdots$};
\node [zxwhite] (o0) at (2,0)   {};
\draw[graph]
(i0) edge[bend right=10] (m0)