(i1) edge[bend left=10]  (m0)
(m0) edge[bend right=10] (o0)
(m0) edge[bend left=10]  (o1);
\draw [rounded corners]
(-0.5,-0.5) rectangle (2.5,1.5);
\node (21t) at (1,1.6)  {};
\node (21l) at (-0.6,0.5) {};
\node (21r) at (2.6,0.5)  {};
\end{scope}
%   %
\begin{scope}[shift={(6,-6)}] % bommot right
\node [zxwhite] at (0,1) {};
\node [zxwhite] at (0,0) {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\node (22l) at (-0.6,0.5) {};
\node (22t) at (0,1.6)  {};
\end{scope}
\draw[cd]
(00r) edge (01l)
(02l) edge (01r)
(10r) edge (11l)
(12l) edge (11r)
(20r) edge (21l)
(22l) edge (21r)
(10t) edge (00b)
(10b) edge (20t)
(11t) edge (01b)
(11b) edge (21t)
(12t) edge (02b)
(12b) edge (22t);
\end{tikzpicture}
\]
\[
\begin{tikzpicture}
\node () at (-3,-2.5) {\textsc{Cup Relation}};
\begin{scope}[shift={(0,0)}] % up left
\node [zxwhite] () at (0,0) {};
\node [zxwhite] () at (0,1) {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\node (00r) at (0.6,0.5) {};
\node (00b) at (0,-0.6) {};
\end{scope}
\begin{scope}[shift={(2,0)}] % up mid
\node [zxwhite] (a) at (0,0) {};
\node [zxwhite] (b) at (0,1) {};
\node [zxgreen] (c) at (1,0.5) {};
\draw [graph]
(a) edge[bend right=10] (c)
(b) edge[bend left=10]  (c);
\draw [rounded corners]
(-0.5,-0.5) rectangle (1.5,1.5);
\node (01l) at (-0.6,0.5) {};
\node (01r) at (1.6,0.5)  {};
\node (01b) at (0.5,-0.6) {};
\end{scope}
\begin{scope}[shift={(5,0)}] % up right
\node () at (0,0.5) {$ 0 $};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\node (02l) at (-0.6,0.5) {};
\node (02b) at (0,-0.6) {};
\end{scope}
% ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
\begin{scope}[shift={(0,-3)}] % mid left
\node [zxwhite] () at (0,0) {};
\node [zxwhite] () at (0,1) {};
\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] (a) at (0,0) {};
\node [zxwhite] (b) at (0,1) {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (1.5,1.5);
\node (11l) at (-0.6,0.5) {};
\node (11r) at (1.6,0.5)  {};
\node (11t) at (0.5,1.6)  {};
\node (11b) at (0.5,-0.6) {};
\end{scope}
\begin{scope}[shift={(5,-3)}] % mid right
\node () at (0,0.5) {$ 0 $};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\node (12l) at (-0.6,0.5) {};
\node (12t) at (0,1.6)    {};
\node (12b) at (0,-0.6)   {};
\end{scope}
% ~~~~~~~~~~~~~~~~~~~~~
\begin{scope}[shift={(0,-6)}] % down left
\node [zxwhite] () at (0,0) {};
\node [zxwhite] () at (0,1) {};
\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)}] % down mid
\node [zxwhite] (a) at (0,0) {};
\node [zxwhite] (b) at (0,1) {};
\node [zxwhite] (c) at (1,0.5) {};
\draw[graph]
(a) edge[bend right=10] (c)
(b) edge[bend left=10]  (c);
\draw [rounded corners]
(-0.5,-0.5) rectangle (1.5,1.5);
\node (21l) at (-0.6,0.5) {};
\node (21r) at (1.6,0.5)  {};
\node (21t) at (0.5,1.6)  {};
\node (21b) at (0.5,-0.6) {};
\end{scope}
\begin{scope}[shift={(5,-6)}] % down right
\node () at (0,0.5) {$ 0 $};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\node (22l) at (-0.6,0.5) {};
\node (22t) at (0,1.6)    {};
\node (22b) at (0,-0.6)   {};
\end{scope}
% ~~~~~~~~~~~~~~~~~~~
\path[cd]
(00r) edge (01l)
(02l) edge (01r)
(10r) edge (11l)
(12l) edge (11r)
(20r) edge (21l)
(22l) edge (21r)
(00b) edge (10t)
(20t) edge (10b)
(01b) edge (11t)
(21t) edge (11b)
(02b) edge (12t)
(22t) edge (12b);
\end{tikzpicture}
\]

The remaining relations from Figure
\ref{fig:zx-equations} can be translated into
spans of structured cospans in this way.  We include an additional rewrite
\[
\begin{tikzpicture}
\node () at (-3,-2) {\textsc{Wire Relation}};
\begin{scope}[shift={(0,0)}] % up left
\node [zxwhite] () at (0,0) {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,0.5);
\node (00r) at (0.6,0) {};
\node (00b) at (0,-0.6) {};
\end{scope}
\begin{scope}[shift={(2,0)}] % up mid
\node [zxwhite] (a) at (0,0) {};
\node [zxwhite] (b) at (1,0) {};
\draw [graph] (a) to (b);
\draw [rounded corners]
(-0.5,-0.5) rectangle (1.5,0.5);
\node (01l) at (-0.6,0) {};
\node (01r) at (1.6,0)  {};
\node (01b) at (0.5,-0.6) {};
\end{scope}
\begin{scope}[shift={(5,0)}] % up right
\node [zxwhite] () at (0,0) {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,0.5);
\node (02l) at (-0.6,0) {};
\node (02b) at (0,-0.6) {};
\end{scope}
% ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
\begin{scope}[shift={(0,-2)}] % mid left
\node [zxwhite] () at (0,0) {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,0.5);
\node (10t) at (0,0.6)   {};
\node (10r) at (0.6,0) {};
\node (10b) at (0,-0.6)  {};
\end{scope}
\begin{scope}[shift={(2,-2)}] % mid mid
\node [zxwhite] (a) at (0,0) {};
\node [zxwhite] (b) at (1,0) {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (1.5,0.5);
\node (11l) at (-0.6,0) {};
\node (11r) at (1.6,0)  {};
\node (11t) at (0.5,0.6)  {};
\node (11b) at (0.5,-0.6) {};
\end{scope}
\begin{scope}[shift={(5,-2)}] % mid right
\node [zxwhite] () at (0,0) {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,0.5);
\node (12l) at (-0.6,0) {};
\node (12t) at (0,0.6)  {};
\node (12b) at (0,-0.6) {};
\end{scope}
% ~~~~~~~~~~~~~~~~~~~~~
\begin{scope}[shift={(0,-4)}] % down left
\node [zxwhite] () at (0,0) {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,0.5);
\node (20t) at (0,0.6)   {};
\node (20r) at (0.6,0) {};
\end{scope}
\begin{scope}[shift={(2,-4)}] % down mid
\node [zxwhite] (a) at (0.5,0) {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (1.5,0.5);
\node (21l) at (-0.6,0) {};
\node (21r) at (1.6,0)  {};
\node (21t) at (0.5,0.6)  {};
\end{scope}
\begin{scope}[shift={(5,-4)}] % down right
\node [zxwhite] () at (0,0) {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,0.5);
\node (22l) at (-0.6,0) {};
\node (22t) at (0,0.6)  {};
\end{scope}
% ~~~~~~~~~~~~~~~~~~~
\draw[cd]
(00r) edge node[]{$  $} (01l)
(02l) edge node[]{$  $} (01r)
(10r) edge node[]{$  $} (11l)
(12l) edge node[]{$  $} (11r)
(20r) edge node[]{$  $} (21l)
(22l) edge node[]{$  $} (21r)
(10t) edge[] (00b)
(10b) edge[] (20t)
(11t) edge[] (01b)
(11b) edge[] (21t)
(12t) edge[] (02b)
(12b) edge[] (22t);
\end{tikzpicture}
\]
to account for the fact that the wire structured
cospan in Figure
\ref{fig:basic-diagrams-as-str-csps}
is, a priori, not an identity. This wire relation
ensures that the wire structured cospan is an

We are now ready to define the double category
$ \ZZZX $.

\begin{definition}
\label{def:zx-double-category}
\[
\adjunction{\FinSet}{\FinGraphGamma}{L}{R}{4}
\]
be the adjunction defined so that $ L $ assigns a set to
the discrete graph that is constant over the white node on
that set and where $ R $ returns the set of white nodes of
a graph over $ \Gamma $.  Define $\ZZZX$ to be the
isofibrant symmetric monoidal sub-double of
$_L \BBBoldRewrite$ generated by the basic structured
cospans and the basic rewrites for ZX-diagrams.
\end{definition}

In this definition, using $ _L \BBBoldRewrite $ as an
ambient double category ensures that generating $ \ZZZX $ is
well-defined. All of the required structure and properties
are in place and $ _L \BBBoldRewrite $ bounds the
generation. Now, because $ \ZZZX $ is an isofibrant
symmetric monoidal category---true by construction---we use
Shulman's work
[58]
to provide the symmetric monoidal bicategory
$ \ZZX $.

\begin{proposition}
There is a symmetric monoidal bicategory $ \ZZX
$ whose objects are finite sets, 1-arrows are
generated by the basic $ L $-structured cospans
in Figure \ref{fig:basic-diagrams-as-str-csps},
and 2-arrows are bold rewrites generated by the
basic rewrites of ZX-diagrams.
\end{proposition}

The ZX-diagrams appear in $ \ZZZX $ as horizontal 1-arrows
and in $ \ZZX $ as 1-arrows. Composing the ZX-diagrams works
as it does in the original ZX-calculus; pushout formalizes
the gluing of dangling edges. Indeed, composing basic
diagrams provides `compound' diagrams. For example,
\[
\begin{tikzpicture}
\begin{scope}
\node [zxwhite] () at (0,0) {};
\node [zxwhite] () at (0,1) {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\node (0r) at (0.6,0.5) {};
\end{scope}
% ~~
\begin{scope}[shift={(2,1)}]
\node [zxwhite]  (a) at (0,0)    {};
\node [zxwhite]  (b) at (0,1)    {};
\node [zxgreen]  (c) at (1,0.5)  {};
\node            ()  at (1,1)    {$ \alpha $};
\node [zxwhite]  (d) at (2,0.5)  {};
\draw[graph]
(a) edge[bend right=10] (c)
(b) edge[bend left=10]  (c)
(c) edge                (d);
\draw [rounded corners]
(-0.5,-0.5) rectangle (2.5,1.5);
\node (1l) at (-0.6,0.5) {};
\node (1r) at (2.6,0.5)  {};
\end{scope}
% ~~
\begin{scope}[shift={(6,0)}]
\node [zxwhite] () at (0,0.5) {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\node (2l) at (-0.6,0.5) {};
\node (2r) at (0.6,0.5) {};
\end{scope}
% ~~
\begin{scope}[shift={(8,1)}]
\node [zxwhite] (a) at (0,0.5) {};
\node [zxgreen] (b) at (1,0.5) {};
\node           ( ) at (1,1)   {$\beta$};
\node [zxwhite] (c) at (2,0.5) {};
\draw [graph]
(a) edge (b)
(b) edge (c);
\draw [rounded corners]
(-0.5,-0.5) rectangle (2.5,1.5);
\node (3l) at (-0.6,0.5) {};
\node (3r) at (2.6,0.5)  {};
\end{scope}
% ~~
\begin{scope}[shift={(12,0)}]
\node [zxwhite] () at (0,0.5) {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\node (4l) at (-0.6,0.5) {};
\end{scope}
% ~~
\draw[cd]
(0r) edge node[]{$  $} (1l)
(2l) edge node[]{$  $} (1r)
(2r) edge node[]{$  $} (3l)
(4l) edge node[]{$  $} (3r);
\end{tikzpicture}
\]
\[
\begin{tikzpicture}
\begin{scope}
\node [zxwhite] () at (0,0) {};
\node [zxwhite] () at (0,1) {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\node (0r) at (0.6,0.5) {};
\end{scope}
% ~~
\begin{scope}[shift={(2,1)}]
\node [zxwhite]  (a) at (0,0)    {};
\node [zxwhite]  (b) at (0,1)    {};
\node [zxgreen]  (c) at (1,0.5)  {};
\node            ( ) at (1,1)    {$\alpha$};
\node [zxwhite]  (d) at (2,0.5)  {};
\node [zxgreen]  (e) at (3,0.5)  {};
\node            ( ) at (3,1)    {$\beta$};
\node [zxwhite]  (f) at (4,0.5)  {};
\draw[graph]
(a) edge[bend right=10] (c)
(b) edge[bend left=10]  (c)
(c) edge                (d)
(d) edge                (e)
(e) edge                (f);
\draw [rounded corners]
(-0.5,-0.5) rectangle (4.5,1.5);
\node (1l) at (-0.6,0.5) {};
\node (1r) at (4.6,0.5)  {};
\end{scope}
% ~~
\begin{scope}[shift={(8,0)}]
\node [zxwhite] () at (0,0.5) {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\node (2l) at (-0.6,0.5) {};
\end{scope}
% ~~
\draw[cd]
(0r) edge (1l)
(2l) edge (1r);
\end{tikzpicture}
\]
To this, we can apply the Spider Relation
\[
\begin{tikzpicture}
\begin{scope}[shift={(0,0)}] % top left
\node [zxwhite] at (0,1) {};
\node [zxwhite] at (0,0) {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\node (00b) at (0,-0.6)  {};
\node (00r) at (0.6,0.5) {};
\end{scope}
\begin{scope}[shift={(2,0)}] % top mid
\node [zxwhite]  (a) at (0,0)    {};
\node [zxwhite]  (b) at (0,1)    {};
\node [zxgreen]  (c) at (1,0.5)  {};
\node            ( ) at (1,1)    {$\alpha$};
\node [zxwhite]  (d) at (2,0.5)  {};
\node [zxgreen]  (e) at (3,0.5)  {};
\node            ( ) at (3,1)    {$\beta$};
\node [zxwhite]  (f) at (4,0.5)  {};
\draw[graph]
(a) edge[bend right=10] (c)
(b) edge[bend left=10]  (c)
(c) edge                (d)
(d) edge                (e)
(e) edge                (f);
\draw [rounded corners]
(-0.5,-0.5) rectangle (4.5,1.5);
\node (01l) at (-0.6,0.5) {};
\node (01r) at (4.6,0.5)  {};
\node (01b) at (2,-0.6)   {};
\end{scope}
\begin{scope}[shift={(8,0)}] % top right
\node [zxwhite] () at (0,0.5) {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\node (02l) at (-0.6,0.5) {};
\node (02b) at (0,-0.6)   {};
\end{scope}
%   %
\begin{scope}[shift={(0,-3)}] % mid left
\node [zxwhite] () at (0,1)   {};
\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 [zxwhite] (i0) at (0,0)   {};
\node [zxwhite] (o0) at (4,0.5) {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (4.5,1.5);
\node (11t) at (2,1.6)    {};
\node (11l) at (-0.6,0.5) {};
\node (11r) at (4.6,0.5)  {};
\node (11b) at (2,-0.6)   {};
\end{scope}
%   %
\begin{scope}[shift={(8,-3)}] % mide right
\node [zxwhite] () at (0,0.5) {};
\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 [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) {};
\end{scope}
%   %
\begin{scope}[shift={(2,-6)}] % bottom mid
\node [zxwhite]  (a) at (0,0)    {};
\node [zxwhite]  (b) at (0,1)    {};
\node [zxgreen]  (c) at (2,0.5)  {};
\node            ( ) at (2,1)    {$\alpha+\beta$};
\node [zxwhite]  (d) at (4,0.5)  {};
\draw[graph]
(a) edge[bend right=10] (c)
(b) edge[bend left=10]  (c)
(c) edge                (d);
\draw [rounded corners]
(-0.5,-0.5) rectangle (4.5,1.5);
\node (21t) at (2,1.6)  {};
\node (21l) at (-0.6,0.5) {};
\node (21r) at (4.6,0.5)  {};
\end{scope}
%   %
\begin{scope}[shift={(8,-6)}] % bommot right
\node [zxwhite] at (0,0.5) {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\node (22l) at (-0.6,0.5) {};
\node (22t) at (0,1.6)  {};
\end{scope}
\draw[cd]
(00r) edge (01l)
(02l) edge (01r)
(10r) edge (11l)
(12l) edge (11r)
(20r) edge (21l)
(22l) edge (21r)
(10t) edge (00b)
(10b) edge (20t)
(11t) edge (01b)
(11b) edge (21t)
(12t) edge (02b)
(12b) edge (22t);
\end{tikzpicture}
\]
Because the vertical 1-arrows are identities, this 2-arrow
exists in both $ \ZZZX $ and $ \ZZX $. The spider relation
simplifies the ZX-diagram in the top row to that in the
bottom row.

\begin{theorem}
The bicategory $ \ZZX $ is a bicategory of relations.
\end{theorem}

\begin{proof}
Because $ \ZZX $ includes the structure maps to give every
object a Frobenius monoid structure, every requirement
descends from ambient category $ _L \BBoldRewrite $ being
a bicategory of relations (see Theorem
\ref{thm:bold-rewrite-bicat-rels}).
\end{proof}

This bicategory extends the original category $ \ZX $. To
show this, we will show the `decategorification' of $ \ZZX $
is $ \ZX $. The process of decategorification essentially
turns an $ n $-category into an $ n-1 $-category. For us, we
turn a (weak) 2-category into a 1-category by identifying any
1-arrows connected by a zig-zag of 2-arrows.

\begin{definition} \label{def:decat-zx}

Define $\decat (\ZZX)$ to be the category whose objects
are those of $\ZZX$ and whose arrows the 1-arrows of
$\ZZX $ modulo the equivalence relation $\sim$ generated
by $f \sim g$ if and only if there is a 2-arrow
$f \Rightarrow g$ in $\ZZX$.

\end{definition}

\begin{theorem} \label{thm:decatzx-is-dagger-compact}

The category $\decat ( \ZZX )$ is dagger compact
via the identity on objects functor described by
\[
\begin{tikzpicture}
% FIRST DIAGRAM
\begin{scope}[shift={(0,0)}] % left left
\node [zxwhite] ()  at (0,1)    {};
\node           ()  at (0,0.75) {$\vdots$};
\node [zxwhite] ()  at (0,0)    {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\node (0r) at (0.6,0.5) {$  $};
\end{scope}
% ~~
\begin{scope}[shift={(2,1)}] % left mid
\node [zxwhite] (a) at (0,1) {};
\node           ()  at (0.25,0.75) {$\vdots$};
\node [zxwhite] (b) at (0,0) {};
\node [zxgreen] (c) at (1,0.5) {};
\node           ( ) at (1,1) {$\alpha$};
\node [zxwhite] (d) at (2,1) {};
\node           ()  at (1.75,0.75) {$\vdots$};
\node [zxwhite] (e) at (2,0) {};
\draw[graph]
(a) edge[bend left=10]  (c)
(b) edge[bend right=10] (c)
(c) edge[bend left=10]  (d)
(c) edge[bend right=10] (e);
\draw [rounded corners]
(-0.5,-0.5) rectangle (2.5,1.5);
\node (1l) at (-0.6,0.5) {$  $};
\node (1r) at (2.6,0.5)  {$  $};
\end{scope}
% ~~
\begin{scope}[shift={(6,0)}] % left right
\node [zxwhite] () at  (0,1)     {};
\node           ()  at (0,0.75) {$\vdots$};
\node [zxwhite] () at  (0,0)     {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\node (2l) at (-0.6,0.5) {$  $};
\end{scope}
% ~~
\path[cd] % left arrows
(0r) edge node[]{$  $} (1l)
(2l) edge node[]{$  $} (1r);
% ~~
% MAPSTO
\node () at (7,1) {$ \xmapsto{\dagger} $};
% ~~
% SECOND DIAGRAM
\begin{scope}[shift={(8,0)}] % right left
\node [zxwhite] () at (0,1) {};
\node           () at (0,0.75) {$\vdots$};
\node [zxwhite] () at (0,0) {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\node (0'r) at (0.6,0.5) {$  $};
\end{scope}
% ~~
\begin{scope}[shift={(10,1)}] % right mid
\node [zxwhite] (a) at (0,1) {};
\node           ()  at (0.25,0.75) {$\vdots$};
\node [zxwhite] (b) at (0,0) {};
\node [zxgreen] (c) at (1,0.5) {};
\node           ( ) at (1,1)       {$-\alpha$};
\node [zxwhite] (d) at (2,1) {};
\node           ()  at (1.75,0.75) {$\vdots$};
\node [zxwhite] (e) at (2,0) {};
\draw[graph]
(a) edge[bend left=10]  (c)
(b) edge[bend right=10] (c)
(c) edge[bend left=10]  (d)
(c) edge[bend right=10] (e);
\draw [rounded corners]
(-0.5,-0.5) rectangle (2.5,1.5);
\node (1'l) at (-0.6,0.5) {$  $};
\node (1'r) at (2.6,0.5)  {$  $};
\end{scope}
% ~~
\begin{scope}[shift={(14,0)}] % right right
\node [zxwhite] () at (0,1) {};
\node           () at (0,0.75) {$\vdots$};
\node [zxwhite] () at (0,0) {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\node (2'l) at (-0.6,0.5) {$  $};
\end{scope}
% ~~
\path[cd] % right arrows
(0'r) edge node[]{$  $} (1'l)
(2'l) edge node[]{$  $} (1'r);
\end{tikzpicture}
\]
\[
\begin{tikzpicture}
% FIRST DIAGRAM
\begin{scope}[shift={(0,0)}] % left left
\node [zxwhite] () at (0,1)     {};
\node           ()  at (0,0.75) {$\vdots$};
\node [zxwhite] () at (0,0)     {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\node (0r) at (0.6,0.5) {$  $};
\end{scope}
% ~~
\begin{scope}[shift={(2,1)}] % left mid
\node [zxwhite] (a) at (0,1) {};
\node           ()  at (0.25,0.75) {$\vdots$};
\node [zxwhite] (b) at (0,0) {};
\node [zxred] (c) at (1,0.5) {};
\node           ( ) at (1,1) {$\alpha$};
\node [zxwhite] (d) at (2,1) {};
\node           ()  at (1.75,0.75) {$\vdots$};
\node [zxwhite] (e) at (2,0) {};
\draw[graph]
(a) edge[bend left=10]  (c)
(b) edge[bend right=10] (c)
(c) edge[bend left=10]  (d)
(c) edge[bend right=10] (e);
\draw [rounded corners]
(-0.5,-0.5) rectangle (2.5,1.5);
\node (1l) at (-0.6,0.5) {$  $};
\node (1r) at (2.6,0.5)  {$  $};
\end{scope}
% ~~
\begin{scope}[shift={(6,0)}] % left right
\node [zxwhite] () at (0,1)     {};
\node           ()  at (0,0.75) {$\vdots$};
\node [zxwhite] () at (0,0)     {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\node (2l) at (-0.6,0.5) {$  $};
\end{scope}
% ~~
\path[cd] % left arrows
(0r) edge node[]{$  $} (1l)
(2l) edge node[]{$  $} (1r);
% ~~
% MAPSTO
\node () at (7,1) {$ \xmapsto{\dagger} $};
% ~~
% SECOND DIAGRAM
\begin{scope}[shift={(8,0)}] % right left
\node [zxwhite] () at (0,1) {};
\node           () at (0,0.75) {$\vdots$};
\node [zxwhite] () at (0,0) {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\node (0'r) at (0.6,0.5) {$  $};
\end{scope}
% ~~
\begin{scope}[shift={(10,1)}] % right mid
\node [zxwhite] (a) at (0,1) {};
\node           ()  at (0.25,0.75) {$\vdots$};
\node [zxwhite] (b) at (0,0) {};
\node [zxred] (c) at (1,0.5) {};
\node           ( ) at (1,1)       {$-\alpha$};
\node [zxwhite] (d) at (2,1) {};
\node           ()  at (1.75,0.75) {$\vdots$};
\node [zxwhite] (e) at (2,0) {};
\draw[graph]
(a) edge[bend left=10]  (c)
(b) edge[bend right=10] (c)
(c) edge[bend left=10]  (d)
(c) edge[bend right=10] (e);
\draw [rounded corners]
(-0.5,-0.5) rectangle (2.5,1.5);
\node (1'l) at (-0.6,0.5) {$  $};
\node (1'r) at (2.6,0.5)  {$  $};
\end{scope}
% ~~
\begin{scope}[shift={(14,0)}] % right right
\node [zxwhite] () at (0,1) {};
\node           () at (0,0.75) {$\vdots$};
\node [zxwhite] () at (0,0) {};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,1.5);
\node (2'l) at (-0.6,0.5) {$  $};
\end{scope}
% ~~
\draw[cd] % right arrows
(0'r) edge node[]{$  $} (1'l)
(2'l) edge node[]{$  $} (1'r);
\end{tikzpicture}
\]
as well as by identity on the wire, Hadamard, and
diamond morphisms.
\end{theorem}

\begin{proof}
Compact closedness follows from the self duality of
objects via the evaluation
\[
\begin{tikzpicture}
\begin{scope}
\node [zxwhite] (a) at  (0,2)   {$  $};
\node [zxwhite] (b) at  (0,1.5) {$  $};
\node           ( )  at (0,1)   {$\vdots$};
\node [zxwhite] (c) at  (0,0.5) {$  $};
\node [zxwhite] (d) at  (0,0)   {$  $};
\node (0r) at (0.6,1) {$  $};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,2.5);
\end{scope}
% ~~~~~~~~~~
\begin{scope}[shift={(2,1)}]
\node [zxwhite] (a) at (0,2)      {$  $};
\node [zxwhite] (b) at (0,1.5)    {$  $};
\node           ( ) at (0,1)      {$\vdots$};
\node [zxwhite] (c) at (0,0.5)    {$  $};
\node [zxwhite] (d) at (0,0)      {$  $};
\node [zxwhite] (e) at (0.5,1)    {$  $};
\node [zxwhite] (f) at (1,1)      {$  $};
\draw[graph]
(a) edge[bend left=10]  (f)
(d) edge[bend right=10] (f)
(b) edge[bend left=10]  (e)
(c) edge[bend right=10] (e);
\node (1l) at (-0.6,1) {$  $};
\node (1r) at (1.6,1)  {$  $};
\draw [rounded corners]
(-0.5,-0.5) rectangle (1.5,2.5);
\end{scope}
% ~~~~~~~~
\begin{scope}[shift={(5,0)}]
\node (a) at (0,1) {$ \emptyset $};
\node (2l) at (-0.6,1) {$  $};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,2.5);
\end{scope}
% ~~~~~~~~
\path[cd]
(0r) edge node[]{$  $} (1l)
(2l) edge node[]{$  $} (1r);
\end{tikzpicture}
\]
and coevaluation arrows
\[
\begin{tikzpicture}
\begin{scope}
\node (a) at (0,1) {$ \emptyset $};
\node (0r) at (0.6,1) {$  $};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,2.5);
\end{scope}
% ~~~~~~~~~~
\begin{scope}[shift={(2,1)}]
\node [zxwhite] (a) at (1,2)      {$  $};
\node [zxwhite] (b) at (1,1.5)    {$  $};
\node           ( ) at (1,1)      {$\vdots$};
\node [zxwhite] (c) at (1,0.5)    {$  $};
\node [zxwhite] (d) at (1,0)      {$  $};
\node [zxwhite] (e) at (0.5,1)    {$  $};
\node [zxwhite] (f) at (0,1)      {$  $};
\draw[graph]
(f) edge[bend left=10]  (a)
(f) edge[bend right=10] (d)
(e) edge[bend left=10]  (b)
(e) edge[bend right=10] (c);
\node (1l) at (-0.6,1) {$  $};
\node (1r) at (1.6,1)  {$  $};
\draw [rounded corners]
(-0.5,-0.5) rectangle (1.5,2.5);
\end{scope}
% ~~~~~~~~
\begin{scope}[shift={(5,0)}]
\node [zxwhite] (a) at  (0,2)   {$  $};
\node [zxwhite] (b) at  (0,1.5) {$  $};
\node           ( )  at (0,1)   {$\vdots$};
\node [zxwhite] (c) at  (0,0.5) {$  $};
\node [zxwhite] (d) at  (0,0)   {$  $};
\node (2l) at (-0.6,1) {$  $};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,2.5);
\end{scope}
% ~~~~~~~~
\draw[cd]
(0r) edge (1l)
(2l) edge (1r);
\end{tikzpicture}
\]
obtained by applying the braiding maps to the disjoint
union of cups and caps. Moreover, we can derive the snake
equation as follows. Decompose the arrow
\[
\begin{tikzpicture} % SNAKE COMPOSED
\begin{scope} % LEFT
\node [zxwhite] () at (0,0) {$  $};
\node (0r) at (0.6,1) {$  $};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,2.5);
\end{scope}
% ~~
\begin{scope}[shift={(2,1)}] % MID
\node [zxwhite] (a) at (0,0) {$  $};
\node [zxwhite] (b) at (0.5,1.5) {$  $};
\node [zxwhite] (c) at (1,0) {$  $};
\node [zxwhite] (d) at (1,1) {$  $};
\node [zxwhite] (e) at (1,2) {$  $};
\node [zxwhite] (f) at (1.5,0.5) {$  $};
\node [zxwhite] (g) at (2,2) {$  $};
\draw[graph]
(a) edge[bend right=0]   (c)
(c) edge[bend right=10]  (f)
(d) edge[bend right=-10] (f)
(b) edge[bend right=10]  (d)
(b) edge[bend right=-10] (e)
(e) edge[bend right=0]   (g);
\node (1l) at (-0.6,1) {$  $};
\node (1r) at (2.6,1) {$  $};
\draw [rounded corners]
(-0.5,-0.5) rectangle (2.5,2.5);
\end{scope}
\begin{scope}[shift={(6,0)}] % LEFT
\node [zxwhite] () at (0,2) {$  $};
\node (2l) at (-0.6,1) {$  $};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,2.5);
\end{scope}
\path[cd]
(0r) edge node[]{$  $} (1l)
(2l) edge node[]{$  $} (1r);
\end{tikzpicture}
\]
\[
\begin{tikzpicture}
\begin{scope} % LEFT
\node [zxwhite] () at (0,0) {$  $};
\node (0r) at (0.6,1) {$  $};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,2.5);
\end{scope}
% ~~
\begin{scope}[shift={(2,1)}] % LEFT MID
\node [zxwhite] (a) at (0,0) {$  $};
\node [zxwhite] (b) at (0.5,1.5) {$  $};
\node [zxwhite] (c) at (1,0) {$  $};
\node [zxwhite] (d) at (1,1) {$  $};
\node [zxwhite] (e) at (1,2) {$  $};
\draw[graph]
(a) edge                (c)
(b) edge[bend right=10] (d)
(b) edge[bend left=10]  (e);
\node (1l) at (-0.6,1) {$  $};
\node (1r) at (1.6,1) {$  $};
\draw [rounded corners]
(-0.5,-0.5) rectangle (1.5,2.5);
\end{scope}
\begin{scope}[shift={(5,0)}] % GLUE
\node [zxwhite] () at (0,2) {$  $};
\node [zxwhite] () at (0,1) {$  $};
\node [zxwhite] () at (0,0) {$  $};
\node (2l) at (-0.6,1) {$  $};
\node (2r) at (0.6,1)  {$  $};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,2.5);
\end{scope}
\begin{scope}[shift={(7,1)}] % LEFT MID
\node [zxwhite] (a) at (1,2) {$  $};
\node [zxwhite] (b) at (0.5,0.5) {$  $};
\node [zxwhite] (c) at (0,0) {$  $};
\node [zxwhite] (d) at (0,1) {$  $};
\node [zxwhite] (e) at (0,2) {$  $};
\draw[graph]
(a) edge                (e)
(c) edge[bend right=10] (b)
(d) edge[bend left=10]  (b);
\node (3l) at (-0.6,1) {$  $};
\node (3r) at (1.6,1) {$  $};
\draw [rounded corners]
(-0.5,-0.5) rectangle (1.5,2.5);
\end{scope}
\begin{scope}[shift={(10,0)}] % RIGHT
\node [zxwhite] () at (0,2) {$  $};
\node (4l) at (-0.6,1) {$  $};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,2.5);
\end{scope}
\draw[cd]
(0r) edge node[]{$  $} (1l)
(2l) edge node[]{$  $} (1r)
(2r) edge node[]{$  $} (3l)
(4l) edge node[]{$  $} (3r);
\end{tikzpicture}
\]
which by the cup relation, illustrated in Figure
\ref{fig:zx-equations}, equals
\[
\begin{tikzpicture}
\begin{scope} % LEFT
\node [zxwhite] () at (0,0) {$  $};
\node (0r) at (0.6,1) {$  $};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,2.5);
\end{scope}
% ~~
\begin{scope}[shift={(2,1)}] % LEFT MID
\node [zxwhite] (a) at (0,0) {$  $};
\node [zxgreen] (b) at (0.5,1.5) {$  $};
\node [zxwhite] (c) at (1,0) {$  $};
\node [zxwhite] (d) at (1,1) {$  $};
\node [zxwhite] (e) at (1,2) {$  $};
\draw[graph]
(a) edge                (c)
(b) edge[bend right=10] (d)
(b) edge[bend left=10]  (e);
\node (1l) at (-0.6,1) {$  $};
\node (1r) at (1.6,1) {$  $};
\draw [rounded corners]
(-0.5,-0.5) rectangle (1.5,2.5);
\end{scope}
\begin{scope}[shift={(5,0)}] % GLUE
\node [zxwhite] () at (0,2) {$  $};
\node [zxwhite] () at (0,1) {$  $};
\node [zxwhite] () at (0,0) {$  $};
\node (2l) at (-0.6,1) {$  $};
\node (2r) at (0.6,1)  {$  $};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,2.5);
\end{scope}
\begin{scope}[shift={(7,1)}] % LEFT MID
\node [zxwhite] (a) at (1,2) {$  $};
\node [zxgreen] (b) at (0.5,0.5) {$  $};
\node [zxwhite] (c) at (0,0) {$  $};
\node [zxwhite] (d) at (0,1) {$  $};
\node [zxwhite] (e) at (0,2) {$  $};
\draw[graph]
(a) edge                (e)
(c) edge[bend right=10] (b)
(d) edge[bend left=10]  (b);
\node (3l) at (-0.6,1) {$  $};
\node (3r) at (1.6,1) {$  $};
\draw [rounded corners]
(-0.5,-0.5) rectangle (1.5,2.5);
\end{scope}
\begin{scope}[shift={(10,0)}] % RIGHT
\node [zxwhite] () at (0,2) {$  $};
\node (4l) at (-0.6,1) {$  $};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,2.5);
\end{scope}
\draw[cd]
(0r) edge (1l)
(2l) edge (1r)
(2r) edge (3l)
(4l) edge (3r);
\end{tikzpicture}
\]
This can be composed to get
\[
\begin{tikzpicture} % SNAKE COMPOSED
\begin{scope} % LEFT
\node [zxwhite] () at (0,0) {$  $};
\node (0r) at (0.6,1) {$  $};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,2.5);
\end{scope}
% ~~
\begin{scope}[shift={(2,1)}] % MID
\node [zxwhite] (a) at (0,0) {$  $};
\node [zxgreen] (b) at (0.5,1.5) {$  $};
\node [zxwhite] (c) at (1,0) {$  $};
\node [zxwhite] (d) at (1,1) {$  $};
\node [zxwhite] (e) at (1,2) {$  $};
\node [zxgreen] (f) at (1.5,0.5) {$  $};
\node [zxwhite] (g) at (2,2) {$  $};
\draw[graph]
(a) edge                (c)
(c) edge[bend right=10] (f)
(d) edge[bend left=10]  (f)
(b) edge[bend right=10] (d)
(b) edge[bend left=10]  (e)
(e) edge                (g);
\node (1l) at (-0.6,1) {$  $};
\node (1r) at (2.6,1) {$  $};
\draw [rounded corners]
(-0.5,-0.5) rectangle (2.5,2.5);
\end{scope}
\begin{scope}[shift={(6,0)}] % LEFT
\node [zxwhite] () at (0,2) {$  $};
\node (2l) at (-0.6,1) {$  $};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,2.5);
\end{scope}
\path[cd]
(0r) edge (1l)
(2l) edge (1r);
\end{tikzpicture}
\]
which equals
\[
\begin{tikzpicture} % SNAKE COMPOSED
\begin{scope} % LEFT
\node [zxwhite] () at (0,0) {$  $};
\node (0r) at (0.6,0) {$  $};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,0.5);
\end{scope}
% ~~
\begin{scope}[shift={(2,1)}] % MID
\node [zxwhite] (a) at (0,0) {$  $};
\node [zxwhite] (b) at (1,0) {$  $};
\node [zxgreen] (c) at (2,0) {$  $};
\node [zxwhite] (d) at (3,0) {$  $};
\node [zxwhite] (e) at (4,0) {$  $};
\draw [graph]
(a) edge (b)
(b) edge (c)
(c) edge (d)
(d) edge (e);
\node (1l) at (-0.6,0) {$  $};
\node (1r) at (4.6,0) {$  $};
\draw [rounded corners]
(-0.5,-0.5) rectangle (4.5,0.5);
\end{scope}
\begin{scope}[shift={(8,0)}] % LEFT
\node [zxwhite] () at (0,0) {$  $};
\node (2l) at (-0.6,0) {$  $};
\draw [rounded corners]
(-0.5,-0.5) rectangle (0.5,0.5);
\end{scope}
\path[cd]
(0r) edge node[]{$  $} (1l)
(2l) edge node[]{$  $} (1r);
\end{tikzpicture}
\]
because of the spider relation. Finally, this
equals the identity because of the trivial
spider and wire relations.  Showing that the
described functor is a dagger functor is a
matter of checking some easy to verify details.
\end{proof}

We now show that $ \ZZZX $ is an extension of
$ \ZX $ in the sense that the category
$ \decat ( \ZZX ) $ obtained from $ \ZZZX $ is
equivalent to $ \ZX $.

\begin{theorem}
\label{thm:equiv of zx cats}
The identity on objects, dagger compact functor
$E \colon \ZX \to
\operatorname{decat}(\ZZX)$
given by
\begin{align*}
\raisebox{
\includegraphics{generater_green_spider}}
\begin{tikzpicture}
\node () at (-1,0.5) {$ \mapsto  $};
\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)  {};
\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}
\draw[cd,>=angle 90]
(l) edge node[]{$  $} (cl)
(r) edge node[]{$  $} (cr);
\end{tikzpicture}
\\
\raisebox{
\includegraphics{generater_red_spider}}
\begin{tikzpicture}
\node () at (-1,0.5) {$ \mapsto  $};
\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)  {};
\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}
\draw[cd]
(l) edge node[]{$  $} (cl)
(r) edge node[]{$  $} (cr);
\end{tikzpicture}
\\
\raisebox{
\includegraphics{generater_wire}}
\begin{tikzpicture}
\node () at (-1,0) {$ \mapsto  $};
\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) {};
\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}
\\
\raisebox{
\includegraphics{generater_diamond}}
\begin{tikzpicture}
\node () at (-1,0) {$ \mapsto  $};
\begin{scope}[shift={(0,0)}]
\node () at (0,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 [zxblack] () at (1,0) {$$};
\draw [rounded corners]
(-0.5,-0.5) rectangle (2.5,0.5);
\node (cl) at (-0.6,0) {};
\node (cr) at (2.6,0) {};
\end{scope}
\begin{scope}[shift={(6,0)}]
\node (a) at (0,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 node[]{$  $} (cl)
(r) edge node[]{$  $} (cr);
\end{tikzpicture}
\\
\raisebox{
\includegraphics{generater_hadamard}}
\begin{tikzpicture}
\node () at (-1,0) {$ \mapsto  $};
\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)  {};
\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 node[]{$  $} (cl)
(r) edge node[]{$  $} (cr);
\end{tikzpicture}
\end{align*}
is an equivalence of categories.
\end{theorem}

\begin{proof}
Essential surjectivity follows immediately from
$E$ being identity on objects.  Fullness follows
from the fact that the morphism generators for
$\decat (\ZZX)$ are all in the image of $E$.

Faithfulness is more involved. Let $f,g$ be
$\ZX$-morphisms. Let $\widetilde{Ef}$,
$\widetilde{Eg}$ be the representatives of $Ef$,
$Eg$ obtained by directly translating the
graphical representation of $f,g$ to structured
cospans of graphs of $\Gamma$. For faithfulness,
it suffices to show that the existence of a
$\widetilde{Ef} \Rightarrow \widetilde{Eg}$ in
$\ZZX$ implies that $f=g$.

Observe that any 2-arrow $\alpha$ in $\ZZX$ can
be written, not necessarily uniquely, as
$\alpha_1 \square \dotsm \square \alpha_n$ of
length $n$ where each $\alpha_i$ is a basic
$2$-cell and each box is filled in with
`$\hcirc$', `$\vcirc$', or `$+$'. By `$\hcirc$'
and `$\vcirc$', we mean horizontal and vertical
composition. We will induct on sequence length.
$\alpha \colon \widetilde{Ef} \Rightarrow
\widetilde{Eg}$ is a basic 2-arrow, then there
is clearly a corresponding basic relation
equating $f$ and $g$.  Suppose we have a
sequence of length $n+1$ such that the left-most
square is a `$+$'. When we have a 2-arrow
$\alpha_1 + \alpha_2 \colon Ef \Rightarrow Eg$
where $\alpha_1$ is a basic 2-arrow and
$\alpha_2$ can be written with length $n$.  By
fullness, we can write
$\alpha_1 + \alpha_2 \colon Ef_1 + EF_2
\Rightarrow Eg_1 + Eg_2$ where
$\alpha_i \colon Ef_i \Rightarrow Eg_i$.  This
gives that $f_i = g_i$ and the result follows.
A similar argument handles the cases when the
left-most operation is vertical or horizontal
\end{proof}

%%%%%%%%%%%%%%%%%%%                      %%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%       CHAPTER        %%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%% STRUCTURAL INDUCTION %%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%                      %%%%%%%%%%%%%%%%%

\chapter{Decomposing systems}
\label{sec:structural-induction}

The idea of decomposing a whole into parts has long been
useful. It exists across so many human disciplines, be it
academic, artistic, or artisanal. A biologist decomposes
life-forms into genuses and species. A literary critic
decomposed a play into acts and scenes. A sommelier
decomposes a wine into color, viscosity, aroma, and
taste. In this chapter, as do the biologist, critic, and
sommelier, we decompose. Though for us, we decompose a
closed system into open sub-systems.

This may seem to conflict with the aim of this thesis, which
is to advance a theory of open systems. However, we still
recognize the value of closed systems. We just believe that
our ideas on open systems are useful for closed systems.

As mathematicians, we must bring rigor to our
decomposition. In this chapter, we do just that. We start
by formalizing closed systems as structured cospans with an
empty interface $ 0 \to x \gets 0 $. Then,
using the fine rewriting paradigm from Chapter
\ref{sec:fine-rewriting}, we place structured cospans into
the double category $ _L \FFFineRewrite $ as horizontal
1-arrows.  To decompose a closed system
\[
L0 \to x \gets L0
\]
is to write an arrow as a composite of arrows
\[
L0 \to x_1 \gets La_1 \to x_2 \gets La_2
\dotsm La_{n-1} \to x_n \gets L0
\]
We use such decompositions to prove our main result which states that two structured cospans
\[
L0 \to x \gets L0
\quad \text{and} \quad
L0 \to x' \gets L0
\]
are equivalent precisely when there is a square between
them.  We interpret this result in three ways.

\begin{enumerate}
\item It shows that the rewriting relation for a closed system
is functorial and is characterized using squares in a double
\item A closed system decomposes into open systems, and
simplifying each open system simplifies the composite
closed system.
\item Open systems provide a local perspective on the closed
perspective via this decomposition.
\end{enumerate}

There are two main thrusts to this proof.  The first
generalizes a classification of formal graph grammars given
by Ehrig, et.~al. [34]. This is
Theorem \ref{thm:production-same-rewrite-relation-as-discrete}.
Gadducci and Heckel proved this in the case of graphs
[35], but our result generalizes
this to structured cospans. Our proof mirrors theirs.

% =====================================================
\section{Expressiveness of underlying discrete grammars}
\label{sec:gen-result-graph-rewriting}
% =====================================================

As mentioned above, we want to decompose closed systems into
open systems.  We did not yet mention which open systems are
available to use. This depends on context.  That is,
whatever type of system one has, there is an appropriate
grammar stipulated by a theory that describes that
system. To illustrate, for an electrical system, a
corresponding grammar would have rules for adding resistors
in series, or adding the reciprocal of resistors in
parallel. Therefore, our starting data is a grammar
$ ( \X , P ) $---a topos $ \X $ and a set of fine rewrite
rules $ P \bydef \{ \ell_j \gets k_j \to r_j \} $---plus a
closed system $ x $ in $ \X $.  Eventually entering the
story is a topos $ \A $ of input types and an adjunction
between $ \A $ and $ \X $.  For now, however, we focus on the
set of rewrite rules $ P $.

We can prove the main result of this section, Theorem
\ref{thm:production-same-rewrite-relation-as-discrete}, by
controlling the form of the rewrite rules.  In particular,
we want the intermediary of the rules, the $ k_j $'s, to be
`discrete'. In what follows, we discuss what we mean by
`discrete' and show that the grammar obtained by
discretizing $ ( \X,P ) $ is just as expressive as
$ ( \X,P ) $, by which we mean that the induced rewriting
relations are equal. This result generalizes a
characterization of discrete \emph{graph grammars} given by
Ehrig, et.~al. \cite[Prop.~3.3]{ehrig_graph-grammars}.

Our concept of `discreteness' is borrowed from the flat
modality on a local topos. However, we avoid the lengthy
detour required to discuss the `flat modality' and a `local
topos'. The background does not add to our story, so we
point curious readers elsewhere
\cite[Ch.~C3.6]{johnstone_elephant}. By avoiding that
detour, we instead require the concept of a comonad, which
we present in Definition \ref{def:(co)monad}.

To start our discussion on discreteness, we define a
`discrete comonad'. The definition is straightforward enough,
but its purpose may seem alien at first. After the
definition, we explain its role in rewriting structured

\begin{definition}[Discrete comonad]
\label{def:discrete-comonad}
A comonad on a topos is called \defn{discrete} if its
counit is monic. We use $ \flat $ to denote a discrete comonad.
\end{definition}

Secretly, we have been working with a discrete comonad all
along. The adjunction
\[
\adjunction{\Set}{\RGraph}{L}{R}{4}
\]
induces the comonad $ LR $ on $ \RGraph $.  Applying $ LR $ to
a graph $ x $ returns the edgeless graph underlying $
x $, hence the term `discrete'. For example
\begin{center}
\begin{tikzpicture}
\begin{scope}
\node (a) at (0,2) {$ \bullet $};
\node (b) at (2,1) {$ \bullet $};
\node (c) at (0,0) {$ \bullet $};
\draw [graph]
(a) edge[] (b)
(a) edge[] (c)
(b) edge[] (c);
\draw [rounded corners] (-1,-1) rectangle (3,3);
\end{scope}
\begin{scope}[shift={(6,0)}]
\node (a) at (0,2) {$ \bullet $};
\node (b) at (2,1) {$ \bullet $};
\node (c) at (0,0) {$ \bullet $};
\draw [rounded corners] (-1,-1) rectangle (3,3);
\end{scope}
\draw [|->] (3.5,1) to node[above]{$ LR $} (4.5,1);
\end{tikzpicture}
\end{center}
The counit $ \epsilon_x \from LRx \to x $ of the comonad
$ LR $ includes the underlying edgeless graph $ LRx $ into
the original graph $ x $. For example
\begin{center}
\begin{tikzpicture}
\begin{scope}
\node (a) at (0,2) {$ \bullet $};
\node (b) at (2,1) {$ \bullet $};
\node (c) at (0,0) {$ \bullet $};
\draw [rounded corners] (-1,-1) rectangle (3,3);
\end{scope}
\begin{scope}[shift={(6,0)}]
\node (a) at (0,2) {$ \bullet $};
\node (b) at (2,1) {$ \bullet $};
\node (c) at (0,0) {$ \bullet $};
\draw [graph]
(a) edge[] (b)
(a) edge[] (c)
(b) edge[] (c);
\draw [rounded corners] (-1,-1) rectangle (3,3);
\end{scope}
\draw [->]
(3.5,1) to node[above]{$ \epsilon $} (4.5,1);
\end{tikzpicture}
\end{center}

Abstractly, this inclusion is why we ask for the counit to be monic. The
property we capture with a discrete comonad comes from the
systems interpretation of the adjunctions
\[
\adjunction{\A}{\X}{L}{R}{2}
\]
between topoi. That is, $ R $ takes a system $ x $,
identifies the largest sub-system that can serve as an
interface and turns that sub-system into an interface type
$ Rx $. Then $ L $ takes that interface type and turns it
back into a system $ LRx $. This process effectively strips
away every part of a system leaving only those parts that
can connect to the outside world. That means $ LRx $ is a
part of $ x $ or, in the parlance of category theory,
$ LRx $ is a subobject of $ x $.  Hence, we ask for a monic

How do we plan to use discrete comonads?  We use them to
control the form of our grammars.  In general, a rewrite
rule has form
\[
\ell \gets k \to r
\]
where there are no restrictions on what $ k $ can be.
However, recall that $ k $ identifies the part of $ \ell $
that is fixed throughout the rewrite. It does not direct how
the rewrite is performed.  Therefore, we can deform it a bit
without changing the outcome of the applying the rewrite.
In particular, we can discretize it by replacing $ k $ with
$ \flat k $.  And because $ \flat $ has a monic counit, we
can insert $ \flat k $ right into the middle of the
fine rewrite rule.

\begin{definition}[Discrete grammar]
Given a grammar $ ( \X , P ) $, define the set $ P_\flat $
as consisting of the rules
\[
\ell \gets k \gets \flat k \to k \to r
\]
for each rule $ \ell \gets k \to r $ in $ P $. We call $
( X , P_\flat ) $ the \defn{discrete grammar} underlying $
( \X, P ) $.
\end{definition}

Discrete grammars are easier to work with than arbitrary
grammars. So when given an opportunity to work with a
discrete grammar instead of a non-discrete grammar, we
should take it. Theorem
\ref{thm:production-same-rewrite-relation-as-discrete} gives
a sufficient condition that allows us to swap $ ( \X,P ) $
for $ ( \X,P_\flat ) $ without consequence. To prove this,
however, we borrow from lattice theory which requires that
we make a brief turn to fill in some required background.

\begin{definition}[Lattice]
A lattice is a poset $ ( S, \leq ) $ equipped with all
finite joins $ \bigvee $ and all finite meets
$ \bigwedge $. It follows that there is a minimal element
and maximal element, realized as the empty meet and join
respectively, which we denote by $ 0 $ and $ 1 $.
\end{definition}

Joins and meets are also known as suprema and infima. We are
using the definition of a lattice common in the category
theory literature. This leaves out objects that some
mathematicians might consider lattices. Below we give one
counter-example and several examples of lattices, the last
one being the most relevant.

\begin{example}[Integer Lattice]
The integers with the usual ordering $ \leq $ do not form
a lattice because there is no minimal or maximal element.
\end{example}

\begin{example}[Lattice of power sets]
For any set $ S $, its powerset $ \mathcal{P}S $ is a
poset via subset inclusion. The powerset becomes a lattice
by taking join to be union $ a \vee b \bydef a \cup b $,
and meet to be intersection $ a \wedge b \bydef a \cap b
$. In general, union and intersection are defined over
arbitrary sets, thus realizing arbitrary joins
$ \bigvee a_\alpha $ and arbitrary meets
$ \bigwedge a_\alpha $.
\end{example}

Those few examples provide intuition about lattices, but the
next example is the most important lattice for us. It is the
mechanism by which the power set is generalized into topos
theory. It is called the subobject lattice.

\begin{example}[Subobject lattice]
Let $ \T $ be a topos and $ t $ be an object. There is a
lattice $ \Sub (t) $ called the subobject lattice of
$ t $.  The elements of $ \Sub (t) $ are called subobjects.
They are isomorphism classes of monomorphisms into $ t
$. Here, two monomorphisms $ f,g $ into $ t $ are isomorphic if
there is a commuting diagram
\begin{center}
\begin{tikzpicture}
\node (a) at (-1,2) {$ a $};
\node (b) at (1,2) {$ b $};
\node (t) at (0,0) {$ t $};
\draw [cd]
(a) edge[] node[left]{$ f $} (t)
(b) edge[] node[right]{$ g $} (t)
(a) edge[] node[above]{$ \iso $} (b);
\end{tikzpicture}
\end{center}
The order on $ \Sub (t) $ is given by $ f \leq g $ if
$ f $ factors through $ g $, meaning there is an arrow
$ h \from a \to b $ such that $ f = gh $. Note that $ h $
is necessarily monic. The meet operation in $ \Sub (t) $ is given by
\begin{center}
\begin{tikzpicture}
\node (ab) at (0,2) {$ a \vee b $};
\node (a)  at (0,0) {$ a $};
\node (b)  at (2,2) {$ b $};
\node (t)  at (2,0) {$ t $};
\draw [cd]
(ab) edge[] (a)
(ab) edge[] (b)
(a)  edge[] (t)
(b)  edge[] (t);
\draw [->,dashed] (ab) edge (t) ;
\draw (0.3,1.6) -- (0.4,1.6) -- (0.4,1.7);
\end{tikzpicture}
\end{center}
and join is given by pushout over the meet
\begin{center}
\begin{tikzpicture}
\node (ab) at (0,2) {$ a \vee b $};
\node (a)  at (0,0) {$ a $};
\node (b)  at (2,2) {$ b $};
\node (t)  at (2,0) {$ a \wedge b $};
\node (tt) at (4,-2) {$ t $};
\draw [cd]
(ab) edge[]           (a)
(ab) edge[]           (b)
(a)  edge[]           (t)
(b)  edge[]           (t)
(a)  edge[bend right] (tt)
(b)  edge[bend left]  (tt);
\draw [->,dashed] (t) edge (tt) ;
\draw (1.7,0.4) -- (1.6,0.4) -- (1.6,0.3);
\end{tikzpicture}
\end{center}
\end{example}

We use subobject lattices to characterize which grammars are
as expressive as their underlying discrete grammars. To do
this, we require subobject lattices with arbitrary meets.  The
powerset lattice mentioned above has this property, but
when do subobject lattices have this property?  Here are
several sufficient conditions, starting with a well-known
result coming from the domain of order theory.

\begin{proposition} \label{thm:lattice-alljoins-allmeets}
Any lattice that has all joins also has all meets.
\end{proposition}

\begin{proof}
Consider a subset $ S $ of a lattice. Define the meet of $
S $ to be the join of the set of all lower bounds of $ S $.
\end{proof}

\begin{proposition} \label{thm:subob-arbitrary-meets}
Consider a topos $ \T $ and object $ t $.  The subobject
lattice $ \Sub (t) $ has arbitrary meets when the over
category $ T \downarrow t $ has all products.
\end{proposition}

\begin{proof}
Because $ T \downarrow t $ is a topos, it has
equalizers. Thus giving it all products ensures the
existence of all limits, hence meets.
\end{proof}

\begin{corollary}
Consider a topos $ \T $ and object $ t $.  The subobject
lattice $ \Sub (t) $ has arbitrary meets when the over
category $ T \downarrow t $ has all coproducts.
\end{corollary}

\begin{proof}
Combine Propositions \ref{thm:lattice-alljoins-allmeets}
and \ref{thm:subob-arbitrary-meets}.
\end{proof}

\begin{corollary}
Consider a presheaf category $ \Set^{ \C^{\op} } $ on a
small category $ \C $. For any presheaf $ x $,
$ \Sub (x) $ has all meets.
\end{corollary}

\begin{proof}
The category $ \Set^{ \C^{\op} } \downarrow x $ of
presheaves over $ x $ is again a presheaf category by
Theorem \ref{thm:presheaf-slice-is-presheaf} so has all
\end{proof}

At last, we combine the discrete comonad, the discrete
grammar, and the complete subobject lattice into a result on
the expressiveness on discrete grammars.

\begin{theorem}
\label{thm:production-same-rewrite-relation-as-discrete}
Let $ \T $ be a topos and $ \flat \from \T \to \T $ be a
discrete comonad.  Let $ ( \T , P ) $ be a grammar such
that for every rule $ \ell \gets k \to r $ in $ P $, the
subobject lattice $ \Sub (k) $ has all meets. Then the
rewriting relation for $ ( \T , P ) $ equals the
rewriting relation for the underlying discrete grammar
$ ( \T,P_\flat ) $.
\end{theorem}

\begin{proof}
Suppose that $ ( \T,P ) $ induces $ \dderiv{g}{h} $. That
means there exists a rule $ \spn{\ell}{k}{r} $ in $ P $
and a derivation
\begin{equation} \label{eq:prod-rewrite-1}
\begin{tikzpicture}
\node (1t) at (0,2) {$ \ell $};
\node (2t) at (2,2) {$ k $};
\node (3t) at (4,2) {$ r $};
\node (1b) at (0,0) {$ g $};
\node (2b) at (2,0) {$ d $};
\node (3b) at (4,0) {$ h $};
\draw [cd]
(2t) edge (1t)
(2t) edge (3t)
(2b) edge (1b)
(2b) edge (3b)
(1t) edge (1b)
(2t) edge (2b)
(3t) edge (3b);
\draw (0.3,0.4) -- (0.4,0.4) -- (0.4,0.3);
\draw (3.7,0.4) -- (3.6,0.4) -- (3.6,0.3);
\end{tikzpicture}
\end{equation}
we can achieve that same derivation using rules in
$ P_\flat $. This requires we build a pushout complement
$ w $ of the diagram
\begin{center}
\begin{tikzpicture}
\node (k) at (0,2) {$ k $};
\node (bk) at (2,2) {$ \flat k $};
\node (d) at (0,0) {$ d $};
\draw [cd]
(bk) edge[] node[above]{$ \epsilon $} (k)
(k) edge[] (d);
\end{tikzpicture}
\end{center}
\[
w \coloneqq
\bigwedge \{ z \colon z \vee k = d \} \vee
\flat k,
\]
This comes with inclusions $ \flat k \to w $ and
$ w \to d $. This $ w $ exists because $ \Sub (k) $ has
all meets.  Note that $ w \vee k = d $ and
$ w \wedge k = \flat k $ which means that
\begin{center}
\begin{tikzpicture}
\node (k) at (0,2) {$ k $};
\node (bk) at (2,2) {$ \flat k $};
\node (d) at (0,0) {$ d $};
\node (w) at (2,0) {$ w $};
\draw [cd]
(bk) edge[] (k)
(bk) edge[] (w)
(k) edge[] (d)
(w) edge[] (d);
\draw (0.3,0.4) -- (0.4,0.4) -- (0.4,0.3);
\end{tikzpicture}
\end{center}
is a pushout. It follows that there is a derivation
\begin{equation} \label{eq:prod-rewrite-2}
\begin{tikzpicture}
\node (01) at (0,2) {$ \ell $};
\node (11) at (2,2) {$ k $};
\node (21) at (4,2) {$ \flat k $};
\node (31) at (6,2) {$ k $};
\node (41) at (8,2) {$ r $};
\node (00) at (0,0) {$ g $};
\node (10) at (2,0) {$ d $};
\node (20) at (4,0) {$ w $};
\node (30) at (6,0) {$ d $};
\node (40) at (8,0) {$ h $};
\draw [cd] (11) to node [] {\scriptsize{$  $}} (01);
\draw [cd] (21) to node [] {\scriptsize{$  $}} (11);
\draw [cd] (21) to node [] {\scriptsize{$  $}} (31);
\draw [cd] (31) to node [] {\scriptsize{$  $}} (41);
\draw [cd] (10) to node [] {\scriptsize{$  $}} (00);
\draw [cd] (20) to node [] {\scriptsize{$  $}} (10);
\draw [cd] (20) to node [] {\scriptsize{$  $}} (30);
\draw [cd] (30) to node [] {\scriptsize{$  $}} (40);
\draw [cd] (01) to node [] {\scriptsize{$  $}} (00);
\draw [cd] (11) to node [] {\scriptsize{$  $}} (10);
\draw [cd] (21) to node [] {\scriptsize{$  $}} (20);
\draw [cd] (31) to node [] {\scriptsize{$  $}} (30);
\draw [cd] (41) to node [] {\scriptsize{$  $}} (40);
\draw (0.3,0.4) -- (0.4,0.4) -- (0.4,0.3);
\draw (2.3,0.4) -- (2.4,0.4) -- (2.4,0.3);
\draw (5.7,0.4) -- (5.6,0.4) -- (5.6,0.3);
\draw (7.7,0.4) -- (7.6,0.4) -- (7.6,0.3);
\end{tikzpicture}
\end{equation}
with respect to $ P_\flat $ because, the top row is a rule in
$ P_\flat $.  Therefore, $ \dderiv{g}{h} $ via $ P $ in
Diagram \eqref{eq:prod-rewrite-1} implies that
$ \deriv{g}{h} $ via $ P_\flat $ as shown in Diagram
\eqref{eq:prod-rewrite-2}.

For the other direction, suppose $ \dderiv{g}{h} $ via $
P_\flat $, giving a derivation
\begin{equation}
\label{eq:prod-rewrite-3}
\begin{tikzpicture}
\node (1t) at (0,2) {$ \ell $};
\node (2t) at (2,2) {$ \flat k $};
\node (3t) at (4,2) {$ r $};
\node (1b) at (0,0) {$ g $};
\node (2b) at (2,0) {$ d $};
\node (3b) at (4,0) {$ h $};
\draw [cd]
(2t) edge                          (1t)
(2t) edge                          (3t)
(2b) edge node[below]{$ \psi $}    (1b)
(2b) edge                          (3b)
(1t) edge node[left]{$ m $}        (1b)
(2t) edge node[left]{$ \theta $}   (2b)
(3t) edge node[right]{$ m' $}      (3b);
\draw (0.3,0.4) -- (0.4,0.4) -- (0.4,0.3);
\draw (3.7,0.4) -- (3.6,0.4) -- (3.6,0.3);
\end{tikzpicture}
\end{equation}
By construction of $ P_\flat $, the rule
$ \spn{\ell}{\flat k}{r} $ in $ P_\flat $ was induced from a
\[
\ell \xgets{\tau} k \to r
\]
in $ P $, meaning that the map $ \flat k \to \ell $ factors
through $ \tau $. Next, define $ d' $ to be the pushout of the diagram
\begin{center}
\begin{tikzpicture}
\node (flatk) at (0,2) {$ \flat k $};
\node (k)     at (2,2) {$ k $};
\node (d)     at (0,0) {$ d $};
\node (d')    at (2,0) {$ d' $};
\draw [cd]
(flatk) edge[] node[above]{$ \epsilon $}       (k)
(flatk) edge[] node[left]{$ \theta $}          (d)
(d)     edge[] node[below]{$ \hat{\epsilon} $} (d')
(k)     edge[] node[right]{$ \hat{\theta} $}   (d');
\draw (1.7,0.4) -- (1.6,0.4) -- (1.6,0.3);
\end{tikzpicture}
\end{center}
By invoking the universal property of this pushout with the
\[
\psi \from d \to g
\quad \text{and} \quad
m \tau \from k \to \ell \to g,
\]
we get a canonical map $ d' \to g $ that we can fit into a
commuting diagram
\begin{center}
\begin{tikzpicture}
\node (l) at (0,2) {$ \ell $};
\node (g) at (0,0) {$ g $};
\node (k) at (2,2) {$ k $};
\node (d') at (2,0) {$ d' $};
\node (flatk) at (1,3) {$ \flat k $};
\node (d) at (1,1) {$ d $};
\draw [cd]
(flatk) edge[] (l)
(flatk) edge[] node[right]{$ \epsilon $} (k)
(flatk) edge[] node[left,pos=0.7]{$ \theta $} (d)
(d) edge[] node[below,pos=0.3]{$ \psi $}     (g)
(d) edge[] node[below,pos=0.3]{$ \hat{\epsilon} $} (d')
(l) edge[] node[left]{$ m $} (g)
(k) edge[] node[right]{$ \hat{\theta} $} (d')
(d') edge[] (g);
\draw [white,line width=0.5em] (k) -- (l);
\draw [cd] (k) to node[above,pos=0.3]{$ \tau $} (l);
\draw (0.2,0.6) -- (0.3,0.7) -- (0.3,0.6);
\draw (1.8,0.6) -- (1.7,0.7) -- (1.7,0.6);
\end{tikzpicture}
\end{center}
whose back faces are pushouts. Using a standard diagram
chasing argument, we can show that the front face is also a
pushout.  Similarly, the square
\begin{center}
\begin{tikzpicture}
\node (k) at (0,2) {$ k $};
\node (r) at (2,2) {$ r $};
\node (d') at (0,0) {$ d' $};
\node (h) at (2,0) {$ h $};
\draw [cd]
(k) edge[] (r)
(k) edge[] (d')
(d') edge[] (h)
(r) edge[] (h);
\draw (1.7,0.4) -- (1.6,0.4) -- (1.6,0.3);
\end{tikzpicture}
\end{center}
is a pushout.  Sticking these two pushouts together
\begin{center}
\begin{tikzpicture}
\node (1t) at (0,2) {$ \ell $};
\node (2t) at (2,2) {$ k $};
\node (3t) at (4,2) {$ r $};
\node (1b) at (0,0) {$ g $};
\node (2b) at (2,0) {$ d' $};
\node (3b) at (4,0) {$ h $};
\draw [cd]
(2t) edge                     (1t)
(2t) edge                     (3t)
(2b) edge                     (1b)
(2b) edge                     (3b)
(1t) edge node[left]{$ m $}   (1b)
(2t) edge node[left]{$ f $}   (2b)
(3t) edge node[right]{$ m' $} (3b);
\draw (0.3,0.4) -- (0.4,0.4) -- (0.4,0.3);
\draw (3.7,0.4) -- (3.6,0.4) -- (3.6,0.3);
\end{tikzpicture}
\end{center}
shows that $ \dderiv{g}{h} $ arises from $ P $.

Because the relation $ \dderiv{}{} $ is the same for
$ P $ and $ P_\flat $, it follows that $ \deriv{}{} $ is
also the same as claimed.
\end{proof}

% ===========================================
\section{Rewriting structured cospans}
\label{sec:Rewriting-StrCsp}
% ===========================================

Equipped with knowledge about when grammars and their
underlying discrete grammars generate the same rewriting
relation, we continue towards goal of decomposing closed
systems. First, we revisit Section \ref{sec:rewriting-topoi}
to get some facts about grammars. We then obtain the
language associated to a grammar in a functorial
way. Finally, we show how to decompose into open subsystems a given system
equipped with a grammar.

Recall the category $ \Gram $.  The objects of $ \Gram $ are
pairs $ ( \T , P ) $ where $ \T $ is a topos and $ P $ is a
set of rewrite rules in $ \T $.  The arrows
$ (\T , P) \to ( \T' , P' )$ of $ \Gram $ are
rule-preserving functors $ \T \to \T' $.  Our interest now lies
in the full subcategory of structured cospan grammars
$ \StrCspGram $ whose objects are the grammars of form
$ ( _L \StrCsp , P ) $ where $ P $ consists of fine rewrites
of structured cospans, meaning they have the form
\begin{center}
\begin{tikzpicture}
\begin{scope}
\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' \)};
\draw [cd] (1) to (2);
\draw [cd] (3) to (2);
\draw [cd] (4) to (5);
\draw [cd] (6) to (5);
\draw [cd] (7) to (8);
\draw [cd] (9) to (8);
\draw [cd] (4) to node[left]{\( \iso \)} (1);
\draw [cd] (4) to node[left]{\( \iso \)} (7);
\draw [cd,>->] (5) to (2);
\draw [cd,>->] (5) to (8);
\draw [cd] (6) to node[right]{\( \iso \)} (3);
\draw [cd] (6) to node[right]{\( \iso \)} (9);
\end{scope}
\end{tikzpicture}
\end{center}
and the left adjoint $ L $ has a monic counit.

It is on this category $ \StrCspGram $ that we define a
functor encoding the rewrite relation to each grammar. We
denote this functor
\[
\Lang \from \StrCspGram \to \DblCat
\]
where $ \Lang $ is short for `language'. This is an
appropriate term as this functor provides \emph{(i)} the
terms formed by connecting together open systems (instead
of, in linguistics, concatenating units of syntax) and
\emph{(ii)} the rules governing how to interchange open
systems (instead of parts of speech). To help visualize
this, we sketch a simple example.

\begin{example}

Start with the, by now familiar, adjunction
\[
\adjunction{\Set}{\RGraph}{L}{R}{4}
\]
For this $ L $, $ _L \StrCsp $ is the category of open
graphs.  Make a grammar from $ _L \StrCsp $ by defining a
$ P $ to have the single rule
\begin{center}
\begin{tikzpicture}
\begin{scope}[shift={(0,0)}] % up left
\node () at (0,0) {$ \bullet $};
\draw [rounded corners] (-1,-1) rectangle (1,1);
\node (00r) at (1.1,0) {};
\node (00b) at (0,-1.1) {};
\end{scope}
\begin{scope}[shift={(3,0)}] % up mid
\node (a) at (0,0) {$ \bullet $};
\draw [graph]
(a) edge[loop above] (a);
\draw [rounded corners] (-1,-1) rectangle (1,1);
\node (01l) at (-1.1,0) {};
\node (01r) at (1.1,0)  {};
\node (01b) at (0,-1.1) {};
\end{scope}
\begin{scope}[shift={(6,0)}] % up right
\node () at (0,0) {$ \bullet $};
\draw [rounded corners] (-1,-1) rectangle (1,1);
\node (02l) at (-1.1,0) {};
\node (02b) at (0,-1.1) {};
\end{scope}
% ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
\begin{scope}[shift={(0,-3)}] % mid left
\node () at (0,0) {$ \bullet $};
\draw [rounded corners] (-1,-1) rectangle (1,1);
\node (10t) at (0,1.1)   {};
\node (10r) at (1.1,0) {};
\node (10b) at (0,-1.1)  {};
\end{scope}
\begin{scope}[shift={(3,-3)}] % mid mid
\node (a) at (0,0) {$ \bullet $};
\draw [rounded corners] (-1,-1) rectangle (1,1);
\node (11l) at (-1.1,0) {};
\node (11r) at (1.1,0)  {};
\node (11t) at (0,1.1)  {};
\node (11b) at (0,-1.1) {};
\end{scope}
\begin{scope}[shift={(6,-3)}] % mid right
\node () at (0,0) {$ \bullet $};
\draw [rounded corners] (-1,-1) rectangle (1,1);
\node (12l) at (-1.1,0) {};
\node (12t) at (0,1.1)    {};
\node (12b) at (0,-1.1)   {};
\end{scope}
% ~~~~~~~~~~~~~~~~~~~~~
\begin{scope}[shift={(0,-6)}] % down left
\node () at (0,0) {$ \bullet $};
\draw [rounded corners] (-1,-1) rectangle (1,1);
\node (20t) at (0,1.1)   {};
\node (20r) at (1.1,0) {};
\node (20b) at (0,-1.1)  {};
\end{scope}
\begin{scope}[shift={(3,-6)}] % down mid
\node (a) at (0,0) {$ \bullet $};
\draw [rounded corners] (-1,-1) rectangle (1,1);
\node (21l) at (-1.1,0) {};
\node (21r) at (1.1,0)  {};
\node (21t) at (0,1.1)  {};
\node (21b) at (0,-1.1) {};
\end{scope}
\begin{scope}[shift={(6,-6)}] % down right
\node () at (0,0) {$ \bullet $};
\draw [rounded corners]
(-1,-1) rectangle (1,1);
\node (22l) at (-1.1,0) {};
\node (22r) at (1.1,0)  {};
\node (22t) at (0,1.1)  {};
\node (22b) at (0,-1.1) {};
\end{scope}
% ~~~~~~~~~~~~~~~~~~~
\path[cd]
(00r) edge (01l)
(02l) edge (01r)
(10r) edge (11l)
(12l) edge (11r)
(20r) edge (21l)
(22l) edge (21r)
(00b) edge (10t)
(20t) edge (10b)
(01b) edge (11t)
(21t) edge (11b)
(02b) edge (12t)
(22t) edge (12b);
\end{tikzpicture}
\end{center}
The language associated to this grammar consists of all
open graphs. The rewrite relation says $ \deriv{g}{h} $ if
we obtain $ h $ be removing loops from $ g $. We
illustrate this with the following square in the double
category $ \Lang ( _L \StrCsp , P ) $.
\begin{center}
\begin{tikzpicture}
\begin{scope}[shift={(0,0)}] % up left
\node (a) at (0,-1) {$ \bullet $};
\node (b) at (0,1) {$ \bullet $};
\draw [rounded corners] (-2,-2) rectangle (2,2);
\node (00r) at (2.1,0) {};
\node (00b) at (0,-2.1) {};
\end{scope}
\begin{scope}[shift={(5,0)}] % up mid
\node (a) at (-1,-1) {$ \bullet $};
\node (b) at (-1,1) {$ \bullet $};
\node (c) at (0,0) {$ \bullet $};
\node (d) at (1,0) {$ \bullet $};
\draw [graph]
(b) edge[loop above] (b)
(c) edge[loop above] (c)
(a) edge[] (c)
(b) edge[] (c)
(c) edge[] (d);
\draw [rounded corners] (-2,-2) rectangle (2,2);
\node (01l) at (-2.1,0) {};
\node (01r) at (2.1,0)  {};
\node (01b) at (0,-2.1) {};
\end{scope}
\begin{scope}[shift={(10,0)}] % up right
\node () at (0,0) {$ \bullet $};
\draw [rounded corners] (-2,-2) rectangle (2,2);
\node (02l) at (-2.1,0) {};
\node (02b) at (0,-2.1) {};
\end{scope}
% ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
\begin{scope}[shift={(0,-5)}] % mid left
\node () at (0,-1) {$ \bullet $};
\node () at (0,1) {$ \bullet $};
\draw [rounded corners] (-2,-2) rectangle (2,2);
\node (10t) at (0,2.1)   {};
\node (10r) at (2.1,0) {};
\node (10b) at (0,-2.1)  {};
\end{scope}
\begin{scope}[shift={(5,-5)}] % mid mid
\node (a) at (-1,-1) {$ \bullet $};
\node (b) at (-1,1) {$ \bullet $};
\node (d) at (1,0) {$ \bullet $};
\draw [rounded corners] (-2,-2) rectangle (2,2);
\node (11l) at (-2.1,0) {};
\node (11r) at (2.1,0)  {};
\node (11t) at (0,2.1)  {};
\node (11b) at (0,-2.1) {};
\end{scope}
\begin{scope}[shift={(10,-5)}] % mid right
\node () at (0,0) {$ \bullet $};
\draw [rounded corners] (-2,-2) rectangle (2,2);
\node (12l) at (-2.1,0) {};
\node (12t) at (0,2.1)    {};
\node (12b) at (0,-2.1)   {};
\end{scope}
% ~~~~~~~~~~~~~~~~~~~~~
\begin{scope}[shift={(0,-10)}] % down left
\node () at (0,-1) {$ \bullet $};
\node () at (0,1) {$ \bullet $};
\draw [rounded corners] (-2,-2) rectangle (2,2);
\node (20t) at (0,2.1)   {};
\node (20r) at (2.1,0) {};
\node (20b) at (0,-2.1)  {};
\end{scope}
\begin{scope}[shift={(5,-10)}] % down mid
\node (a) at (-1,-1) {$ \bullet $};
\node (b) at (-1,1) {$ \bullet $};
\node (c) at (0,0) {$ \bullet $};
\node (d) at (1,0) {$ \bullet $};
\draw [graph]
(a) edge[] (c)
(b) edge[] (c)
(c) edge[] (d);
\draw [rounded corners] (-2,-2) rectangle (2,2);
\node (21l) at (-2.1,0) {};
\node (21r) at (2.1,0)  {};
\node (21t) at (0,2.1)  {};
\node (21b) at (0,-2.1) {};
\end{scope}
\begin{scope}[shift={(10,-10)}] % down right
\node () at (0,0) {$ \bullet $};
\draw [rounded corners] (-2,-2) rectangle (2,2);
\node (22l) at (-2.1,0) {};
\node (22r) at (2.1,0)  {};
\node (22t) at (0,2.1)  {};
\node (22b) at (0,-2.1) {};
\end{scope}
% ~~~~~~~~~~~~~~~~~~~
\path[cd]
(00r) edge (01l)
(02l) edge (01r)
(10r) edge (11l)
(12l) edge (11r)
(20r) edge (21l)
(22l) edge (21r)
(00b) edge (10t)
(20t) edge (10b)
(01b) edge (11t)
(21t) edge (11b)
(02b) edge (12t)
(22t) edge (12b);
\end{tikzpicture}
\end{center}
\end{example}

To actually construct $ \Lang $, we use functors
$ D \from \StrCspGram \to \StrCspGram $ and
$ S \from \StrCspGram \to \DblCat $. Roughly, $ D $ sends a
grammar $ ( _L \StrCsp , P ) $ to all of the rewrite rules
derived from $ P $ and $ S $ generates a double category on
the squares obtained from the rewrite rules of a grammar
$ ( _L \StrCsp , P ) $. In this way, we get the language of
a grammar as a double category where the squares are the
rewrite rules.  The next lemma defines $ D $ and gives some
of its properties.

\begin{lemma}
There is an idempotent functor
$ D \from \StrCspGram \to \StrCspGram $ defined as
follows. On objects define $ D ( _{L}\StrCsp , P ) $ to be
the grammar $ ( _{L} \StrCsp , P_D) $, where $ P_D $
consists of all rules $ \spn{g}{h}{d} $ witnessing the
relation $ \dderiv{g}{h} $ with respect to
$ ( _{L}\StrCsp , P ) $. On arrows, define
$ DF \from D( _{L}\StrCsp , P ) \to D( _{L'}\StrCsp , Q )
$ to be $ F $.  Moreover, the identity on $ \StrCspGram $
is a subfunctor of $ D $.
\end{lemma}

\begin{proof}
That $ D ( _{L}\StrCsp , P ) $ actually gives a grammar
follows from the fact that pushouts respect monics in a
topos \cite[Lem.~12]{lack-sobo_adhesive-cats}.

To show that $ \D $ is idempotent, we show that for any
grammar $ ( _{L}\StrCsp , P ) $, we have
$ D ( _{L}\StrCsp , P ) = DD ( _{L}\StrCsp , P ) $.  Rules
in $ DD ( _{L}\StrCsp , P ) $ appear in the bottom row of a
double pushout diagram whose top row is a rule in
$ D ( _{L}\StrCsp , P ) $, which in turn is the bottom row
of a double pushout diagram whose top row is in
$ ( _{L}\StrCsp , P ) $. Thus, a rule in
$ DD ( _{L}\StrCsp , P ) $ is the bottom row of a double
pushout diagram whose top row is in
$ ( _{L}\StrCsp , P ) $. See Figure \ref{fig:idempotentD}.

\begin{figure}[h]
\centering
\fbox{
\begin{minipage}{\linewidth}
\vspace{2em}
\[
\begin{tikzpicture}
\node (1) at (0,4) {$ g $};
\node (2) at (2,4) {$ d $};
\node (3) at (4,4) {$ h $};
\node (4) at (0,2) {$ g' $};
\node (5) at (2,2) {$ d' $};
\node (6) at (4,2) {$ h' $};
\node (7) at (0,0) {$ g'' $};
\node (8) at (2,0) {$ d'' $};
\node (9) at (4,0) {$ h'' $};
\draw [cd] (2) to node [] {\scriptsize{$  $}} (1);
\draw [cd] (2) to node [] {\scriptsize{$  $}} (3);
\draw [cd] (5) to node [] {\scriptsize{$  $}} (4);
\draw [cd] (5) to node [] {\scriptsize{$  $}} (6);
\draw [cd] (8) to node [] {\scriptsize{$  $}} (7);
\draw [cd] (8) to node [] {\scriptsize{$  $}} (9);
\draw [cd] (1) to node [] {\scriptsize{$  $}} (4);
\draw [cd] (2) to node [] {\scriptsize{$  $}} (5);
\draw [cd] (3) to node [] {\scriptsize{$  $}} (6);
\draw [cd] (4) to node [] {\scriptsize{$  $}} (7);
\draw [cd] (5) to node [] {\scriptsize{$  $}} (8);
\draw [cd] (6) to node [] {\scriptsize{$  $}} (9);
\draw (0.3,0.4) -- (0.4,0.4) -- (0.4,0.3);
\draw (3.7,0.4) -- (3.6,0.4) -- (3.6,0.3);
\draw (0.3,2.4) -- (0.4,2.4) -- (0.4,2.3);
\draw (3.7,2.4) -- (3.6,2.4) -- (3.6,2.3);
\end{tikzpicture}
\]
\caption{Stacked double pushout diagrams}
\label{fig:idempotentD}
\end{minipage}
\end{figure}

The identity is a subfunctor of $ D $ because
$ \dderiv{\ell}{r} $ for any production
$ \spn{\ell}{k}{r} $ in $ ( _{L}\StrCsp , P ) $ via a
triple of identity arrows. Hence there is a monomorphism
\[
( _L \StrCsp , P ) \to
D ( _L \StrCsp , P )
\]
induced from the identity functor on $ _L\StrCsp $.
\end{proof}

In this lemma, we have created a functor $ D $ that sends a
grammar to a new grammar consisting of
all derived rules.  That $ D $ is idempotent means that all
rules derived from $ P $ can be derived directly; multiple
applications of $ D $ are unnecessary.  That the identity is
a subfunctor of $ D $ means that set of the derived rules
$ P_D $ contains the set of initial rules $ P $.

The next stage in defining $ \Lang $ is to define
$ S \from \StrCspGram \to \DblCat $. On objects, let
$ S ( _L \StrCsp , P ) $ be the sub-double category of
$ _L \SSStrCsp $ generated by the rules in $ P $ considered
as squares.  On arrows, $ S $ sends
\[
F \from ( _{L}\StrCsp , P ) \to ( _{L'} \StrCsp , P' )
\]
to the double functor defined that extends the mapping
between the generators of $ S ( _{L}\StrCsp , P ) $ and
$ S ( _{L'}\StrCsp , P' ) $.  This preserves composition because
$ F $ preserves pullbacks and pushouts.

\begin{definition}(Language of a grammar)
The \defn{language functor} is defined to be
$ \Lang \coloneqq SD $.
\end{definition}

To witness the rewriting relation on a closed system as a
square in a double category, we require this next lemma
that formalizes the analogy between rewriting the disjoint
union of systems and tensoring squares.

\begin{lemma} \label{thm:rewrite-rel-is-additive}
If $ \deriv{x}{y} $ and $ \deriv{x'}{y'} $, then
$ \deriv{x+x'}{y+y'} $
\end{lemma}

\begin{proof}
If the derivation $ \deriv{x}{y} $ comes from a string of
double pushout diagrams
\begin{center}
\begin{tikzpicture}[scale=0.8]
\node (1t) at (0,2) {$ \ell_1 $};
\node (2t) at (2,2) {$ k_1 $};
\node (3t) at (4,2) {$ r_1 $};
\node (4t) at (6,2) {$ \ell_2 $};
\node (5t) at (8,2) {$ k_2 $};
\node (6t) at (10,2) {$ r_2 $};
\node (7t) at (11,2) {$ \ell_n $};
\node (8t) at (13,2) {$ k_n $};
\node (9t) at (15,2) {$ r_n $};
\node (1b) at (0,0) {$ x $};
\node (2b) at (2,0) {$ d_1 $};
\node (3b) at (5,0) {$ w_1 $};
\node (4b) at (8,0) {$ d_2 $};
\node (5b) at (10,0) {$ w_2 $};
\node (6b) at (11,0) {$ w_{n-1} $};
\node (7b) at (13,0) {$ d_n $};
\node (8b) at (15,0) {$ y $};
\draw [cd] (2t) to node [] {\scriptsize{$  $}} (1t);
\draw [cd] (2t) to node [] {\scriptsize{$  $}} (3t);
\draw [cd] (5t) to node [] {\scriptsize{$  $}} (4t);
\draw [cd] (5t) to node [] {\scriptsize{$  $}} (6t);
\draw [cd] (8t) to node [] {\scriptsize{$  $}} (7t);
\draw [cd] (8t) to node [] {\scriptsize{$  $}} (9t);
\draw [cd] (2b) to node [] {\scriptsize{$  $}} (1b);
\draw [cd] (2b) to node [] {\scriptsize{$  $}} (3b);
\draw [cd] (4b) to node [] {\scriptsize{$  $}} (3b);
\draw [cd] (4b) to node [] {\scriptsize{$  $}} (5b);
\draw [cd] (7b) to node [] {\scriptsize{$  $}} (6b);
\draw [cd] (7b) to node [] {\scriptsize{$  $}} (8b);
\draw [cd] (1t) to node [] {\scriptsize{$  $}} (1b);
\draw [cd] (2t) to node [] {\scriptsize{$  $}} (2b);
\draw [cd] (3t) to node [] {\scriptsize{$  $}} (3b);
\draw [cd] (4t) to node [] {\scriptsize{$  $}} (3b);
\draw [cd] (5t) to node [] {\scriptsize{$  $}} (4b);
\draw [cd] (6t) to node [] {\scriptsize{$  $}} (5b);
\draw [cd] (7t) to node [] {\scriptsize{$  $}} (6b);
\draw [cd] (8t) to node [] {\scriptsize{$  $}} (7b);
\draw [cd] (9t) to node [] {\scriptsize{$  $}} (8b);
\node () at (10.5,1) {$ \dotsm $};
\draw (0.3,0.4) -- (0.4,0.4) -- (0.4,0.3);
\draw (4.7,0.4) -- (4.6,0.4) -- (4.6,0.3);
\draw (5.3,0.4) -- (5.4,0.4) -- (5.4,0.3);
\draw (9.7,0.4) -- (9.6,0.4) -- (9.6,0.3);
\draw (11.3,0.4) -- (11.4,0.4) -- (11.4,0.3);
\draw (14.7,0.4) -- (14.6,0.4) -- (14.6,0.3);
\end{tikzpicture}
\end{center}
and the derivation $ \deriv{x'}{y'} $ comes from a string
of double pushout diagrams
\[
\begin{tikzpicture}[scale=0.8]
\node (1t) at (0,2) {$ \ell'_1 $};
\node (2t) at (2,2) {$ k'_1 $};
\node (3t) at (4,2) {$ r'_1 $};
\node (4t) at (6,2) {$ \ell'_2 $};
\node (5t) at (8,2) {$ k'_2 $};
\node (6t) at (10,2) {$ r'_2 $};
\node (7t) at (11,2) {$ \ell'_m $};
\node (8t) at (13,2) {$ k'_m $};
\node (9t) at (15,2) {$ r'_m $};
\node (1b) at (0,0) {$ x' $};
\node (2b) at (2,0) {$ d'_1 $};
\node (3b) at (5,0) {$ w'_1 $};
\node (4b) at (8,0) {$ d'_2 $};
\node (5b) at (10,0) {$ w'_2 $};
\node (6b) at (11,0) {$ w'_{m-1} $};
\node (7b) at (13,0) {$ d'_m $};
\node (8b) at (15,0) {$ y' $};
\draw [cd] (2t) to node [] {\scriptsize{$  $}} (1t);
\draw [cd] (2t) to node [] {\scriptsize{$  $}} (3t);
\draw [cd] (5t) to node [] {\scriptsize{$  $}} (4t);
\draw [cd] (5t) to node [] {\scriptsize{$  $}} (6t);
\draw [cd] (8t) to node [] {\scriptsize{$  $}} (7t);
\draw [cd] (8t) to node [] {\scriptsize{$  $}} (9t);
\draw [cd] (2b) to node [] {\scriptsize{$  $}} (1b);
\draw [cd] (2b) to node [] {\scriptsize{$  $}} (3b);
\draw [cd] (4b) to node [] {\scriptsize{$  $}} (3b);
\draw [cd] (4b) to node [] {\scriptsize{$  $}} (5b);
\draw [cd] (7b) to node [] {\scriptsize{$  $}} (6b);
\draw [cd] (7b) to node [] {\scriptsize{$  $}} (8b);
\draw [cd] (1t) to node [] {\scriptsize{$  $}} (1b);
\draw [cd] (2t) to node [] {\scriptsize{$  $}} (2b);
\draw [cd] (3t) to node [] {\scriptsize{$  $}} (3b);
\draw [cd] (4t) to node [] {\scriptsize{$  $}} (3b);
\draw [cd] (5t) to node [] {\scriptsize{$  $}} (4b);
\draw [cd] (6t) to node [] {\scriptsize{$  $}} (5b);
\draw [cd] (7t) to node [] {\scriptsize{$  $}} (6b);
\draw [cd] (8t) to node [] {\scriptsize{$  $}} (7b);
\draw [cd] (9t) to node [] {\scriptsize{$  $}} (8b);
\node () at (10.5,1) {$ \dotsm $};
\draw (0.3,0.4) -- (0.4,0.4) -- (0.4,0.3);
\draw (4.7,0.4) -- (4.6,0.4) -- (4.6,0.3);
\draw (5.3,0.4) -- (5.4,0.4) -- (5.4,0.3);
\draw (9.7,0.4) -- (9.6,0.4) -- (9.6,0.3);
\draw (11.3,0.4) -- (11.4,0.4) -- (11.4,0.3);
\draw (14.7,0.4) -- (14.6,0.4) -- (14.6,0.3);
\end{tikzpicture}
\]
realize $ \deriv{x+x'}{y+y'} $ by
\begin{center}
\begin{tikzpicture}[scale=0.8]
\node (1t) at (0,2) {$ \ell_1 $};
\node (2t) at (2,2) {$ k_1 $};
\node (3t) at (4,2) {$ r1 $};
\node () at (5,1) {$ \cdots $};
\node (4t) at (6,2) {$ r_n $};
\node (5t) at (8,2) {$ \ell'_1 $};
\node (6t) at (10,2) {$ k'_1 $};
\node (7t) at (12,2) {$ r'_1 $};
\node () at (13,1) {$ \cdots $};
\node (8t) at (14,2) {$ k'_m $};
\node (9t) at (16,2) {$ r'_m $};
\node (1b) at (0,0) {$ x+x' $};
\node (2b) at (2,0) {$ d_1+x' $};
\node (3b) at (4,0) {$ w_1+x' $};
\node (5b) at (7,0) {$ y+x' $};
\node (6b) at (10,0) {$ y+d'_1 $};
\node (7b) at (12,0) {$ y+w'_1 $};
\node (8b) at (14,0) {$ y+d'_m $};
\node (9b) at (16,0) {$ y+y' $};
\draw [cd]
(2t) edge[] (1t)
(2t) edge[] (3t)
(6t) edge[] (5t)
(6t) edge[] (7t)
(8t) edge[] (9t)
(2b) edge[] (1b)
(2b) edge[] (3b)
(6b) edge[] (5b)
(6b) edge[] (7b)
(8b) edge[] (9b)
(1t) edge[] (1b)
(2t) edge[] (2b)
(3t) edge[] (3b)
(4t) edge[] (5b)
(5t) edge[] (5b)
(6t) edge[] (6b)
(7t) edge[] (7b)
(8t) edge[] (8b)
(9t) edge[] (9b);
\end{tikzpicture}
\end{center}
\end{proof}

As promised, we can now decompose closed systems into open
systems. For this, we need a topos of closed systems $ \X $
equipped with a grammar $ ( \X , P ) $. The closed systems
need interfaces, meaning we need to introduce an adjunction
\[
\adjunction{\A}{\X}{L}{R}{2}
\]
where $ L $ preserves pullbacks and has a monic counit. At
this point, the material from the previous section
returns. This adjunction gives a discrete comonad $ \flat
\bydef LR $ from which we form the discrete
grammar $ ( \X, P_\flat ) $. Now define the structured cospan
grammar $ ( _L \StrCsp , \hat{P_\flat} ) $ where $
\hat{P_\flat} $ contains the rule
\begin{equation} \label{eq:decomposition-square}
\begin{tikzpicture}
\node (1) at (0,4) {$ L 0 $};
\node (2) at (2,4) {$ \ell $};
\node (3) at (4,4) {$ LRk $};
\node (4) at (0,2) {$ L 0 $};
\node (5) at (2,2) {$ LRk $};
\node (6) at (4,2) {$ LRk $};
\node (7) at (0,0) {$ L 0 $};
\node (8) at (2,0) {$ r $};
\node (9) at (4,0) {$ LRk $};
\draw [cd] (1) to (2);
\draw [cd] (3) to (2);
\draw [cd] (4) to (5);
\draw [cd] (6) to (5);
\draw [cd] (7) to (8);
\draw [cd] (9) to (8);
\draw [cd] (4) to (1);
\draw [cd] (4) to (7);
\draw [cd] (5) to (2);
\draw [cd] (5) to (8);
\draw [cd] (6) to (3);
\draw [cd] (6) to (9);
\end{tikzpicture}
\end{equation}
for each rule $ \spn{\ell}{LRk}{r} $ of $ P_{\flat} $. We
use $ ( _L \StrCsp , \hat{P_\flat} ) $ to prove our main

Before stating the theorem, we note that this theorem
generalizes work by Gadducci and Heckel
[35] whose domain of
inquiry was graph rewriting. The arc of our
proof follows theirs.

\begin{theorem} \label{thm:inductive-rewriting}

Fix an adjunction $ (L \dashv R) \from \X \lrto \A $ with monic
counit. Let $ ( \X , P ) $ be a grammar such that for
every $ \X $-object $ x $ in the apex of a production of
$ P $, the lattice $ \Sub (x) $ has all meets. Given
$ g $, $ h \in \X $, then $ \deriv{g}{h} $ in the
rewriting relation for a grammar $ ( \X , P ) $ if and
only if there is a square
\[
\begin{tikzpicture}
\node (1t) at (0,4) {$ LR 0 $};
\node (2t) at (2,4) {$ g $};
\node (3t) at (4,4) {$ LR 0 $};
\node (1m) at (0,2) {$ LR 0 $};
\node (2m) at (2,2) {$ d $};
\node (3m) at (4,2) {$ LR 0 $};
\node (1b) at (0,0) {$ LR 0 $};
\node (2b) at (2,0) {$ h $};
\node (3b) at (4,0) {$ LR 0 $};
\draw [cd] (1t) to node [] {\scriptsize{$  $}} (2t);
\draw [cd] (3t) to node [] {\scriptsize{$  $}} (2t);
\draw [cd] (1m) to node [] {\scriptsize{$  $}} (2m);
\draw [cd] (3m) to node [] {\scriptsize{$  $}} (2m);
\draw [cd] (1b) to node [] {\scriptsize{$  $}} (2b);
\draw [cd] (3b) to node [] {\scriptsize{$  $}} (2b);
\draw [cd] (1m) to node [] {\scriptsize{$  $}} (1t);
\draw [cd] (1m) to node [] {\scriptsize{$  $}} (1b);
\draw [cd] (2m) to node [] {\scriptsize{$  $}} (2t);
\draw [cd] (2m) to node [] {\scriptsize{$  $}} (2b);
\draw [cd] (3m) to node [] {\scriptsize{$  $}} (3t);
\draw [cd] (3m) to node [] {\scriptsize{$  $}} (3b);
\end{tikzpicture}
\]
in the double category $ \Lang ( _{L}\StrCsp , \hat{P_\flat} ) $.
\end{theorem}

\begin{proof}
We show sufficiency by inducting on the length of the
derivation. If $ \deriv{g}{h} $ in a single step, meaning
that there is a diagram
\[
\begin{tikzpicture}
\node (1t) at (0,2) {$ \ell $};
\node (2t) at (2,2) {$ LRk $};
\node (3t) at (4,2) {$ r $};
\node (1b) at (0,0) {$ g $};
\node (2b) at (2,0) {$ d $};
\node (3b) at (4,0) {$ h $};
\draw [cd] (2t) to (1t);
\draw [cd] (2t) to (3t);
\draw [cd] (2b) to (1b);
\draw [cd] (2b) to (3b);
\draw [cd] (1t) to (1b);
\draw [cd] (2t) to (2b);
\draw [cd] (3t) to (3b);
\draw (0.3,0.4) -- (0.4,0.4) -- (0.4,0.3);
\draw (3.7,0.4) -- (3.6,0.4) -- (3.6,0.3);
\end{tikzpicture}
\]
then the desired square is the horizontal composition of
\[
\begin{tikzpicture}
\begin{scope}
\node (1t) at (0,4) {$ L0 $};
\node (2t) at (2,4) {$ \ell $};
\node (3t) at (4,4) {$ LRk $};
\node (4t) at (6,4) {$ d $};
\node (5t) at (8,4) {$ L0 $};
\node (1m) at (0,2) {$ L 0 $};
\node (2m) at (2,2) {$ LRk $};
\node (3m) at (4,2) {$ LRk $};
\node (4m) at (6,2) {$ d $};
\node (5m) at (8,2) {$ L 0 $};
\node (1b) at (0,0) {$ L 0 $};
\node (2b) at (2,0) {$ r $};
\node (3b) at (4,0) {$ LRk $};
\node (4b) at (6,0) {$ d $};
\node (5b) at (8,0) {$ L 0 $};
\draw [cd] (1t) to node [] {\scriptsize{$  $}} (2t);
\draw [cd] (3t) to node [] {\scriptsize{$  $}} (2t);
\draw [cd] (3t) to node [] {\scriptsize{$  $}} (4t);
\draw [cd] (5t) to node [] {\scriptsize{$  $}} (4t);
\draw [cd] (1m) to node [] {\scriptsize{$  $}} (2m);
\draw [cd] (3m) to node [] {\scriptsize{$  $}} (2m);
\draw [cd] (3m) to node [] {\scriptsize{$  $}} (4m);
\draw [cd] (5m) to node [] {\scriptsize{$  $}} (4m);
\draw [cd] (1b) to node [] {\scriptsize{$  $}} (2b);
\draw [cd] (3b) to node [] {\scriptsize{$  $}} (2b);
\draw [cd] (3b) to node [] {\scriptsize{$  $}} (4b);
\draw [cd] (5b) to node [] {\scriptsize{$  $}} (4b);
\draw [cd] (1m) to node [] {\scriptsize{$  $}} (1t);
\draw [cd] (1m) to node [] {\scriptsize{$  $}} (1b);
\draw [cd] (2m) to node [] {\scriptsize{$  $}} (2t);
\draw [cd] (2m) to node [] {\scriptsize{$  $}} (2b);
\draw [cd] (3m) to node [] {\scriptsize{$  $}} (3t);
\draw [cd] (3m) to node [] {\scriptsize{$  $}} (3b);
\draw [cd] (4m) to node [] {\scriptsize{$  $}} (4t);
\draw [cd] (4m) to node [] {\scriptsize{$  $}} (4b);
\draw [cd] (5m) to node [] {\scriptsize{$  $}} (5t);
\draw [cd] (5m) to node [] {\scriptsize{$  $}} (5b);
\end{scope}
\end{tikzpicture}
\]
The left square is a generator and the right square is the
identity on the horizontal arrow $ \csp{LRk}{d}{L0}
$. The square for a derivation
$ \dderiv{\deriv{g}{h}}{j} $ is the vertical composition
\[
\begin{tikzpicture}
\node (1t) at (0,8) {$ L 0 $};
\node (2t) at (2,8) {$ g $};
\node (3t) at (4,8) {$ L 0 $};
\node (1m) at (0,6) {$ L 0 $};
\node (2m) at (2,6) {$ d $};
\node (3m) at (4,6) {$ L 0 $};
\node (1b) at (0,4) {$ L 0 $};
\node (2b) at (2,4) {$ h $};
\node (3b) at (4,4) {$ L 0 $};
\node (1bb) at (0,2) {$ L 0 $};
\node (2bb) at (2,2) {$ e $};
\node (3bb) at (4,2) {$ L 0 $};
\node (1bbb) at (0,0) {$ L 0 $};
\node (2bbb) at (2,0) {$ j $};
\node (3bbb) at (4,0) {$ L 0 $};
\draw [cd] (1t) to node [] {\scriptsize{$  $}} (2t);
\draw [cd] (3t) to node [] {\scriptsize{$  $}} (2t);
\draw [cd] (1m) to node [] {\scriptsize{$  $}} (2m);
\draw [cd] (3m) to node [] {\scriptsize{$  $}} (2m);
\draw [cd] (1b) to node [] {\scriptsize{$  $}} (2b);
\draw [cd] (3b) to node [] {\scriptsize{$  $}} (2b);
\draw [cd] (1m) to node [] {\scriptsize{$  $}} (1t);
\draw [cd] (1m) to node [] {\scriptsize{$  $}} (1b);
\draw [cd] (2m) to node [] {\scriptsize{$  $}} (2t);
\draw [cd] (2m) to node [] {\scriptsize{$  $}} (2b);
\draw [cd] (3m) to node [] {\scriptsize{$  $}} (3t);
\draw [cd] (3m) to node [] {\scriptsize{$  $}} (3b);
\draw [cd] (1bb) to node [] {\scriptsize{$  $}} (2bb);
\draw [cd] (3bb) to node [] {\scriptsize{$  $}} (2bb);
\draw [cd] (1bbb) to node [] {\scriptsize{$  $}} (2bbb);
\draw [cd] (3bbb) to node [] {\scriptsize{$  $}} (2bbb);
\draw [cd] (1bb) to node [] {\scriptsize{$  $}} (1b);
\draw [cd] (1bb) to node [] {\scriptsize{$  $}} (1bbb);
\draw [cd] (2bb) to node [] {\scriptsize{$  $}} (2b);
\draw [cd] (2bb) to node [] {\scriptsize{$  $}} (2bbb);
\draw [cd] (3bb) to node [] {\scriptsize{$  $}} (3b);
\draw [cd] (3bb) to node [] {\scriptsize{$  $}} (3bbb);
\end{tikzpicture}
\]
The top square is from $ \deriv{g}{h} $ and the second
from $ \dderiv{h}{j} $.

Conversely, proceed by structural induction on the
generating squares of
$ \Lang ( _{L}\StrCsp , \hat{P_\flat} ) $.  It suffices to
show that the rewrite relation is preserved by vertical
and horizontal composition by generating squares.  Suppose
we have a square
\[
\begin{tikzpicture}
\node (1t) at (0,4) {$ L 0 $};
\node (2t) at (2,4) {$ w $};
\node (3t) at (4,4) {$ L 0 $};
\node (1m) at (0,2) {$ L 0 $};
\node (2m) at (2,2) {$ x $};
\node (3m) at (4,2) {$ L 0 $};
\node (1b) at (0,0) {$ L 0 $};
\node (2b) at (2,0) {$ y $};
\node (3b) at (4,0) {$ L 0 $};
\draw [cd] (2t) to node [] {\scriptsize{$  $}} (1t);
\draw [cd] (2t) to node [] {\scriptsize{$  $}} (3t);
\draw [cd] (2m) to node [] {\scriptsize{$  $}} (1m);
\draw [cd] (2m) to node [] {\scriptsize{$  $}} (3m);
\draw [cd] (2b) to node [] {\scriptsize{$  $}} (1b);
\draw [cd] (2b) to node [] {\scriptsize{$  $}} (3b);
\draw [cd] (1m) to node [] {\scriptsize{$  $}} (1t);
\draw [cd] (2m) to node [] {\scriptsize{$  $}} (2t);
\draw [cd] (3m) to node [] {\scriptsize{$  $}} (3t);
\draw [cd] (1m) to node [] {\scriptsize{$  $}} (1b);
\draw [cd] (2m) to node [] {\scriptsize{$  $}} (2b);
\draw [cd] (3m) to node [] {\scriptsize{$  $}} (3b);
\end{tikzpicture}
\]
corresponding to a derivation $ \deriv{w}{y} $. Composing
this vertically with a generating square, which must have
\[
\begin{tikzpicture}
\node (1t) at (0,4) {$ L 0 $};
\node (2t) at (2,4) {$ y $};
\node (3t) at (4,4) {$ L 0 $};
\node (1m) at (0,2) {$ L 0 $};
\node (2m) at (2,2) {$ L 0 $};
\node (3m) at (4,2) {$ L 0 $};
\node (1b) at (0,0) {$ L 0 $};
\node (2b) at (2,0) {$ z $};
\node (3b) at (4,0) {$ L 0 $};
\draw [cd] (2t) to node [] {\scriptsize{$  $}} (1t);
\draw [cd] (2t) to node [] {\scriptsize{$  $}} (3t);
\draw [cd] (2m) to node [] {\scriptsize{$  $}} (1m);
\draw [cd] (2m) to node [] {\scriptsize{$  $}} (3m);
\draw [cd] (2b) to node [] {\scriptsize{$  $}} (1b);
\draw [cd] (2b) to node [] {\scriptsize{$  $}} (3b);
\draw [cd] (1m) to node [] {\scriptsize{$  $}} (1t);
\draw [cd] (2m) to node [] {\scriptsize{$  $}} (2t);
\draw [cd] (3m) to node [] {\scriptsize{$  $}} (3t);
\draw [cd] (1m) to node [] {\scriptsize{$  $}} (1b);
\draw [cd] (2m) to node [] {\scriptsize{$  $}} (2b);
\draw [cd] (3m) to node [] {\scriptsize{$  $}} (3b);
\end{tikzpicture}
\]
corresponding to a production $ \spn{y}{L0}{z} $ gives
\[
\begin{tikzpicture}
\node (1t) at (0,4) {$ L 0 $};
\node (2t) at (2,4) {$ w $};
\node (3t) at (4,4) {$ L 0 $};
\node (1m) at (0,2) {$ L 0 $};
\node (2m) at (2,2) {$ L 0 $};
\node (3m) at (4,2) {$ L 0 $};
\node (1b) at (0,0) {$ L 0 $};
\node (2b) at (2,0) {$ z $};
\node (3b) at (4,0) {$ L 0 $};
\draw [cd] (2t) to node [] {\scriptsize{$  $}} (1t);
\draw [cd] (2t) to node [] {\scriptsize{$  $}} (3t);
\draw [cd] (2m) to node [] {\scriptsize{$  $}} (1m);
\draw [cd] (2m) to node [] {\scriptsize{$  $}} (3m);
\draw [cd] (2b) to node [] {\scriptsize{$  $}} (1b);
\draw [cd] (2b) to node [] {\scriptsize{$  $}} (3b);
\draw [cd] (1m) to node [] {\scriptsize{$  $}} (1t);
\draw [cd] (2m) to node [] {\scriptsize{$  $}} (2t);
\draw [cd] (3m) to node [] {\scriptsize{$  $}} (3t);
\draw [cd] (1m) to node [] {\scriptsize{$  $}} (1b);
\draw [cd] (2m) to node [] {\scriptsize{$  $}} (2b);
\draw [cd] (3m) to node [] {\scriptsize{$  $}} (3b);
\end{tikzpicture}
\]
which corresponds to a derivation
$ \dderiv{\deriv{w}{y}}{z} $.  Composing horizontally with
a generating square
\[
\begin{tikzpicture}
\node (1t) at (0,4) {$ L 0 $};
\node (2t) at (2,4) {$ \ell $};
\node (3t) at (4,4) {$ L 0 $};
\node (1m) at (0,2) {$ L 0 $};
\node (2m) at (2,2) {$ LRk $};
\node (3m) at (4,2) {$ L 0 $};
\node (1b) at (0,0) {$ L 0 $};
\node (2b) at (2,0) {$ r $};
\node (3b) at (4,0) {$ L 0 $};
\draw [cd] (2t) to node [] {\scriptsize{$  $}} (1t);
\draw [cd] (2t) to node [] {\scriptsize{$  $}} (3t);
\draw [cd] (2m) to node [] {\scriptsize{$  $}} (1m);
\draw [cd] (2m) to node [] {\scriptsize{$  $}} (3m);
\draw [cd] (2b) to node [] {\scriptsize{$  $}} (1b);
\draw [cd] (2b) to node [] {\scriptsize{$  $}} (3b);
\draw [cd] (1m) to node [] {\scriptsize{$  $}} (1t);
\draw [cd] (2m) to node [] {\scriptsize{$  $}} (2t);
\draw [cd] (3m) to node [] {\scriptsize{$  $}} (3t);
\draw [cd] (1m) to node [] {\scriptsize{$  $}} (1b);
\draw [cd] (2m) to node [] {\scriptsize{$  $}} (2b);
\draw [cd] (3m) to node [] {\scriptsize{$  $}} (3b);
\end{tikzpicture}
\]
corresponding with a production $ \spn{\ell}{LRk}{r} $
results in the square
\[
\begin{tikzpicture}
\node (1t) at (0,4) {$ L 0 $};
\node (2t) at (2,4) {$ w + \ell $};
\node (3t) at (4,4) {$ L 0 $};
\node (1m) at (0,2) {$ L 0 $};
\node (2m) at (2,2) {$ x + LRk $};
\node (3m) at (4,2) {$ L 0 $};
\node (1b) at (0,0) {$ L 0 $};
\node (2b) at (2,0) {$ y + r $};
\node (3b) at (4,0) {$ L 0 $};
\draw [cd] (2t) to node [] {\scriptsize{$  $}} (1t);
\draw [cd] (2t) to node [] {\scriptsize{$  $}} (3t);
\draw [cd] (2m) to node [] {\scriptsize{$  $}} (1m);
\draw [cd] (2m) to node [] {\scriptsize{$  $}} (3m);
\draw [cd] (2b) to node [] {\scriptsize{$  $}} (1b);
\draw [cd] (2b) to node [] {\scriptsize{$  $}} (3b);
\draw [cd] (1m) to node [] {\scriptsize{$  $}} (1t);
\draw [cd] (2m) to node [] {\scriptsize{$  $}} (2t);
\draw [cd] (3m) to node [] {\scriptsize{$  $}} (3t);
\draw [cd] (1m) to node [] {\scriptsize{$  $}} (1b);
\draw [cd] (2m) to node [] {\scriptsize{$  $}} (2b);
\draw [cd] (3m) to node [] {\scriptsize{$  $}} (3b);
\end{tikzpicture}
\]
But $ \deriv{w+\ell}{y+r} $ as seen in Lemma
\ref{thm:rewrite-rel-is-additive}.
\end{proof}

With this result, we have completely described the rewrite
relation for a grammar $ ( \X , P ) $ with squares in
$ \Lang ( _{L}\StrCsp, \hat{P_\flat} ) $ framed by the
initial object of $ \X $.  These squares are rewrites of a
closed system in the sense that the interface is empty.  We
can instead begin with a closed system $ x $ in $ \X $ as
represented by a horizontal arrow $ \csp{L0}{x}{L0} $ in
$ \Lang ( _{L}\StrCsp , \hat{P_\flat} ) $ and decompose it
into a composite of sub-systems, that is a sequence of
composable horizontal arrows
\begin{center}
\begin{tikzpicture}
\node (L0) at (0,0) {$ L0 $};
\node (x1) at (1,1) {$ x_1 $};
\node (La1) at (2,0) {$ La_1 $};
\node (x2) at (3,1) {$ x_2 $};
\node (La2) at (4,0) {$ La_2 $};
\node () at (5,0) {$ \dotsm $};
\node (Lan1) at (6,0) {$ La_{n-1} $};
\node (xn) at (7,1) {$ x_n $};
\node (L0') at (8,0) {$ L0 $};
\draw [cd]
(L0) edge[] (x1)
(La1) edge[] (x1)
(La1) edge[] (x2)
(La2) edge[] (x2)
(Lan1) edge[] (xn)
(L0') edge[] (xn);
\end{tikzpicture}
\end{center}

Rewriting can be performed on each of these sub-systems
\[
\begin{tikzpicture}
\begin{scope}[shift={(0,6)}]
\node (1) at (0,4) {$ L0 $};
\node (2) at (2,4) {$ x_1 $};
\node (3) at (4,4) {$ La_1 $};
\node (4) at (0,2) {$ L0 $};
\node (5) at (2,2) {$ x'_1 $};
\node (6) at (4,2) {$ La'_1 $};
\node (7) at (0,0) {$ L0 $};
\node (8) at (2,0) {$ x''_1 $};
\node (9) at (4,0) {$ La''_1 $};
\draw [cd] (1) to (2);
\draw [cd] (3) to (2);
\draw [cd] (4) to (5);
\draw [cd] (6) to (5);
\draw [cd] (7) to (8);
\draw [cd] (9) to (8);
\draw [cd] (4) to node [left]
{\scriptsize{$ \cong $}} (1);
\draw [cd] (4) to node [left]
{\scriptsize{$ \cong $}} (7);
\draw [>->] (5) to (2);
\draw [>->] (5) to (8);
\draw [cd] (6) to node [right]
{\scriptsize{$ \cong  $}} (3);
\draw [cd] (6) to node [right]
{\scriptsize{$ \cong $}} (9);
\end{scope}
\begin{scope}[shift={(6,6)}]
\node (1) at (0,4) {$ La_{n-1} $};
\node (2) at (2,4) {$ x_n $};
\node (3) at (4,4) {$ L0 $};
\node (4) at (0,2) {$ La_{n-1} $};
\node (5) at (2,2) {$ x'_n $};
\node (6) at (4,2) {$ L0 $};
\node (7) at (0,0) {$ La_{n-1} $};
\node (8) at (2,0) {$ x''_n $};
\node (9) at (4,0) {$ L0 $};
\draw [cd] (1) to (2);
\draw [cd] (3) to (2);
\draw [cd] (4) to (5);
\draw [cd] (6) to (5);
\draw [cd] (7) to (8);
\draw [cd] (9) to (8);
\draw [cd] (4) to node [left]
{\scriptsize{$ \cong $}} (1);
\draw [cd] (4) to node [left]
{\scriptsize{$ \cong $}} (7);
\draw [>->] (5) to (2);
\draw [>->] (5) to (8);
\draw [cd] (6) to node [right]
{\scriptsize{$ \cong  $}} (3);
\draw [cd] (6) to node [right]
{\scriptsize{$ \cong $}} (9);
\end{scope}
\begin{scope}
\node (1) at (0,4) {$ L0 $};
\node (2) at (2,4) {$ y_1 $};
\node (3) at (4,4) {$ La_1 $};
\node (4) at (0,2) {$ L0 $};
\node (5) at (2,2) {$ y'_1 $};
\node (6) at (4,2) {$ La_1 $};
\node (7) at (0,0) {$ L0 $};
\node (8) at (2,0) {$ y''_1 $};
\node (9) at (4,0) {$ La_1 $};
\draw [cd] (1) to (2);
\draw [cd] (3) to (2);
\draw [cd] (4) to (5);
\draw [cd] (6) to (5);
\draw [cd] (7) to (8);
\draw [cd] (9) to (8);
\draw [cd] (4) to node [left]
{\scriptsize{$ \cong $}} (1);
\draw [cd] (4) to node [left]
{\scriptsize{$ \cong $}} (7);
\draw [>->] (5) to (2);
\draw [>->] (5) to (8);
\draw [cd] (6) to node [right]
{\scriptsize{$ \cong  $}} (3);
\draw [cd] (6) to node [right]
{\scriptsize{$ \cong $}} (9);
\end{scope}
\begin{scope}[shift={(6,0)}]
\node (1) at (0,4) {$ La_{n-1} $};
\node (2) at (2,4) {$ y_n $};
\node (3) at (4,4) {$ L0 $};
\node (4) at (0,2) {$ La_{n-1} $};
\node (5) at (2,2) {$ y'_n $};
\node (6) at (4,2) {$ L0 $};
\node (7) at (0,0) {$ La_{n-1} $};
\node (8) at (2,0) {$y''_n $};
\node (9) at (4,0) {$ L0 $};
\draw [cd] (1) to (2);
\draw [cd] (3) to (2);
\draw [cd] (4) to (5);
\draw [cd] (6) to (5);
\draw [cd] (7) to (8);
\draw [cd] (9) to (8);
\draw [cd] (4) to node [left]
{\scriptsize{$ \cong $}} (1);
\draw [cd] (4) to node [left]
{\scriptsize{$ \cong $}} (7);
\draw [>->] (5) to (2);
\draw [>->] (5) to (8);
\draw [cd] (6) to node [right]
{\scriptsize{$ \cong  $}} (3);
\draw [cd] (6) to node [right]
{\scriptsize{$ \cong $}} (9);
\end{scope}
\node () at (5,2) {$ \dotsm $};
\node () at (2,5) {$ \vdots $};
\node () at (5,8) {$ \dotsm $};
\node () at (8,5) {$ \vdots $};
\end{tikzpicture}
\]
The composite of these squares is a rewriting of the
original system.

%%%%%%%%%%%%%%%%%%%             %%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%   CHAPTER   %%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%% CONCLUSIONS %%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%             %%%%%%%%%%%%%%

\chapter{Conclusions}
\label{sec:conclusions}

Our work here demarcates a starting line on the path
towards a fully general mathematical theory of systems. We now
have a syntax to reason with.  Built into this syntax is a
mechanism to identify when distinct systems behave
similarly. That is, our syntax reflects semantics.

The semantics side requires attention.  We can conjecture
that the category $ \Rel $ of sets and relations will be the
most appropriate category to serve as our semantic
universe.  The naive idea behind this belief is that
semantics should describe the relationship between inputs
and outputs possible for a particular system.  If not
$ \Rel $, then something structurally similar such as the
category $ \cat{Hilb} $ of Hilbert spaces and linear
maps. This would be appropriate semantics for the

Given a more robust theory of semantics to work with, we can
fill in the larger picture of a general language for
systems.  To do this, Lawvere's `functorial semantics'
[45] is a promising area from which
to pull. Functorial semantics has been successful in
developing universal algebra, and the author believes that
we can leverage Lawvere's thinking in the systems context. To
what extent, however, remains an open question.

%%%%%%%%%%%%%%%%%%%          %%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%% APPENDIX %%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%          %%%%%%%%%%%%%%%%%

\appendix

% ===================================================
% APPENDIX
% CHAPTER: double categories
% ===================================================

\chapter{An account of some category theory topics}
\label{sec:double-cats}

Category theory has been in mainstream mathematical
discourse for decades now.  This section does not seek to
add to an already crowded literature on category
theory. Instead, we give just enough background for those
readers coming to this thesis without much knowledge about
category theory. For a more in depth study of category
theory, there are many excellent resources
[2, 44, 46, 56].

As a baseline, we assume basic knowledge of category
theory.  This includes the definitions of categories, functors,
natural transformations, limits, colimits, adjunctions,
monoidal categories, and symmetric monoidal categories.
But our needs extend beyond these basic concepts, so we
provide the reader with a brief account of some more
advanced topics.

% ===============================================
\section{Enrichment and bicategories}
\label{sec:extern-bicats}
% ===============================================

The most familiar examples of categories are built from
mathematical widgets and their homomorphisms.  For example,
the category $ \Vect_F $ whose objects are vector spaces
over a fixed field $ F $ and arrows are linear maps.  Yet,
as a category, $ \Vect_F $ does not truly capture everything
we like about vector spaces. We are missing the fact that,
for any two vector spaces $ V $ and $ W $, the space of
linear maps from $ V $ to $ W $ form a vector space by
pointwise addition and scaling.  Yet the hom-set
$ \Vect_F (V,W) $ is merely a collection of linear maps
without additional structure.  The theory of enriched
categories fixes this drawback.

Many familiar categories are actually enriched. For example,
the category $ \Set $ of sets has that, for any two sets
$ x,y $, the collection of arrows $ \Set (x,y) $ is actually
a set.  We say that $ \Set $ is enriched over $ \Set $.
Given the category $ \Mod_R $ whose objects are modules over
an arbitrary ring $ R $ and any two such modules $ x $,
$ y $, the collections of arrows $ \Mod_R (x,y) $ is
actually a $ \mathbb{Z} $-module.  Thus we say that
$ \Mod_R $ is enriched over $ \Mod_{\mathbb{Z}} $.  However,
to be an enriched category, it is not enough for the
collections of arrows to simply have additional structure.
Cohesion is needed.

\begin{definition}[Enriched category]
Let $ (\M,\otimes,I,\alpha,\lambda,\rho) $ be a
monoidal category. A category $ \C $ is \defn{enriched}
over $ \M $ consists of
\begin{itemize}
\item a class $ \ob (\C) $ of objects,
\item an object $ \C (a,b) $ of $ \M $ for each
pair $ a,b \in \ob (\C) $ that collects the
arrows of type $ a \to b $
\item an arrow $ 1_a \from I \to \C (a,a) $ in
$ \M $ that chooses an identity arrow on $ a $
\item an arrow
\[
\circ_{abc} \from \C (b,c) \otimes \C (a,b)
\to \C (a,c)
\]
for each triple of objects $ a,b,c \in \ob
(\C) $ that defines the composition
\end{itemize}
together with a commuting diagram expressing associativity
\[
\begin{tikzpicture}
\node (1) at (0,4)
{$ (\C (c,d) \otimes \C (b,c) )
\otimes \C (a,b) $};
\node (2) at (6,4)
{$ \C (b,d) \otimes \C (a,d) $};
\node (3) at (6,2)
{$ \C (a,d) $};
\node (4) at (0,0)
{$ \C (c,d) \otimes (\C (b,c)
\otimes \C ( a,b) ) $};
\node (5) at (6,0)
{$ \C (c,d) \otimes \C (a,c) $};
\draw[cd]
(1) edge node[above]{$\circ \otimes \id$} (2)
(2) edge node[right]{$\circ$} (3)
(1) edge node[left]{$\alpha$} (4)
(4) edge node[below]{$\id \otimes \circ$} (5)
(5) edge node[right]{$\circ$} (3);
\end{tikzpicture}
\]
and commuting diagrams expressing left and right unity
\[
\begin{tikzpicture}
\begin{scope}
\node (1) at (0,2)
{$ I \otimes \C (a,b) $};
\node (2) at (2,0)
{$ \C (a,b) $};
\node (3) at (4,2)
{$ \C (b,b) \otimes \C (a,b) $};
\draw[cd]
(1) edge node[left]{$ \lambda $} (2)
(1) edge node[above]{$ 1 \otimes \id $} (3)
(3) edge node[right]{$ \circ $} (2);
\end{scope}
\begin{scope}[shift={(8,0)}]
\node (1) at (0,2)
{$ \C (a,b) \otimes I $};
\node (2) at (2,0)
{$ \C (a,b) $};
\node (3) at (4,2)
{$ \C (a,b) \otimes \C (a,a) $};
\draw[cd]
(1) edge node[left]{$ \rho $} (2)
(1) edge node[above]{$ \id \otimes 1 $} (3)
(3) edge node[right]{$ \circ $} (2);
\end{scope}
\end{tikzpicture}
\]
When $ \M $ is actually a 2-category and the
above diagrams only commute up to natural
isomorphism, then we say that $ \C $ is
\defn{weakly enriched} over $ \M $.
\end{definition}

In this thesis, the we are interested in one example of an
weakly enriched category: a bicategory. In short, a
bicategory is a category weakly enriched in the 2-category $
\Cat $.  Thus a bicategory has a \emph{category} of arrows between
objects, not merely a collection of arrows.

Defining a bicategory to be a category weakly enriched in
$ \Cat $ is elegant but hardly illuminating. Thus, the
definition is worth unpacking but, for clarity's sake, we
only approximate the definition by providing the important
information to know and ignoring technical details.

\begin{definition}[Bicategory]
A bicategory $ \CC $ consists of
\begin{itemize}
\item a collection of objects $ \ob (\CC) $
\item for each pair of objects $ x,y $, a collection of
arrows of type $ x \to y $ which compose, that is
\[
( x \xto{f} y \xto{g} z ) \mapsto (x \xto{gf} z)
\]
\item for each pair of arrows $ f,g \from x \to y $ of the
same type, a collection of 2-arrows
\[
\begin{tikzpicture}
\node (x) at (0,0) {$ x $};
\node (y) at (2,0) {$ y $};
\draw[cd]
(x) edge[bend left=60]  node[above]{$ f $} (y)
(x) edge[bend right=60] node[below]{$ g $} (y);
\node at (1,0) {$\Downarrow$};
\end{tikzpicture}
\]
together with operations expressing a horizontal composition
\[
\begin{tikzpicture}
\begin{scope}
\node (x) at (0,0) {$ x $};
\node (y) at (2,0) {$ y $};
\node (z) at (4,0) {$ z $};
\draw [cd]
(x) edge[bend left=60] node[above]{$ f $} (y)
(x) edge[bend right=60] node[below]{$ g $} (y)
(y) edge[bend left=60] node[above]{$ f' $} (z)
(y) edge[bend right=60] node[below]{$ g' $} (z);
\node at (1,0) {{$\Downarrow_\alpha$}};
\node at (3,0) {{$\Downarrow_\beta$}};
\end{scope}
\begin{scope}[shift={(6,0)}]
\node (x) at (0,0) {$ x $};
\node (z) at (2,0) {$ z $};
\draw [cd]
(x) edge[bend left=60] node[above]{$f'f$} (z)
(x) edge[bend right=60] node[below]{$g'g$} (z);
\node at (1,0) {{$\Downarrow_{\alpha\hcirc\beta}$}};
\end{scope}
\node () at (5,0) {$\xmapsto{\hcirc}$};
\end{tikzpicture}
\]
and vertical composition
\[
\begin{tikzpicture}
\begin{scope}
\node (x) at (0,0) {$ x $};
\node (y) at (3,0) {$ y $};
\draw [cd]
(x) edge[bend left=60] (y)
(x) edge[bend right=60] (y)
(x) edge (y);
\node at (1.5,0.5)
{\scriptsize{$\Downarrow_\alpha $}};
\node at (1.5,-0.5)
{\scriptsize{$\Downarrow_\beta $}};
\end{scope}
\begin{scope}[shift={(5,0)}]
\node (x) at (0,0) {$ x $};
\node (y) at (3,0) {$ y $};
\draw [cd]
(x) edge[bend left=60] (y)
(x) edge[bend right=60] (y);
\node () at (1.5,0) {$\Downarrow_{\beta\vcirc\alpha}$};
\end{scope}
\node () at (4,0) {$\xmapsto{\vcirc}$};
\end{tikzpicture}
\]
that satisfy the interchange law
\[
(\alpha  \hcirc \beta   ) \vcirc
(\alpha' \hcirc \beta'  ) =
(\alpha  \vcirc \alpha' ) \hcirc
(\beta   \vcirc \beta'  )
\]
\end{itemize}

The interchange law states that given an array of 2-arrows
\[
\begin{tikzpicture}
\node (x) at (0,0) {$ x $};
\node (y) at (3,0) {$ y $};
\node (z) at (6,0) {$ z $};
\node () at (1.5,0.5)  {$ \Downarrow_\alpha $};
\node () at (1.5,-0.5) {$ \Downarrow_{\alpha'} $};
\node () at (4.5,0.5)  {$ \Downarrow_\beta $};
\node () at (4.5,-0.5) {$ \Downarrow_{\beta'} $};
\draw[cd]
(x) edge[bend left=60]  (y)
(x) edge                (y)
(x) edge[bend right=60] (y)
(y) edge[bend left=60]  (z)
(y) edge                (z)
(y) edge[bend right=60] (z);
\end{tikzpicture}
\]
performing the two horizontal compositions
\[
\begin{tikzpicture}
\node (x) at (0,0) {$ x $};
\node (z) at (4,0) {$ z $};
\node at (2,0.5)  {$\Downarrow_{\alpha \hcirc \beta}$};
\node at (2,-0.5) {$\Downarrow_{\alpha' \hcirc \beta}$};
\path[cd,font=\scriptsize]
(x) edge[bend left=60] (z)
(x) edge               (z)
(x) edge[bend right=60] (z);
\end{tikzpicture}
\]
followed by the vertical composition
\[
\begin{tikzpicture}
\node (x) at (0,0) {$ x $};
\node (z) at (4,0) {$ z $};
\node at (2,0)
{ $\Downarrow_{(\alpha \hcirc \beta)
\vcirc (\alpha' \hcirc \beta')} $};
\draw[cd]
(x) edge[bend left=60]  (z)
(x) edge[bend right=60] (z);
\end{tikzpicture}
\]
gives exactly the same 2-arrow as first performing
the two vertical compositions
\[
\begin{tikzpicture}
\node (x) at (0,0) {$ x $};
\node (y) at (2,0) {$ y $};
\node (z) at (4,0) {$ z $};
\node at (1,0) {$\Downarrow_{\alpha \vcirc \beta}$};
\node at (3,0) {$\Downarrow_{\alpha' \vcirc \beta'}$};
\draw[cd]
(x) edge[bend left=60]  (y)
(x) edge[bend right=60] (y)
(y) edge[bend left=60]  (z)
(y) edge[bend right=60] (z);
\end{tikzpicture}
\]
followed by the horizontal composition
\[
\begin{tikzpicture}
\node (x) at (0,0) {$ x $};
\node (z) at (4,0) {$ z $};
\node () at (2,0) {
$ \Downarrow_{(\alpha \vcirc \alpha')
\hcirc (\beta \vcirc \beta'}) $ };
\draw[cd]
(x) edge[bend left=60] (z)
(x) edge[bend right=60] (z);
\end{tikzpicture}
\]
\end{definition}

That definition deconstructs a bicategory, laying out all of
the components. Next, we give a definition in the spirit of

\begin{definition}[Bicategory]
Consider the monoidal 2-category $ (\CCat, \times,
\cat{1}) $. A bicategory $ \CC $ has
\begin{itemize}
\item a collection of objects $ \ob (\CC) $
\item for each pair of objects $ a,b \in \ob (\CC) $, a
category $ \CC (a,b) $ of arrows
\item for each object $ a \in \ob (\CC) $, a functor $ \id_a \from
\cat{1} \to \CC (a,a) $ that chooses the identity element
\item for each triple of objects $ a,b,c \in \ob (\CC) $,
a functor
\[
\circ_{a,b,c} \from
\CC (b,c) \times \CC (a,b) \to \CC (a,c)
\]
expressing composition
\end{itemize}
such that, for all $ a,b,c,d \in \ob (\CC) $, the associativity diagram
\[
\begin{tikzpicture}
\node (1) at (0,2)
{$ (\CC (c,d) \times \CC (b,c)) \times \CC (a,b) $};
\node (2) at (8,2)
{$ \CC (c,d) \times (\CC (b,c) \times \CC (a,b) $};
\node (3) at (0,0) {$ \CC (b,d) \times \CC (a,b) $};
\node (4) at (8,0) {$ \CC (c,d) \times \CC (a,c) $};
\node (5) at (4,-2) {$ \CC (a,d) $};
\node () at (4,0) {$ \Downarrow \iso $};
\draw[cd]
(1) edge node[above]{$ \alpha $} (2)
(1) edge node[left]{$ \circ \times \id $} (3)
(2) edge node[right]{$ \id \times \circ $} (4)
(3) edge node[left]{$ \circ $} (5)
(4) edge node[right]{$ \circ $} (5);
\end{tikzpicture}
\]
and the left and right unitor diagrams
\[
\begin{tikzpicture}
\begin{scope}
\node (1) at (0,2) {$ \bicat{1} \times \CC (a,b) $};
\node (2) at (4,2) {$ \CC (b,b) \times \CC (a,b) $};
\node (3) at (4,0) {$ \CC (a,b) $};
\node () at (3,1.25)  {$ \Downarrow \iso $};
\draw[cd]
(1) edge node[above]{$ i_b \times \id $} (2)
(1) edge node[below]{$ \lambda $} (3)
(2) edge node[right]{$ \circ $} (3);
\end{scope}
\begin{scope}[shift={(8,0)}]
\node (1) at (0,2) {$ \CC (a,b) \times \bicat{1} $};
\node (2) at (4,2) {$ \CC (a,b) \times \CC (a,a) $};
\node (3) at (4,0) {$ \CC (a,b) $};
\node ()  at (3,1.25) {$ \Downarrow \iso $};
\draw[cd]
(1) edge node[above]{$ i_a \times \id $} (2)
(1) edge node[below]{$ \rho $}           (3)
(2) edge node[right]{$ \circ $}          (3);
\end{scope}
\end{tikzpicture}
\]
commute up to a natural isomorphism.
\end{definition}

We observe that the objects of the hom-category
$ \CC (a,b) $ are arrows in $ \CC $ and the arrows of
$ \CC (a,b) $ are 2-arrows in $ \CC $. Composition in
$ \CC (a,b) $ is the vertical composition in $ \CC $. The
composition of the arrows and horizontal composition of
2-arrows in $ \CC $ is given by the functor $ \circ $ which,
by light of it preserving composition, gives the interchange

% ===============================================
\section{Internalization and double categories}
\label{sec:internal-double-cats}
% ===============================================

Most treatments of mathematics base definitions on set
theory. The definitions for a monoid, topological space,
poset, and so on all begin by establishing a set. An
alternative viewpoint is to internalize such gadgets in a

For example, a monoid is traditionally defined to be a set
$ M $ together with an identity element $ e \in M $ equipped
with a binary operation $ M \times M \to M $ such that for
all $ x,y,z \in M $, we have $ ex=x=xe $ and $ (xy)z=x(yz)
$. However, we can also define a monoid \emph{internal} to a

\begin{definition}[Internal monoid]
\label{def:intern-monoid}
Let $ (\C , \otimes , I ) $ be a
monoidal category.  A \defn{monoid internal to $ \C $}
consists of an object $ m \in \ob (\C) $ and two arrows in
$ \C $
\begin{itemize}
\item (multiplication) $ \mu \from m \otimes m \to m $,
\item (unit) $ \eta \from I \to m $
\end{itemize}
such that the associator diagram
\[
\begin{tikzpicture}
\node (1) at (0,2) {$ (m \otimes m) \otimes m $};
\node (2) at (4,2) {$ m \otimes (m \otimes m) $};
\node (3) at (8,2) {$ m \otimes m $};
\node (4) at (0,0) {$ m \otimes m $};
\node (5) at (8,0) {$ m $};
\draw [cd] (1) to node [above]
{$ \alpha $} (2);
\draw [cd] (2) to node [above]
{$ \id \otimes \mu $} (3);
\draw [cd] (3) to node [right]
{$ \mu $} (5);
\draw [cd] (1) to node [left]
{$ \mu \otimes \id$} (4);
\draw [cd] (4) to node [below] {$ \mu $} (5);
\end{tikzpicture}
\]
and unitor diagram
\[
\begin{tikzpicture}
\node (1) at (-4,2) {$ I \otimes m $};
\node (2) at (0,2)  {$ m \otimes m $};
\node (3) at (4,2)  {$ m \otimes I $};
\node (4) at (0,0)  {$ m $};
\draw [cd] (1) to node[above]{$ \eta \otimes \id $} (2);
\draw [cd] (1) to node[below]{$ \lambda $} (4);
\draw [cd] (2) to node[left]{$ \mu $} (4);
\draw [cd] (3) to node[above]{$ \id \otimes \eta $} (2);
\draw [cd] (3) to node[below]{$ \rho $} (4);
\end{tikzpicture}
\]

A \defn{morphism of monoids} is an arrow
$ f \from m \to m' $ in $ \C $ between two monoid objects $
( m,\mu,\eta ) $ and $ ( m',\mu',\eta' ) $ that
preserve multiplication and the unit as expressed by the
following commuting diagrams
\begin{center}
\begin{tikzpicture}
\begin{scope}
\node (mm) at (0,2) {$ m \otimes m $};
\node (m'm') at (3,2) {$ m' \otimes m' $};
\node (m) at (0,0) {$ m $};
\node (m') at (3,0) {$ m' $};
\draw [cd]
(mm) edge[] node[above]{$ f \otimes f $} (m'm')
(mm) edge[] node[left]{$ \mu $} (m)
(m) edge[] node[below]{$ f $} (m')
(m'm') edge[] node[right]{$ \mu' $} (m');
\end{scope}
\begin{scope}[shift={(6,0)}]
\node (I) at (0,2) {$ I $};
\node (m) at (2,2) {$ m $};
\node (m') at (2,0) {$ m' $};
\draw [cd]
(I) edge[] node[above]{$ \eta $} (m)
(I) edge[] node[below]{$ \eta' $} (m')
(m) edge[] node[right]{$ f $} (m');
\end{scope}
\node () at (4,1) {and};
\end{tikzpicture}
\end{center}
\end{definition}

We can also provide an internal monoid with a commutative

\begin{definition}[Internal commutative monoid]
\label{def:intern-comm-monoid}
Given a symmetric monoidal category $ ( \C,\otimes,I,\tau ) $
where $ \tau $ is the twist map, a \defn{commutative
monoid internal to $ \C $} is, first, a monoid internal
to $ \C $ with the additional property that the diagram
\begin{center}
\begin{tikzpicture}
\node (mm1) at (0,2) {$ m \otimes m $};
\node (mm2) at (2,2) {$ m \otimes m $};
\node (m) at (1,0) {$ m $};
\draw [cd]
(mm1) edge[] node[above]{$ \tau $} (mm2)
(mm1) edge[] node[below]{$ \mu $} (m)
(mm2) edge[] node[below]{$ \mu $} (m);
\end{tikzpicture}
\end{center}
\end{definition}

Algebraic structures often have dual counterparts, and
internal monoids are no exception.

\begin{definition}[Internal comonoid]
Given a monoidal category $ ( \C , \otimes , I ) $, a
\defn{comonoid internal to $ \C $} is a monoid internal to
$ \C\op $. If $ ( \C , \otimes , I , \tau ) $ is a
symmetric monoidal category, then a \defn{cocommutative
comonoid internal to $ \C $} is a cocommutative
comonoid internal to $ \C\op $.
\end{definition}

In other words, we define comonoids exactly as we did
monoids in Definitions \ref{def:intern-monoid} and
\ref{def:intern-comm-monoid} except we turn the arrows
around.  Many familiar algebraic objects can be exhibited as
monoids internal to select categories.

\begin{example}

A monoid internal to $ \Set $ is an ordinary monoid. A
monoid internal to the category $ \Ab $ of abelian groups
is a ring. A monoid internal to a category $ [\C,\C] $ of
endofunctors is a monad on $ \C $.
\end{example}

As in algebra, objects can have multiple structures
simultaneously. The most important for us is the Frobenius

\begin{definition}[Frobenius monoid]
\label{def:frobenius-monoid}
An object $ (m,\mu,\eta,\delta,\epsilon) $ in a monoidal
category $ ( \C, \otimes , I ) $ is called a
\defn{Frobenius monoid} if $ ( m,\mu,\eta ) $ is a monoid
object, $ ( m,\delta,\epsilon ) $ is a comonoid structure
and the equation
\[
(\id \otimes \mu)
( \delta \otimes \id )
= \delta \mu
= ( \mu \otimes \id )
( \id \otimes \delta ).
\]
\end{definition}

% MAYBE I'LL FINISH THIS FROBENIUS STRING DIAGRAM
% FIGURE TIME PERMITTING. IF SO, REF IT FROM ZX-CALCULUS
% PARAGRAPH WHERE THEY ARE MENTIONED
% \begin{figure}
%   \centering
%   \fbox{
%     \begin{minipage}{1.0\linewidth}
%       A Frobenius monoid consists of the operations
%     \end{minipage}
%     \linebreak
%     \begin{minipage}{0.2\linewidth}
%       \begin{tikzpicture}
%         \node () at (-1,1) {$ \mu \bydef $};
%         \node (1) at (0,2) {};
%         \node (2) at (0,0) {};
%         \node (3) at (1,1) {};
%         \node (4) at (2,1) {};
%         \draw [line width=1cm]
%         (1.center) edge[bend left] (3.center)
%         (2.center) edge[bend right] (3.center)
%         (3.center) edge[] (4.center);
%       \end{tikzpicture}
%     \end{minipage}
%     \hfill
%     \begin{minipage}{0.2\linewidth}
%       \begin{tikzpicture}
%         \node () at (-1,1) {$ \eta \bydef $};
%         \node (1) at (0,1) {};
%         \node [draw=circle,fillblack] (2) at (1,1) {};
%         \draw [line width=1cm]
%         (1.center) edge (2.center);
%       \end{tikzpicture}
%     \end{minipage}
%     \begin{minipage}{0.2\linewidth}
%       \begin{tikzpicture}
%         \node () at (-1,1) {$ \delta \bydef $};
%         \node (1) at (2,2) {};
%         \node (2) at (2,0) {};
%         \node (3) at (1,1) {};
%         \node (4) at (0,1) {};
%         \draw [line width=1cm]
%         (3.center) edge[bend left] (1.center)
%         (3.center) edge[bend right] (2.center)
%         (3.center) edge[] (4.center);
%       \end{tikzpicture}
%     \end{minipage}
%     \hfill
%     \begin{minipage}{0.2\linewidth}
%       \begin{tikzpicture}
%         \node () at (-1,1) {$ \epsilon \bydef $};
%         \node (1) at (1,1) {};
%         \node [draw=circle,fillblack] (2) at (0,1) {};
%         \draw [line width=1cm]
%         (1.center) edge (2.center);
%       \end{tikzpicture}
%     \end{minipage}
%     \linebreak
%     % --------
%     \begin{minipage}{1.0\linewidth}
%       and satisfy the equations
%     \end{minipage}
%     \linebreak

%   \caption{String diagrams for Frobenius monoids}
%   \label{fig:string-for-frobenius}
%   }
% \end{figure}

Internalization can be extended to constructions beyond
monoids and their variants.  The most important construction
for us is the internalization of a category.

\begin{definition}[Internal category]

Let $ \D $ be a category. A \defn{category $ \CCC $
internal to $ \D $} consists of the data
\begin{itemize}
\item an object $ \CCC_0 \in \ob (\D) $ of \emph{objects} of $ \CCC $
\item an object $ \CCC_1 \in \ob (\D) $ of \emph{arrows} of $ \CCC $
\item source and target arrows $ s,t \from \CCC_1 \to \CCC_0
$ in $ \D $
\item an identity arrow $ e \from \CCC_0 \to \CCC_1 $ in $ \D $
\item a composition arrow $ \circ \from \CCC_1 \times_{\CCC_0}
\CCC_1 \to \CCC_1 $
\end{itemize}
together with commuting diagrams
\begin{itemize}
\item that specify the source and target of the identity
\[
\begin{tikzpicture}
\begin{scope}
\node (1) at (0,2) {$ \CCC_0 $};
\node (2) at (2,2) {$ \CCC_1 $};
\node (3) at (2,0) {$ \CCC_0 $};
\draw [cd] (1) to node[above]{$ e $}  (2);
\draw [cd] (1) to node[left]{$ \id $} (3);
\draw [cd] (2) to node[right]{$ s $}  (3);
\end{scope}
\begin{scope}[shift={(6,0)}]
\node (1) at (0,2) {$ \CCC_0 $};
\node (2) at (2,2) {$ \CCC_1 $};
\node (3) at (2,0) {$ \CCC_0 $};
\draw [cd] (1) to node[above]{$ e $}  (2);
\draw [cd] (1) to node[left]{$ \id $} (3);
\draw [cd] (2) to node[right]{$ t $}  (3);
\end{scope}
\end{tikzpicture}
\]
\item that specify the source and target of composite
\[
\begin{tikzpicture}
\begin{scope}
\node (1) at (0,2) {$ \CCC_1 \times_{\CCC_0} \CCC_1 $};
\node (2) at (3,2) {$ \CCC_1 $};
\node (3) at (0,0) {$ \CCC_1 $};
\node (4) at (3,0) {$ \CCC_0 $};
\draw [cd] (1) to node[above]{$ \circ $} (2);
\draw [cd] (1) to node[left]{$ p_1 $}    (3);
\draw [cd] (2) to node[right]{$ s $} (4);
\draw [cd] (3) to node[below]{$ s $} (4);
\end{scope}
\begin{scope}[shift={(6,0)}]
\node (1) at (0,2) {$ \CCC_1 \times_{\CCC_0} \CCC_1 $};
\node (2) at (3,2) {$ \CCC_1 $};
\node (3) at (0,0) {$ \CCC_1 $};
\node (4) at (3,0) {$ \CCC_0 $};
\draw [cd] (1) to node[above]{$ \circ $} (2);
\draw [cd] (1) to node[left]{$ p_2 $} (3);
\draw [cd] (2) to node[right]{$ t $} (4);
\draw [cd] (3) to node[below]{$ t $} (4);
\end{scope}
\end{tikzpicture}
\]
\item that specify associativity
\[
\begin{tikzpicture}
\node (1) at (0,2)
{$ \CCC_1 \times_{\CCC_0} \CCC_1 \times_{\CCC_0} \CCC_1 $};
\node (2) at (4,2) {$ \CCC_1 \times_{\CCC_0} \CCC_1 $};
\node (3) at (0,0) {$ \CCC_1 \times_{\CCC_0} \CCC_1 $};
\node (4) at (4,0) {$ \CCC_1 $};
\draw[cd]
(1) to node[above]{$ \circ \times_{\CCC_0} \id $} (2)
(1) to node[left]{$ \id \times_{\CCC_0} \circ $} (3)
(2) to node[right]{$ \circ $} (4)
(3) to node[below]{$ \circ $} (4);
\end{tikzpicture}
\]
\item that specify unit laws
\[
\begin{tikzpicture}
\node (1) at (-4,2) {$ \CCC_0 \times_{\CCC_0} \CCC_1 $};
\node (2) at (0,2) {$ \CCC_1 \times_{\CCC_0} \CCC_1 $};
\node (3) at (4,2) {$ \CCC_1 \times_{\CCC_0} \CCC_0 $};
\node (4) at (0,0) {$ \CCC_0 $};
\draw [cd]
(1) to node[above]{$ e \times_{\CCC_0} \id $} (2)
(3) to node[above]{$ \id \times_{\CCC_0} e $} (2)
(1) to node[below]{$ p_2 $} (4)
(3) to node[below]{$ p_1 $} (4);
\end{tikzpicture}
\]
\end{itemize}
If we are instead working in an ambient 2-category $ \D $
and the diagrams only commute up to natural isomorphism,
we say that $ \CCC $ is \defn{weakly internal} to $ \D
\end{definition}

The most important example of an internal category for us is
a (pseudo) double category. A \defn{(pseudo) double
category} $ \CCC $ is a category weakly internal to
$ \Cat $. This can be unpacked.

Roughly, a double category consists of two categories $
\CCC_0 $ and $ \CCC_1 $ that we consider as follows.
\begin{itemize}
\item The $ \CCC_0 $-objects are called the
objects of $ \CCC $.
\item The $ \CCC_0 $-arrows are called the
vertical arrows in $ \CCC $.
\item The $ \CCC_1 $-objects are called the the
horizontal arrows in $ \CCC $.
\item The $ \CCC_1 $-arrows are called the squares
of $ \CCC $.
\end{itemize}

This data is depicted in Figure \ref{fig:square}. When the
vertical arrows are both identities, we call the square
\defn{globular}.

Double categories often arise when a mathematical object
has two different sorts of morphisms. One morphism type
becomes the horizontal arrows, which we denote by $ \hto $,
and the other morphism type becomes the vertical arrows,
which we denote by $ \to $.

\begin{example}
\label{ex:sets-rel-dbl-cat}
There is a double category whose objects are sets,
vertical arrows $ f \from x \to y $ are functions, horizontal
arrows $r \from x \hto y $ are relations $ r \subseteq x
\times y $, and squares
\[
\begin{tikzpicture}
\node (1) at (0,2) {$ x $};
\node (2) at (2,2) {$ y $};
\node (3) at (0,0) {$ x' $};
\node (4) at (2,0) {$ y' $};
\draw [cd] (1) to node[above]{$ r $} (2);
\draw [cd] (1) to node[left]{$ f $} (3);
\draw [cd] (2) to node[right]{$ g $} (4);
\draw [cd] (3) to node[below]{$ s $} (4);
\node () at (1,1) {$ \Downarrow $};
\end{tikzpicture}
\]
are inclusions of relations $ gr \subseteq sf  $.
\end{example}

\begin{figure}[h]
\centering
\fbox{
\begin{minipage}{\linewidth}
\[
\begin{tikzpicture}
\node (1) at (0,2) {\( c \)};
\node (2) at (2,2) {\( d \)};
\node (3) at (0,0) {\( c' \)};
\node (4) at (2,0) {\( d' \)};
\draw [cd,-|->] (1) to node[above]{\( m \)} (2);
\draw [cd] (1) to node[left]{\( f \)} (3);
\draw [cd] (2) to node[right]{\( g \)} (4);
\draw [-|->] (3) to node[below]{\( n \)} (4);
\node (5) at (6,2) {\( c,c',d,d' \in \ob ( \C_0 ) \)};
\node (6) at (6,1.33) {\( f,g \in \arr ( \C_0 ) \)};
\node (7) at (6,.66) {\( m,n \in \ob ( \C_1 ) \)};
\node (8) at (1,1) {\( \Downarrow  \theta \)};
\node (9) at (6,0) {\( \theta \in \arr ( \C_1 ) \)};
\end{tikzpicture}
\]
\caption{A square in a double category}
\label{fig:square}
\end{minipage}
\end{figure}

The first definition for a double category we gave---a
category weakly internal to $ \Cat $---is too terse to
provide much meaningful interpretation. So we unpack it.

\begin{definition}[Double category]
\label{def:dbl-cat}
A \defn{pseudo double category} $\CCC$, or simply
\defn{double category}, consists of a category of objects
$\CCC_{0}$ and a category of arrows $\CCC_{1}$
together with the following functors
\begin{align*}
U     & \from \CCC_{0} \to \CCC_{1}, \\
S,T   & \from \CCC_{1} \to \CCC_{0},  \\
\odot & \from \CCC_{1} \times_{\CCC_{0}} \CCC_{1} \to \CCC_{1}
\end{align*}
where the pullback $\CCC_{1} \times_{\CCC_{0}} \CCC_{1}$
is taken over $S$ and $T$.  These functors satisfy the
\begin{align}
SUa = a & = TUa \\
S(x \odot y) & = Sy \\
T(x \odot y) & = Tx.
\end{align}
This also comes equipped with natural
\begin{align}
\alpha  & \from (x \odot y) \odot z \to
x \odot (y \odot z) \\
\lambda & \from Ua \odot x \to x \\
\rho    & \from x \odot Ua \to x
\end{align}
such that $S(\alpha)$, $S(\lambda)$, $S(\rho)$,
$T(\alpha)$, $T(\lambda)$, and $T(\rho)$ are
each identities and that the coherence axioms of
a monoidal category are satisfied.\footnote{
Sometimes the term \defn{horizontal
1-cell} is used for these
[58], and for good
reason. A $(n \times 1)$-category consists of
categories $\mathbf{D_i}$ for
$0 \leq i \leq n$ where the objects of
$\mathbf{D_i}$ are $i$-cells and the morphisms
of $\mathbf{D_i}$ are vertical
$i+1$-morphisms. A double category is then
just a $(1 \times 1)$-category. From this
perspective, `cells' are always objects with
morphisms going between them.}

As for notation, we write vertical and
horizontal morphisms with the arrows $\to$ and
$\hto$, respectively, and 2-morphisms we draw as
in Figure \ref{fig:square}.

One can define double functors and double transformations,
but we refrain having no need of them in this thesis.
Double categories, double functors, and double
transformations form a 2-category $ \DblCat $.
\end{definition}

Like categories, we can equip double categories with
additional structure. We focus on adding a monoidal
structure. As is typical in category theory, we can provide
definitions at various levels of abstraction.  As such, a
symmetric monoidal double category is a monoid weakly
internal to $ \DblCat $.  This uses the same definition of a
monoid internal to a category $ \D $ as above, though the
diagrams commute up to invertible transformation. It is
worth unpacking this definition.

\begin{definition}[Monoidal double category] \label{def:mndl-dbl-cats}
A \defn{monoidal double category} $ ( \CCC, \otimes ) $ is a double category
$\CCC$ equipped with a functor $ \otimes \from \CCC \times
\CCC \to \CCC $ such that
\begin{enumerate}
\item $\CCC_{0}$ and $\CCC_{1}$ are
both monoidal categories.
\item If $I$ is the monoidal unit of
$\CCC_{0}$, then $U_I$ is the monoidal
unit of $\CCC_{1}$.
\item The functors $S$ and $T$ are strict
monoidal and preserve the associativity and
unit constraints.
\item There are globular 2-isomorphisms
\[
\mathfrak{x} \from
(x \otimes y) \odot (x' \otimes y')
\to
(x \odot x') \otimes (y \odot y')
\]
\[
\mathfrak{u} \from
U(a \otimes b)
\to
Ua \otimes Ub
\]

\item \label{diag:MonDblCat}

The following diagrams that express the constraint data
for the double functor $\otimes$ commute
\[
\begin{tikzpicture}[scale=0.9]
\node (A) at (0,3) {\scriptsize{
$((x \otimes y )\odot (x'\otimes y')) \odot (x'' \otimes y'')$}
\node (B) at (9,3) {\scriptsize{
$((x \odot x')\otimes (y \odot y')) \odot (x'' \otimes y'') $}
\node (A') at (0,1.5) {\scriptsize{
$(x \otimes y) \odot ((x' \otimes y') \odot (x''\otimes y'')) $}
\node (B') at (9,1.5) {\scriptsize{
$((x \odot x')\odot x'') \otimes ((y\odot y')\odot y'')$}
\node (A'') at (0,0) {\scriptsize{
$(x\otimes y) \odot ((x'\odot x'') \otimes (y'\odot y''))$}
\node (B'') at (9,0) {\scriptsize{
$(x\odot (x'\odot x'')) \otimes (y\odot (y' \odot y''))$}
\path[cd,font=\scriptsize]
(A) edge node[left]{$\alpha$} (A')
(A') edge node[left]{$1 \odot \mathfrak{x}$} (A'')
(B) edge node[right]{$\mathfrak{x}$} (B')
(B') edge node[right]{$\alpha \otimes \alpha$} (B'')
(A) edge node[above]{$\mathfrak{x} \odot 1$} (B)
(A'') edge node[above]{$\mathfrak{x}$} (B'');
\end{tikzpicture}
\]
\[
\begin{tikzpicture}[scale=0.9]
\node (UL) at (0,1.5) {\scriptsize{
$(x\otimes y) \odot U(a\otimes b)$}
\node (LL) at (0,0) {\scriptsize{
$ x \otimes y$}
\node (UR) at (4.5,1.5) {\scriptsize{
$(x\otimes y)\odot (Ua\otimes Ub)$}
\node (LR) at (4.5,0) {\scriptsize{
$(x\odot Ua) \otimes (y\odot Ub)$}
\path[cd,font=\scriptsize]
(UL) edge node[above]{$1 \odot \mathfrak{u}$} (UR)
(UL) edge node[left]{$\rho$} (LL)
(LR) edge node[above]{$\rho \otimes \rho$} (LL)
(UR) edge node[right]{$\mathfrak{x}$} (LR);
\end{tikzpicture}
\begin{tikzpicture}[scale=0.9]
\node (UL) at (0,1.5) {\scriptsize{$U(a\otimes b)\odot (x\otimes y)$}};
\node (LL) at (0,0) {\scriptsize{$x\otimes y$}};
\node (UR) at (4.5,1.5) {\scriptsize{$(Ua \otimes Ub)\odot (x\otimes y)$}};
\node (LR) at (4.5,0) {\scriptsize{$(Ua \odot x) \otimes (Ub \odot y)$}};
\path[cd,font=\scriptsize]
(UL) edge node[above]{$\mathfrak{u} \odot 1$} (UR)
(UL) edge node[left]{$\lambda$} (LL)
(LR) edge node[above]{$\lambda \otimes \lambda$} (LL)
(UR) edge node[right]{$\mathfrak{x}$} (LR);
\end{tikzpicture}
\]
\item The following diagrams commute expressing
the associativity isomorphism for $\otimes$ is
a transformation of double categories.
\[
\begin{tikzpicture}[scale=0.9]
\node (A) at (0,3) {\scriptsize{
$((x\otimes y) \otimes z) \odot ((x' \otimes y')\otimes z')$}
\node (B) at (9,3) {\scriptsize{
$(x\otimes (y\otimes z)) \odot (x'\otimes (y'\otimes z'))$}
\node (A') at (0,1.5) {\scriptsize{
$((x\otimes y) \odot (x'\otimes y')) \otimes (z\odot z')$}
\node (B') at (9,1.5) {\scriptsize{
$(x\odot x') \otimes ((y\otimes z)\odot (y'\otimes z'))$}
\node (A'') at (0,0) {\scriptsize{
$((x\odot x') \otimes(y\odot y')) \otimes (z\odot z')$}
\node (B'') at (9,0) {\scriptsize{
$(x\odot x') \otimes ((y\odot y')\otimes (z\odot z'))$}
\path[cd,font=\scriptsize]
(A) edge node[left]{$\mathfrak{x}$} (A')
(A') edge node[left]{$\mathfrak{x} \otimes 1$} (A'')
(B) edge node[right]{$\mathfrak{x}$} (B')
(B') edge node[right]{$1 \otimes \mathfrak{x}$} (B'')
(A) edge node[above]{$a \odot a$} (B)
(A'') edge node[above]{$a$} (B'');
\end{tikzpicture}
\]
\[
\begin{tikzpicture}
\node (A) at (0,3)
{\scriptsize{ $ U ( (a \otimes b) \otimes c ) $ }};
\node (B) at (4,3)
{\scriptsize{ $ U ( a \otimes (b \otimes c) ) $ }};
\node (A') at (0,1.5) {\scriptsize{$U(a\otimes b) \otimes Uc $}};
\node (B') at (4,1.5) {\scriptsize{$Ua \otimes U(b\otimes c)$}};
\node (A'') at (0,0) {\scriptsize{$(Ua \otimes Ub)\otimes Uc$}};
\node (B'') at (4,0) {\scriptsize{$Ua\otimes (Ub\otimes Uc) $}};
\path[cd,font=\scriptsize]
(A) edge node[left]{$\mathfrak{u}$} (A')
(A') edge node[left]{$\mathfrak{u} \otimes 1$} (A'')
(B) edge node[right]{$\mathfrak{u}$} (B')
(B') edge node[right]{$\id \otimes \mathfrak{u}$} (B'')
(A) edge node[above]{$Ua$} (B)
(A'') edge node[above]{$a$} (B'');
\end{tikzpicture}
\]
\item The following diagrams commute expressing
that the unit isomorphisms for $\otimes$ are
transformations of double categories.
\[
\begin{tikzpicture}
\node (A) at (0,1.5) {\scriptsize{$(x\otimes UI)\odot (y\otimes UI)$}};
\node (A') at (0,0) {\scriptsize{$x\odot y$}};
\node (B) at (4,1.5) {\scriptsize{$(x\odot y)\otimes (UI \odot UI) $}};
\node (B') at (4,0) {\scriptsize{$(x\odot y)\otimes UI $}};
\path[cd,font=\scriptsize]
(A) edge node[left]{$r \odot r$} (A')
(A) edge node[above]{$\mathfrak{x}$} (B)
(B) edge node[right]{$1 \otimes \rho$} (B')
(B') edge node[above]{$r$} (A');
\end{tikzpicture}
\quad
\begin{tikzpicture}
\node (A) at (0,0.75) {\scriptsize{$U(a \otimes I) $}};
\node (B) at (1.5,1.5) {\scriptsize{$Ua \otimes UI $}};
\node (B') at (1.5,0) {\scriptsize{$Ua$}};
\path[cd,font=\scriptsize]
(A) edge node[above]{$\mathfrak{u}$} (B)
(A) edge node[below]{$U_{r}$} (B')
(B) edge node[right]{$r$} (B');
\end{tikzpicture}
\]
\[
\begin{tikzpicture}
\node (A) at (0,1.5) {\scriptsize{$(UI \otimes x)\odot (UI\otimes y)$}};
\node (A') at (0,0) {\scriptsize{$x\odot y$}};
\node (B) at (4,1.5) {\scriptsize{$(UI \odot UI) \otimes (x\odot y)$}};
\node (B') at (4,0) {\scriptsize{$UI\otimes (x \odot y) $}};
\path[cd,font=\scriptsize]