\draw (0.center) to (3.center);
\draw [in=90, out=-150, looseness=1.00] (4) to (6.center);
\draw (5.center) to (7);
\draw [in=-30, out=90, looseness=1.00] (7) to (4);
\draw (10.center) to (9);
\draw (9) to (4);
\end{pgfonlayer}
\end{tikzpicture}
\]

* $(i) \Rightarrow (iii)$: Here is the proof assuming [nat.1](a) that $\alpha_\ox \alpha_\oa = 1$:

\[ \hspace{-0.75cm}
\begin{tikzpicture} %dag15
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (0.5, 3.5) {};
\node [style=none] (1) at (0.5, -2) {};
\node [style=none] (2) at (0, 3.25) {$F(X)$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (0.center) to (1.center);
\end{pgfonlayer}
\end{tikzpicture} =
\begin{tikzpicture} %dag14
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (0.5, 3.5) {};
\node [style=none] (1) at (0.5, -2) {};
\node [style=none] (2) at (0, 2.5) {};
\node [style=none] (3) at (0, -1) {};
\node [style=none] (4) at (1.5, -1) {};
\node [style=none] (5) at (1.5, 2.5) {};
\node [style=none] (6) at (1.25, -0.5) {$F$};
\node [style=none] (7) at (0.25, -1) {};
\node [style=none] (8) at (0.75, -1) {};
\node [style=none] (9) at (0, 3.25) {$F(X)$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (0.center) to (1.center);
\draw (2.center) to (5.center);
\draw (5.center) to (4.center);
\draw (4.center) to (3.center);
\draw (3.center) to (2.center);
\draw [bend left=90, looseness=1.25] (7.center) to (8.center);
\end{pgfonlayer}
\end{tikzpicture} =
\begin{tikzpicture} %dag13
\begin{pgfonlayer}{nodelayer}
\node [style=circle] (0) at (1.75, 1.25) {$\top$};
\node [style=circle] (1) at (1.75, -0) {$\top$};
\node [style=none] (2) at (0.5, 3.5) {};
\node [style=none] (3) at (0.5, -2) {};
\node [style=circle, scale=0.5] (4) at (0.5, -0.75) {};
\node [style=none] (5) at (0, 2) {};
\node [style=none] (6) at (0, -1.5) {};
\node [style=none] (7) at (2.5, -1.5) {};
\node [style=none] (8) at (2.5, 2) {};
\node [style=none] (9) at (2.25, -1) {$F$};
\node [style=none] (10) at (0.25, -1.5) {};
\node [style=none] (11) at (0.75, -1.5) {};
\node [style=none] (12) at (0, 3.25) {$F(X)$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (2.center) to (3.center);
\draw [dotted, in=0, out=-90, looseness=1.25] (1) to (4);
\draw (5.center) to (8.center);
\draw (8.center) to (7.center);
\draw (7.center) to (6.center);
\draw (6.center) to (5.center);
\draw [bend left=90, looseness=1.25] (10.center) to (11.center);
\draw (0) to (1);
\end{pgfonlayer}
\end{tikzpicture} =
\begin{tikzpicture} %dag12
\begin{pgfonlayer}{nodelayer}
\node [style=circle] (0) at (2, 2) {$\top$};
\node [style=circle] (1) at (2, -0) {$\top$};
\node [style=none] (2) at (0.5, 3.5) {};
\node [style=none] (3) at (0.5, -2) {};
\node [style=circle, scale=0.5] (4) at (0.5, -0.75) {};
\node [style=none] (5) at (0, 0.5) {};
\node [style=none] (6) at (0, -1.5) {};
\node [style=none] (7) at (2.5, -1.5) {};
\node [style=none] (8) at (2.5, 0.5) {};
\node [style=none] (9) at (1.5, 2.5) {};
\node [style=none] (10) at (3, 2.5) {};
\node [style=none] (11) at (1.5, 1.25) {};
\node [style=none] (12) at (3, 1.25) {};
\node [style=none] (13) at (2.25, -1.25) {$F$};
\node [style=none] (14) at (0.25, -1.5) {};
\node [style=none] (15) at (0.75, -1.5) {};
\node [style=none] (16) at (1.75, 1.25) {};
\node [style=none] (17) at (2.25, 1.25) {};
\node [style=none] (18) at (0, 3.25) {$F(X)$};
\node [style=none] (19) at (2.75, 1.5) {$F$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (2.center) to (3.center);
\draw [dotted, in=0, out=-90, looseness=1.25] (1) to (4);
\draw (5.center) to (8.center);
\draw (8.center) to (7.center);
\draw (7.center) to (6.center);
\draw (6.center) to (5.center);
\draw (9.center) to (11.center);
\draw (11.center) to (12.center);
\draw (12.center) to (10.center);
\draw (10.center) to (9.center);
\draw [bend left=90, looseness=1.25] (14.center) to (15.center);
\draw [bend left=90, looseness=1.25] (16.center) to (17.center);
\draw (0) to (1);
\end{pgfonlayer}
\end{tikzpicture}
\begin{tikzpicture} %dag10
\begin{pgfonlayer}{nodelayer}
\node [style=circle] (0) at (2, 1.25) {$\alpha_\oa$};
\node [style=circle] (1) at (2, 2.75) {$\top$};
\node [style=circle] (2) at (2, -0.25) {$\top$};
\node [style=none] (3) at (0.5, 3.5) {};
\node [style=none] (4) at (0.5, -2) {};
\node [style=circle, scale=0.5] (5) at (0.5, -1) {};
\node [style=none] (6) at (0, 0.25) {};
\node [style=none] (7) at (0, -1.5) {};
\node [style=none] (8) at (2.5, -1.5) {};
\node [style=none] (9) at (2.5, 0.25) {};
\node [style=none] (10) at (1.5, 3.25) {};
\node [style=none] (11) at (3, 3.25) {};
\node [style=none] (12) at (1.5, 2) {};
\node [style=none] (13) at (3, 2) {};
\node [style=none] (14) at (2.25, -1.25) {$F$};
\node [style=none] (15) at (0.25, -1.5) {};
\node [style=none] (16) at (0.75, -1.5) {};
\node [style=none] (17) at (1.75, 2) {};
\node [style=none] (18) at (2.25, 2) {};
\node [style=none] (19) at (2.75, 2.25) {$G$};
\node [style=none] (20) at (0, 3.25) {$F(X)$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (1) to (0);
\draw (0) to (2);
\draw (3.center) to (4.center);
\draw [dotted, in=0, out=-90, looseness=1.25] (2) to (5);
\draw (6.center) to (9.center);
\draw (9.center) to (8.center);
\draw (8.center) to (7.center);
\draw (7.center) to (6.center);
\draw (10.center) to (12.center);
\draw (12.center) to (13.center);
\draw (13.center) to (11.center);
\draw (11.center) to (10.center);
\draw [bend left=105, looseness=1.00] (15.center) to (16.center);
\draw [bend left=90, looseness=1.25] (17.center) to (18.center);
\end{pgfonlayer}
\end{tikzpicture}=
\begin{tikzpicture} %dag10
\begin{pgfonlayer}{nodelayer}
\node [style=circle] (0) at (2, 1.25) {$\alpha_\oa$};
\node [style=circle] (1) at (2, 2.75) {$\top$};
\node [style=circle] (2) at (2, -0.25) {$\top$};
\node [style=none] (3) at (0.5, 3.5) {};
\node [style=none] (4) at (0.5, -2) {};
\node [style=circle, scale=0.5] (5) at (0.5, -1) {};
\node [style=none] (6) at (0, 0.5) {};
\node [style=none] (7) at (0, -1.5) {};
\node [style=none] (8) at (2.5, -1.5) {};
\node [style=none] (9) at (2.5, 0.5) {};
\node [style=none] (10) at (1.5, 3.25) {};
\node [style=none] (11) at (3, 3.25) {};
\node [style=none] (12) at (1.5, 2) {};
\node [style=none] (13) at (3, 2) {};
\node [style=none] (14) at (2.25, -1.25) {$F$};
\node [style=none] (15) at (1.75, 0.5) {};
\node [style=none] (16) at (2.25, 0.5) {};
\node [style=none] (17) at (1.75, 2) {};
\node [style=none] (18) at (2.25, 2) {};
\node [style=none] (19) at (2.75, 2.25) {$G$};
\node [style=none] (20) at (0, 3.25) {$F(X)$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (1) to (0);
\draw (0) to (2);
\draw (3.center) to (4.center);
\draw [dotted, in=0, out=-90, looseness=1.25] (2) to (5);
\draw (6.center) to (9.center);
\draw (9.center) to (8.center);
\draw (8.center) to (7.center);
\draw (7.center) to (6.center);
\draw (10.center) to (12.center);
\draw (12.center) to (13.center);
\draw (13.center) to (11.center);
\draw (11.center) to (10.center);
\draw [bend right=105, looseness=1.00] (15.center) to (16.center);
\draw [bend left=90, looseness=1.25] (17.center) to (18.center);
\end{pgfonlayer}
\end{tikzpicture} =
\begin{tikzpicture} %dag11
\begin{pgfonlayer}{nodelayer}
\node [style=circle] (0) at (1.75, 3) {$\top$};
\node [style=circle] (1) at (1.75, 0.75) {$\top$};
\node [style=none] (2) at (0.5, 3.5) {};
\node [style=none] (3) at (0.5, -2.5) {};
\node [style=circle, scale=0.5] (4) at (0.5, -0) {};
\node [style=none] (5) at (0, 1.5) {};
\node [style=none] (6) at (0, -0.75) {};
\node [style=none] (7) at (2.25, -0.75) {};
\node [style=none] (8) at (2.25, 1.5) {};
\node [style=none] (9) at (1.25, 3.5) {};
\node [style=none] (10) at (2.75, 3.5) {};
\node [style=none] (11) at (1.25, 2) {};
\node [style=none] (12) at (2.75, 2) {};
\node [style=none] (13) at (2, -0.5) {$G$};
\node [style=circle, scale=2] (14) at (0.5, 2.5) {};
\node [style=circle, scale=2] (15) at (0.5, -1.5) {};
\node [style=none] (16) at (0.5, 2.5) {$\alpha_\ox$};
\node [style=none] (17) at (0.5, -1.5) {$\alpha_\oa$};
\node [style=none] (18) at (2.5, 2.25) {$F$};
\node [style=none] (19) at (1.5, 2) {};
\node [style=none] (20) at (2, 2) {};
\node [style=none] (21) at (-0.3, 3.25) {$F(X)$};
\node [style=none] (24) at (-0.3, -2) {$F(X)$};
\node [style=none] (25) at (2, 1.5) {};
\node [style=none] (26) at (1.5, 1.5) {};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw [dotted, in=0, out=-105, looseness=1.25] (1) to (4);
\draw (5.center) to (8.center);
\draw (8.center) to (7.center);
\draw (7.center) to (6.center);
\draw (6.center) to (5.center);
\draw (9.center) to (11.center);
\draw (11.center) to (12.center);
\draw (12.center) to (10.center);
\draw (10.center) to (9.center);
\draw (0) to (1);
\draw (2.center) to (14);
\draw (14) to (4);
\draw (4) to (15);
\draw (15) to (3.center);
\draw [bend left=75, looseness=1.50] (19.center) to (20.center);
\draw [bend right=75, looseness=1.50] (26.center) to (25.center);
\end{pgfonlayer}
\end{tikzpicture} =
\begin{tikzpicture} %dag11
\begin{pgfonlayer}{nodelayer}
\node [style=circle] (0) at (1.75, 3) {$\top$};
\node [style=circle] (1) at (1.75, 0.75) {$\top$};
\node [style=none] (2) at (0.5, 3.5) {};
\node [style=none] (3) at (0.5, -2.5) {};
\node [style=circle, scale=0.5] (4) at (0.5, -0) {};
\node [style=none] (5) at (0, 1.5) {};
\node [style=none] (6) at (0, -0.75) {};
\node [style=none] (7) at (2.25, -0.75) {};
\node [style=none] (8) at (2.25, 1.5) {};
\node [style=none] (9) at (1.25, 3.5) {};
\node [style=none] (10) at (2.75, 3.5) {};
\node [style=none] (11) at (1.25, 2) {};
\node [style=none] (12) at (2.75, 2) {};
\node [style=none] (13) at (2, -0.5) {$G$};
\node [style=circle, scale=2] (14) at (0.5, 2.5) {};
\node [style=circle, scale=2] (15) at (0.5, -1.5) {};
\node [style=none] (16) at (0.5, 2.5) {$\alpha_\ox$};
\node [style=none] (17) at (0.5, -1.5) {$\alpha_\oa$};
\node [style=none] (18) at (2.5, 2.25) {$G$};
\node [style=none] (19) at (1.5, 2) {};
\node [style=none] (20) at (2, 2) {};
\node [style=none] (21) at (-0.3, 3.25) {$F(X)$};
\node [style=none] (24) at (-0.3, -2) {$F(X)$};
\node [style=none] (25) at (0.75, -0.75) {};
\node [style=none] (26) at (0.25, -0.75) {};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw [dotted, in=0, out=-105, looseness=1.25] (1) to (4);
\draw (5.center) to (8.center);
\draw (8.center) to (7.center);
\draw (7.center) to (6.center);
\draw (6.center) to (5.center);
\draw (9.center) to (11.center);
\draw (11.center) to (12.center);
\draw (12.center) to (10.center);
\draw (10.center) to (9.center);
\draw (0) to (1);
\draw (2.center) to (14);
\draw (14) to (4);
\draw (4) to (15);
\draw (15) to (3.center);
\draw [bend left=75, looseness=1.50] (19.center) to (20.center);
\draw [bend left=75, looseness=1.50] (26.center) to (25.center);
\end{pgfonlayer}
\end{tikzpicture} = \begin{tikzpicture} %dag16
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (0.5, 3.5) {};
\node [style=none] (1) at (0.5, -2) {};
\node [style=none] (2) at (0, 3.25) {$F(X)$};
\node [style=circle] (3) at (0.5, 2) {$\alpha_\ox$};
\node [style=circle] (4) at (0.5, -0) {$\alpha_\oa$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (0.center) to (3);
\draw (3) to (4);
\draw (4) to (1.center);
\end{pgfonlayer}
\end{tikzpicture}
\]

if either $\alpha_\ox$ or $\alpha_\oa$ are isomorphisms this implies $\alpha_\oa \alpha_\ox =1$.

* $(ii) \Rightarrow (iii)$:
The assumption of [nat.1](a) or (b) yields, as above, that $\alpha_\ox \alpha_\oa =1$:
using [nat.2](c) for example gives $\alpha_\oa \alpha_\ox =1$:

\[
\begin{tikzpicture} %dag10
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (0.5, 3.5) {};
\node [style=none] (1) at (0.5, -2) {};
\node [style=none] (2) at (0, 3.25) {$G(X)$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (0.center) to (1.center);
\end{pgfonlayer}
\end{tikzpicture}=
\begin{tikzpicture} %dag14
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (0.5, 3.5) {};
\node [style=none] (1) at (0.5, -2) {};
\node [style=none] (2) at (0, 2.5) {};
\node [style=none] (3) at (0, -1) {};
\node [style=none] (4) at (1.5, -1) {};
\node [style=none] (5) at (1.5, 2.5) {};
\node [style=none] (6) at (1.25, -0.5) {$G$};
\node [style=none] (7) at (0.25, 2.5) {};
\node [style=none] (8) at (0.75, 2.5) {};
\node [style=none] (9) at (0, 3.25) {$G(X)$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (0.center) to (1.center);
\draw (2.center) to (5.center);
\draw (5.center) to (4.center);
\draw (4.center) to (3.center);
\draw (3.center) to (2.center);
\draw [bend right=90, looseness=1.25] (7.center) to (8.center);
\end{pgfonlayer}
\end{tikzpicture} =
\begin{tikzpicture} %dag12b
\begin{pgfonlayer}{nodelayer}
\node [style=circle] (0) at (1.75, -1) {$\bot$};
\node [style=circle] (1) at (1.75, 1) {$\bot$};
\node [style=none] (2) at (0.5, -2.5) {};
\node [style=none] (3) at (0.5, 3.5) {};
\node [style=circle, scale=0.5] (4) at (0.5, 1.75) {};
\node [style=none] (5) at (0, 0.5) {};
\node [style=none] (6) at (0, 2.5) {};
\node [style=none] (7) at (2.5, 2.5) {};
\node [style=none] (8) at (2.5, 0.5) {};
\node [style=none] (9) at (1.25, -1.5) {};
\node [style=none] (10) at (2.75, -1.5) {};
\node [style=none] (11) at (1.25, -0.25) {};
\node [style=none] (12) at (2.75, -0.25) {};
\node [style=none] (13) at (2.25, 0.75) {$G$};
\node [style=none] (14) at (0.25, 2.5) {};
\node [style=none] (15) at (0.75, 2.5) {};
\node [style=none] (16) at (1.5, -0.25) {};
\node [style=none] (17) at (2, -0.25) {};
\node [style=none] (18) at (2.5, -1.25) {$G$};
\node [style=none] (19) at (0, 3.25) {$G(X)$};
\node [style=none] (20) at (0, -2) {$G(X)$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw [dotted, in=0, out=90, looseness=1.25] (1) to (4);
\draw (5.center) to (8.center);
\draw (8.center) to (7.center);
\draw (7.center) to (6.center);
\draw (6.center) to (5.center);
\draw (9.center) to (11.center);
\draw (11.center) to (12.center);
\draw (12.center) to (10.center);
\draw (10.center) to (9.center);
\draw [bend right=90, looseness=1.50] (14.center) to (15.center);
\draw [bend right=90, looseness=1.25] (16.center) to (17.center);
\draw (3.center) to (4);
\draw (4) to (2.center);
\draw (1) to (0);
\end{pgfonlayer}
\end{tikzpicture} =
\begin{tikzpicture} %dag11b
\begin{pgfonlayer}{nodelayer}
\node [style=circle] (0) at (1.75, -1.75) {$\bot$};
\node [style=circle] (1) at (1.75, 1) {$\bot$};
\node [style=none] (2) at (0.5, -2.5) {};
\node [style=none] (3) at (0.5, 3.5) {};
\node [style=circle, scale=0.5] (4) at (0.5, 1.75) {};
\node [style=none] (5) at (0, 0.5) {};
\node [style=none] (6) at (0, 2.5) {};
\node [style=none] (7) at (2.5, 2.5) {};
\node [style=none] (8) at (2.5, 0.5) {};
\node [style=none] (9) at (1.25, -2.25) {};
\node [style=none] (10) at (2.75, -2.25) {};
\node [style=none] (11) at (1.25, -1) {};
\node [style=none] (12) at (2.75, -1) {};
\node [style=none] (13) at (2.25, 0.75) {$G$};
\node [style=none] (14) at (0.25, 2.5) {};
\node [style=none] (15) at (0.75, 2.5) {};
\node [style=none] (16) at (1.5, -1) {};
\node [style=none] (17) at (2, -1) {};
\node [style=none] (18) at (2.5, -2) {$F$};
\node [style=none] (19) at (0, 3.25) {$G(X)$};
\node [style=none] (20) at (0, -2) {$G(X)$};
\node [style=circle] (21) at (1.75, -0.25) {$\alpha_\oa$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw [dotted, in=0, out=90, looseness=1.25] (1) to (4);
\draw (5.center) to (8.center);
\draw (8.center) to (7.center);
\draw (7.center) to (6.center);
\draw (6.center) to (5.center);
\draw (9.center) to (11.center);
\draw (11.center) to (12.center);
\draw (12.center) to (10.center);
\draw (10.center) to (9.center);
\draw [bend right=90, looseness=1.50] (14.center) to (15.center);
\draw [bend right=90, looseness=1.25] (16.center) to (17.center);
\draw (3.center) to (4);
\draw (4) to (2.center);
\draw (1) to (21);
\draw (21) to (0);
\end{pgfonlayer}
\end{tikzpicture}  =
\begin{tikzpicture} %dag10b
\begin{pgfonlayer}{nodelayer}
\node [style=circle] (0) at (1.75, -1.75) {$\bot$};
\node [style=circle] (1) at (1.75, 0.5) {$\bot$};
\node [style=none] (2) at (0.5, -2.5) {};
\node [style=none] (3) at (0.5, 3.5) {};
\node [style=circle, scale=0.5] (4) at (0.5, 1.25) {};
\node [style=none] (5) at (0, -0) {};
\node [style=none] (6) at (0, 2) {};
\node [style=none] (7) at (2.5, 2) {};
\node [style=none] (8) at (2.5, -0) {};
\node [style=none] (9) at (1.25, -2.25) {};
\node [style=none] (10) at (2.75, -2.25) {};
\node [style=none] (11) at (1.25, -1) {};
\node [style=none] (12) at (2.75, -1) {};
\node [style=none] (13) at (2.25, 0.25) {$F$};
\node [style=none] (14) at (0.25, 2) {};
\node [style=none] (15) at (0.75, 2) {};
\node [style=none] (16) at (1.5, -1) {};
\node [style=none] (17) at (2, -1) {};
\node [style=circle] (18) at (0.5, 2.75) {$\alpha_\oa$};
\node [style=circle] (19) at (0.5, -1.25) {$\alpha_\ox$};
\node [style=none] (20) at (2.5, -2) {$F$};
\node [style=none] (21) at (0, 3.5) {$G(X)$};
\node [style=none] (22) at (0, -2) {$G(X)$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw [dotted, in=0, out=90, looseness=1.25] (1) to (4);
\draw (5.center) to (8.center);
\draw (8.center) to (7.center);
\draw (7.center) to (6.center);
\draw (6.center) to (5.center);
\draw (9.center) to (11.center);
\draw (11.center) to (12.center);
\draw (12.center) to (10.center);
\draw (10.center) to (9.center);
\draw [bend right=90, looseness=1.50] (14.center) to (15.center);
\draw [bend right=90, looseness=1.25] (16.center) to (17.center);
\draw (1) to (0);
\draw (3.center) to (18);
\draw (18) to (4);
\draw (4) to (19);
\draw (19) to (2.center);
\end{pgfonlayer}
\end{tikzpicture} =  \begin{tikzpicture} %dag16
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (0.5, 3.5) {};
\node [style=none] (1) at (0.5, -2) {};
\node [style=none] (2) at (0, 3.25) {$G(X)$};
\node [style=circle] (3) at (0.5, 2) {$\alpha_\oa$};
\node [style=circle] (4) at (0.5, -0) {$\alpha_\ox$};
\node [style=none] (5) at (0, -1.5) {$G(X)$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (0.center) to (3);
\draw (3) to (4);
\draw (4) to (1.center);
\end{pgfonlayer}
\end{tikzpicture}
\]

Since, $\alpha_\ox \alpha_\oa = 1$ and $\alpha_\ox \alpha_\oa = 1$ we have $\alpha_\ox = \alpha_\oa^{-1}$. The other combinations are used in similar fashion.

* $(iii) \Rightarrow (iv)$:
If $\alpha_\ox = \alpha_\oa^{-1}$, then

$(\alpha_\oa \ox \alpha_\oa) m_\ox^F = m_\ox^G \alpha_\ox: G(A) \ox G(B) \to F(A \ox B)$

\[
\begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (-2, 1.25) {};
\node [style=none] (1) at (-2, 0.25) {};
\node [style=none] (2) at (0.25, 0.25) {};
\node [style=none] (3) at (0.25, 1.25) {};
\node [style=ox] (4) at (-1, 0.75) {};
\node [style=circle] (5) at (-1.75, 2) {$\alpha_\oa$};
\node [style=circle] (6) at (-0.25, 2) {$\alpha_\oa$};
\node [style=none] (7) at (-1.75, 2.75) {};
\node [style=none] (8) at (-0.25, 2.75) {};
\node [style=none] (9) at (-1, -1.25) {};
\node [style=none] (10) at (0, 0.5) {};
\node [style=none] (11) at (-1.25, 0.25) {};
\node [style=none] (12) at (-0.75, 0.25) {};
\node [style=none] (15) at (0, 0.5) {$F$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (7.center) to (5);
\draw (8.center) to (6);
\draw (0.center) to (3.center);
\draw (3.center) to (2.center);
\draw (2.center) to (1.center);
\draw (1.center) to (0.center);
\draw [bend right=15, looseness=1.00] (5) to (4);
\draw [bend right=15, looseness=1.00] (4) to (6);
\draw (4) to (9.center);
\draw [bend left=75, looseness=1.00] (11.center) to (12.center);
\end{pgfonlayer}
\end{tikzpicture} = \begin{tikzpicture} %mon2
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (-2, 1.25) {};
\node [style=none] (1) at (-2, 0.25) {};
\node [style=none] (2) at (0.25, 0.25) {};
\node [style=none] (3) at (0.25, 1.25) {};
\node [style=ox] (4) at (-1, 0.75) {};
\node [style=circle] (5) at (-1.75, 2) {$\alpha_\oa$};
\node [style=circle] (6) at (-0.25, 2) {$\alpha_\oa$};
\node [style=none] (7) at (-1.75, 2.75) {};
\node [style=none] (8) at (-0.25, 2.75) {};
\node [style=none] (9) at (-1, -2.5) {};
\node [style=none] (10) at (0, 0.5) {};
\node [style=none] (11) at (-1.25, 0.25) {};
\node [style=none] (12) at (-0.75, 0.25) {};
\node [style=circle] (13) at (-1, -0.5) {$\alpha_\ox$};
\node [style=circle] (14) at (-1, -1.5) {$\alpha_\oa$};
\node [style=none] (15) at (0, 0.5) {$F$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (7.center) to (5);
\draw (8.center) to (6);
\draw (0.center) to (3.center);
\draw (3.center) to (2.center);
\draw (2.center) to (1.center);
\draw (1.center) to (0.center);
\draw [bend right=15, looseness=1.00] (5) to (4);
\draw [bend right=15, looseness=1.00] (4) to (6);
\draw [bend left=75, looseness=1.00] (11.center) to (12.center);
\draw (4) to (13);
\draw (13) to (14);
\draw (14) to (9.center);
\end{pgfonlayer}
\end{tikzpicture} =
\begin{tikzpicture} %mon3
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (-2, 0.25) {};
\node [style=none] (1) at (-2, -0.75) {};
\node [style=none] (2) at (0.25, -0.75) {};
\node [style=none] (3) at (0.25, 0.25) {};
\node [style=ox] (4) at (-1, -0.25) {};
\node [style=circle] (5) at (-1.75, 2) {$\alpha_\oa$};
\node [style=circle] (6) at (-0.25, 2) {$\alpha_\oa$};
\node [style=none] (7) at (-1.75, 2.75) {};
\node [style=none] (8) at (-0.25, 2.75) {};
\node [style=none] (9) at (-1, -2.5) {};
\node [style=none] (10) at (0, -0.5) {};
\node [style=none] (11) at (-1.25, -0.75) {};
\node [style=none] (12) at (-0.75, -0.75) {};
\node [style=circle] (13) at (-1, -1.5) {$\alpha_\oa$};
\node [style=circle] (14) at (-1.75, 1) {$\alpha_\ox$};
\node [style=circle] (15) at (-0.25, 1) {$\alpha_\ox$};
\node [style=none] (16) at (0, -0.5) {$G$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (7.center) to (5);
\draw (8.center) to (6);
\draw (0.center) to (3.center);
\draw (3.center) to (2.center);
\draw (2.center) to (1.center);
\draw (1.center) to (0.center);
\draw [bend left=75, looseness=1.00] (11.center) to (12.center);
\draw (13) to (9.center);
\draw (5) to (14);
\draw (6) to (15);
\draw [bend right, looseness=1.00] (14) to (4);
\draw [bend right, looseness=1.00] (4) to (15);
\draw (4) to (13);
\end{pgfonlayer}
\end{tikzpicture} =
\begin{tikzpicture} %mon4
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (-2, 1.25) {};
\node [style=none] (1) at (-2, 0.25) {};
\node [style=none] (2) at (0.25, 0.25) {};
\node [style=none] (3) at (0.25, 1.25) {};
\node [style=ox] (4) at (-1, 0.75) {};
\node [style=none] (5) at (-1.75, 2.75) {};
\node [style=none] (6) at (-0.25, 2.75) {};
\node [style=none] (7) at (-1, -2.5) {};
\node [style=none] (8) at (-1.25, 0.25) {};
\node [style=none] (9) at (-0.75, 0.25) {};
\node [style=circle] (10) at (-1, -1.5) {$\alpha_\oa$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (0.center) to (3.center);
\draw (3.center) to (2.center);
\draw (2.center) to (1.center);
\draw (1.center) to (0.center);
\draw [bend left=75, looseness=1.00] (8.center) to (9.center);
\draw (10) to (7.center);
\draw [bend right=15, looseness=1.00] (5.center) to (4);
\draw [bend right=15, looseness=1.00] (4) to (6.center);
\draw (4) to (10);
\end{pgfonlayer}
\end{tikzpicture}
\]

$m_\top^F = m_\top^G \alpha_\oa: \top \to F(\top)$

\[
\begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=circle] (0) at (1.25, 2.25) {$\top$};
\node [style=none] (1) at (2, 1.5) {};
\node [style=none] (2) at (2, 3) {};
\node [style=none] (3) at (0.5, 3) {};
\node [style=none] (4) at (0.5, 1.5) {};
\node [style=circle, scale=0.5] (5) at (1.25, 1) {};
\node [style=circle] (6) at (-0.75, 3.25) {$\top$};
\node [style=none] (7) at (1.5, 1.5) {};
\node [style=none] (8) at (1, 1.5) {};
\node [style=none] (9) at (1.25, -2) {};
\node [style=none] (10) at (1.75, 1.75) {};
\node [style=none] (11) at (1.75, 1.75) {$F$};
\node [style=none] (12) at (-0.75, 4.25) {};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (1.center) to (2.center);
\draw (2.center) to (3.center);
\draw (3.center) to (4.center);
\draw (4.center) to (1.center);
\draw (5) to (0);
\draw [in=-90, out=180, looseness=1.25, dotted] (5) to (6);
\draw [bend right=75, looseness=1.25] (7.center) to (8.center);
\draw (5) to (9.center);
\draw (6) to (12.center);
\end{pgfonlayer}
\end{tikzpicture}=
\begin{tikzpicture} %mon7b
\begin{pgfonlayer}{nodelayer}
\node [style=circle] (0) at (1.25, 2.25) {$\top$};
\node [style=none] (1) at (2, 1.5) {};
\node [style=none] (2) at (2, 3) {};
\node [style=none] (3) at (0.5, 3) {};
\node [style=none] (4) at (0.5, 1.5) {};
\node [style=circle, scale=0.5] (5) at (1.25, 1) {};
\node [style=circle] (6) at (-0.75, 3.25) {$\top$};
\node [style=circle] (7) at (1.25, 0.25) {$\alpha_\ox$};
\node [style=none] (8) at (1.5, 1.5) {};
\node [style=none] (9) at (1, 1.5) {};
\node [style=circle] (10) at (1.25, -1) {$\alpha_\oa$};
\node [style=none] (11) at (1.75, 1.75) {$F$};
\node [style=none] (12) at (1.25, -2) {};
\node [style=none] (13) at (-0.75, 4.25) {};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (1.center) to (2.center);
\draw (2.center) to (3.center);
\draw (3.center) to (4.center);
\draw (4.center) to (1.center);
\draw (5) to (0);
\draw [in=-90, out=180, looseness=1.25, dotted] (5) to (6);
\draw [bend right=75, looseness=1.25] (8.center) to (9.center);
\draw (10) to (7);
\draw (7) to (5);
\draw (10) to (12.center);
\draw (6) to (13.center);
\end{pgfonlayer}
\end{tikzpicture} =
\begin{tikzpicture} %mon8b
\begin{pgfonlayer}{nodelayer}
\node [style=circle] (0) at (1.25, 3) {$\top$};
\node [style=none] (1) at (2, 2.25) {};
\node [style=none] (2) at (2, 3.75) {};
\node [style=none] (3) at (0.5, 3.75) {};
\node [style=none] (4) at (0.5, 2.25) {};
\node [style=circle, scale=0.5] (5) at (1.25, 1.75) {};
\node [style=circle] (6) at (-0.75, 4) {$\top$};
\node [style=none] (7) at (1.25, -1) {};
\node [style=none] (8) at (1.5, 2.25) {};
\node [style=none] (9) at (1, 2.25) {};
\node [style=circle] (10) at (1.25, -0.25) {$\alpha_\oa$};
\node [style=none] (11) at (1.75, 2.5) {$G$};
\node [style=none] (12) at (-0.75, 5) {};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (1.center) to (2.center);
\draw (2.center) to (3.center);
\draw (3.center) to (4.center);
\draw (4.center) to (1.center);
\draw (5) to (0);
\draw [dotted, in=-90, out=180, looseness=1.25] (5) to (6);
\draw [bend right=75, looseness=1.25] (8.center) to (9.center);
\draw (7.center) to (10);
\draw (10) to (5);
\draw (6) to (12.center);
\end{pgfonlayer}
\end{tikzpicture}
\]

Thus, $\alpha_\ox$ is comonoidal. Similarly, it can be proven that $\alpha_\oa$ is monoidal. The axioms [LT.4] (a)-(d) for a linear transformation are satisfied for $(\alpha_\oa, \alpha_\ox)$ because $\alpha_\oa = \alpha_\ox^{-1}$.

* $(iv) \Rightarrow (i)$ and $(ii)$: The axioms [nat.1] and [nat.2] are given by the fact that $(\alpha_\oa, \alpha_\ox)$ is a linear transformation.

Frobenius functors between isomix categories are especially important in this development and they satisfy an additional property:

A Frobenius functor between isomix categories is an isomix functor in case it is a mix functor which satisfies, in addition, the following diagram:

\[ \mbox{\bf{[isomix-FF]}}~~~~~\xymatrix{ \top \ar@/^/[rrr]^{{\sf m}^{-1}} \ar[dr]_{m_\top} & & & \bot \\ & F(\top) \ar[r]_{F({\sf m}^{-1})} & F(\bot) \ar[ur]_{n_\top} } \]

Recall that a linear functor is normal in case bot $m_\top$ and $n_\bot$ are isomorphisms.  We observe:

For a mix Frobenius functor, $F: \X \to \Y$, between isomix categories the following are equivalent:

* $n_\bot: F(\bot) \to \bot$  or $m_\top: \top \to F(\top)$ is an isomorphism;

* $F$ is a normal functor;

* $F$ is an isomix functor.

* $(i) \Rightarrow (ii)$:  Note that, as $F$ is a mix functor $F({\sf m}) = n_\bot {\sf m}~m_\top$.  As the mix map ${\sf m}$ is an isomorphism so is $F({\sf m})$.  Then if either $n_\bot$ or $m_\top$ is an isomorphism the other must be an isomorphism.  Thus, $F$ will be a normal functor.

* $(ii) \Rightarrow (iii)$: If $F$ is normal then $n_\bot$ and $m_\top$ are isomorphisms and so

\[ \infer={m_\top F({\sf m}^{-1}) n_\bot = {\sf m}^{-1}}{\infer={F({\sf m}^{-1}) = m_\top^{-1} {\sf m}^{-1} n_\bot^{-1}}{F({\sf m}) = n_\bot {\sf m}~m_\top}} \]

* $(iii) \Rightarrow (i)$: The mix preservation for $F$ makes  $n_\bot$ a section ($m_\top$ a retraction) while isomix preservation makes $m_\bot$ a retraction (and $m_\top$ a section.
This means $n_\bot$ is an isomorphism ($m_\top$ is an isomorphism).

If $\alpha$ is a linear natural isomorphism between isomix Frobenius linear functors if and only if $\alpha_\ox = \alpha_\oa^{-1}$.

Note  that if we can establish [nat.1](a) or (b) then we can prove that $\alpha_\ox\alpha_\oa =1$ and, as $\alpha_\ox$ is an isomorphism it follows that $\alpha_\oa\alpha_\ox =1$.
Thus, it suffices to show that [nat.1](a) holds for this we have:

\[ m_\top \alpha_\oa G({\sf m}^{-1}) n_\bot = m_\top F({\sf m}^{-1})\alpha_\oa  n_\bot = m_\top F({\sf m}^{-1})  n_\bot = {\sf m}^{-1} = m_\top G({\sf m}^{-1}) n_\bot  \]

As $G({\sf m}^{-1}) n_\bot$ is an isomorphism it follows that $m_\top \alpha_\oa = m_\top$.

Lemma <ref> and Corollary <ref> are generalizations of <cit.> which states that given a natural transformation $\alpha: F \Rightarrow G$ which is both monoidal and comonoidal between Frobenius monoidal functors, and an object $A$ which has a dual $(\eta, \epsilon): A \dashv B$, then $\alpha_A$ is invertible. In Lemma <ref>, when $A \dashvv B \in \X$, then $\alpha_\oa$ is defined as follows:

\[
\alpha_\oa: G(A) \to F(A) = \begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=circle] (0) at (-0.25, -0) {$\alpha_\ox$};
\node [style=none] (1) at (1.25, -2.75) {};
\node [style=none] (2) at (-0.25, -1) {};
\node [style=none] (3) at (-1.75, -1) {};
\node [style=none] (4) at (-1.75, 2.75) {};
\node [style=circle] (5) at (-1, -1.75) {$\epsilon$};
\node [style=none] (6) at (-0.25, 1) {};
\node [style=none] (7) at (1.25, 1) {};
\node [style=circle] (8) at (0.5, 1.75) {$\eta$};
\node [style=none] (9) at (1.5, 2.5) {};
\node [style=none] (10) at (1.5, 1) {};
\node [style=none] (11) at (-0.5, 1) {};
\node [style=none] (12) at (-0.5, 2.5) {};
\node [style=none] (13) at (-2, -0.75) {};
\node [style=none] (14) at (0, -0.75) {};
\node [style=none] (15) at (0, -2.5) {};
\node [style=none] (16) at (-2, -2.5) {};
\node [style=none] (17) at (-2.25, 2.5) {$G(A)$};
\node [style=none] (18) at (1.75, -2.5) {$F(A)$};
\node [style=none] (19) at (0.25, 0.65) {$F(B)$};
\node [style=none] (20) at (0.5, -0.5) {$G(B)$};
\node [style=none] (21) at (1.25, 2.25) {$F$};
\node [style=none] (22) at (-0.25, -2.25) {$G$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (0) to (2.center);
\draw (3.center) to (4.center);
\draw [in=0, out=-90, looseness=1.25] (2.center) to (5);
\draw [in=180, out=-90, looseness=1.25] (3.center) to (5);
\draw (11.center) to (10.center);
\draw (12.center) to (11.center);
\draw (10.center) to (9.center);
\draw (9.center) to (12.center);
\draw (7.center) to (1.center);
\draw [in=90, out=0, looseness=1.25] (8) to (7.center);
\draw (6.center) to (0);
\draw [in=180, out=90, looseness=1.25] (6.center) to (8);
\draw (13.center) to (16.center);
\draw (16.center) to (15.center);
\draw (15.center) to (14.center);
\draw (14.center) to (13.center);
\end{pgfonlayer}
\end{tikzpicture}
\]

For these special linear isomorphisms with $\alpha_\ox = \alpha_\oa^{-1}$ we can simplify the coherence requirements:

Suppose $F$ and  $G$ are Frobenius functors and $\alpha$ is a natural isomorphism then:

* If $\alpha: F \to G$ is $\ox$-monoidal and $\oa$-comonoidal then $(\alpha,\alpha^{-1})$ is a linear transformation;

* If $F$ and $G$ are strong Frobenius functors and $\alpha$ is $\ox$-monoidal and $\oa$-monoidal then $(\alpha,\alpha^{-1})$ is a linear transformation.

* If $\alpha$ is $\ox$-monoidal and $\oa$-comonoidal then so is $\alpha^{-1}$ supporting the possibility that it is a component of a linear transformation.
Considering  [LT.1] we show that $(\alpha,\alpha^{-1})$ satisfies this requirement as:

\[ \xymatrix{ F(A \oa B) \ar[rr]^{\alpha_\ox}  \ar[d]_{n_\oa = \nu^R_\ox} & & G(A \oa B) \ar[d]^{n_\oa = \nu^R_\ox} \\
F(A) \oa F(B) \ar[dr]_{1 \oa \alpha} \ar[rr]^{\alpha \oa \alpha} & & G(A) \oa G(B)  \ar[dl]^{\alpha^{-1} \oa 1} \\
& F(A) \oa G(B) } \]

The remaining requirements follow in a similar manner.

* When the laxors for the functors are isomorphisms then being monoidal implies being comonoidal.

§.§ Dagger mix categories

Conventionally, in categorical quantum mechanics a dagger is defined as a contravariant functor which is an involution that is stationary on objects, . Before proceeding to define dagger for LDCs, the notion of the opposite of an LDC and whence the notion of a contravariant linear functors have to be developed.  For LDCs we cannot expect the dagger to be stationary on objects, however, it is still possible that it can act like an involution.

If $(\X, \ox, \top, \oa, \bot)$ is a linear distributive category, the opposite linear distributive category is $(\X, \ox, \top, \oa, \bot)^{\op} := (\X^{\op}, \oa, \bot, \ox, \top)$ where $\X^{\op}$ is the usual opposite category with the monoidal structures are flipped as follows:

\[\ox^{\op} := \oa ~~~~~~~ \top^{\op} : \bot ~~~~~~~ \oa^{\op} := \ox ~~~~~~~ \bot^{\op} := \top\]

Note that $(\X, \ox, \top, \oa, \bot)^{{\op}~{\op}} = (\X, \ox, \top, \oa, \bot) $. A contravariant linear functor $F$ is then a linear functor $F: \Y^{\op} \to \X$. If $(F_\ox, F_\oa): (\X, \ox, \top, \oa, \bot)^{\op} \to (\X, \ox, \top, \oa, \bot)$ is a contravariant linear functor, then the opposite linear functor  $(F_\ox, F_\oa)^{\op}: (\X, \ox, \top, \oa, \bot) \to  (\X, \ox, \top, \oa, \bot)^{\op}$ given by the pair of opposite functors $(F_\oa^{\op}, F_\ox^{\op})$. Observe that $F^{\op}$ is  a mix Frobenius linear functor if and only if $F$ is.

A dagger linearly distributive category, $\dagger$-LDC, is an LDC, $\X$, with a contravariant Frobenius linear functor $(\_)^\dagger: \X^{\op} \to \X$ which is a linear involutive equivalence   $(\_)^\dagger ~\dashvv ~ (\_)^{\dagger^{\op}}: \X^{\op} \to \X$.

First note that saying this is an involutive equivalence asserts that the unit and counit of the equivalence are the same map (although one is in the opposite category).  Thus, the adjunction expands to take the form $(\imath,\imath): (\_)^\dagger ~\dashvv ~ (\_)^{\dagger^{\op}}: \X^{\op} \to \X$.  However, the unit and counit are linear natural transformations so $\imath$ expands to $\imath = (\imath_\ox,\imath_\oa)$.  As the dagger functor is
a left adjoint, it is strong and, thus, is normal.  Furthermore, as the unit of an equivalence, $\imath$ is a linear natural isomorphism.  This means  $\imath = (\imath_\ox,\imath_\oa)$ satisfies the requirements of Lemma <ref>, implying that $\imath_\ox^{-1}  = \imath_\oa$.  Simplifying notation we shall set $\iota:= \imath_\oa$  so the unit linear transformation $\imath := (\iota^{-1},\iota)$ we then can simplify the requirements to those of this $\iota: A \to (A^\dagger)^\dagger$ which we refer to as the involutor.

A symmetric  $\dagger$-LDC is a $\dagger$-LDC which is a symmetric LDC for which the dagger is a symmetric linear functor. A cyclic $\dagger$-$*$-autonomous category is a
$\dagger$-LDC with chosen left are right duals and a cyclor which is preserved by the dagger.  A $\dagger$-mix category is a $\dagger$-LDC for which $(\_)^\dagger: \X^{\op} \to \X$
is a mix functor.  As the dagger functor is strong (and so normal) if the category is an isomix category then being $\dagger$-mix already implies that
the dagger is an isomix functor.  Thus, a $\dagger$-isomix category is a $\dagger$-mix category which happens to be an isomix category.

In the remainder of the section, we unfold the definition of a $\dagger$-isomix categories and give the coherences requirements explicitly.

A dagger linearly distributive category is an LDC with a functor $(\_)^\dag:\X^\op\to \X$ and
natural isomorphisms

\begin{align*}
\text{ \bf laxors: }  &A^\dag \ox B^\dag \xrightarrow{ \lambda_\ox} (A\oa B)^\dag ~~~~~ A^\dag \oa B^\dag \xrightarrow{ \lambda_\oa} (A\ox B)^\dag \\
&\top \xrightarrow{\lambda_\top} \bot^\dag ~~~~~~~~~~~~~~~~~~~~~ \bot \xrightarrow{\lambda_\bot} \top^\dag \\
\text{ \bf and involutor: } & A \xrightarrow{\iota} (A^\dag)^\dag
\end{align*}

such that the following coherences hold:

* Interaction of $\lambda_\ox, \lambda_\oa$  with associators:

\[
\begin{tabular}{cc}
\xymatrix{
A^\dag \ox (B^\dag \ox C^\dag)                \ar@{->}[r]^{a_\ox}    \ar@{->}[d]_{1 \ox  \lambda_\ox}
& (A^\dag \ox B^\dag) \ox C^\dag              \ar@{->}[d]^{\lambda_\ox \ox 1}  \\
A^\dag \ox ( B \oa C)^\dag                     \ar@{->}[d]_{\lambda_\ox}
& (A \oa B)^\dag \oa C^\dag                   \ar@{->}[d]^{\lambda_\ox}    \\
(A \oa (B \oa C))^\dag                          \ar@{->}[r]_{(a_\oa^{-1})^\dag}
& ( (A\oa B) \oa C)^\dag
} &\xymatrix{
A^\dag \oa (B^\dag \oa C^\dag)                \ar@{->}[r]^{a_\oa}    \ar@{->}[d]_{1 \oa \lambda_\oa }
& (A^\dag \oa B^\dag) \oa C^\dag              \ar@{->}[d]^{\lambda_\oa \oa 1}  \\
A^\dag \oa (B \ox C)^\dag                 \ar@{->}[d]_{\lambda_\oa}
& (A \ox B)^\dag \oa C^\dag                    \ar@{->}[d]^{\lambda_\oa}    \\
(A \ox (B\ox C))^\dag                          \ar@{->}[r]_{(a_\ox^{-1})^\dag}
& ((A\ox B) \ox C)^\dag
\end{tabular}
\]

* Interaction of $\lambda_\top, \lambda_\bot$ with unitors:

⊤A^†@->[rr]^λ_⊤1 @->[d]_u_^R

A^†         (A)^†@<-[ll]^(u_^R)^†

A^†@->[rr]^λ_1 @->[d]_u_^R

A^†         (⊤A)^†@<-[ll]^(u_^R)^†

and two symmetric diagrams for $u_\ox^R$ and $u_\oa^R$ must also be satisfied.

* Interaction of $\lambda_\ox, \lambda_\oa$ with linear distributors:

A^†(B^†C^†)              @->[r]^δ^L @->[d]_1λ_

(A^†B^†) C^†@->[r]^δ^R @->[d]_λ_1
A^†(B^†C^†) @->[d]_1λ_

* Interaction of $\iota: A \rightarrow A^{\dagger\dagger}$ with $\lambda_\ox$, $\lambda_\oa$:

AB                          @->[r]^ι @->[d]_ιι

AB                          @->[r]^ι @->[d]_ιι

* Interaction of $\iota: A \rightarrow A^{\dagger\dagger}$ with $\lambda_\top$, $\lambda_\bot$:

$\begin{matrix} \xymatrix{
&\bot                   \ar@{->}[r]^{\iota} \ar@{->}[dr]_{\lambda_\bot}
& (\bot^\dag)^\dag   \ar@{->}[d]^{\lambda_\top^\dag}\\
& \top^\dag
} \end{matrix}$
$\begin{matrix} \xymatrix{
&\top                   \ar@{->}[r]^{\iota} \ar@{->}[dr]_{\lambda_\top}
& (\top^\dag)^\dag   \ar@{->}[d]^{\lambda_\bot^\dag} \\
& \bot^\dag
} \end{matrix}$

* $\iota_{A^\dagger} = (\iota_A^{-1})^\dagger: A^\dagger \to A^{\dagger\dagger\dagger}$

The structure is presented using strong monoidal laxors:  to form a linear functor the laxor $\lambda_\oa$ needs to be reversed by taking its inverse.  Once this
adjustment is made all the required coherences for a linear functor are present.

Note that [$\dagger$-ldc.6] equivalently expresses the triangle identities of the adjunction.

The coherences for the involutor are given as it is a monoidal transformation for both the tensor and par: by Lemma <ref> (ii) this suffices.

A symmetric $\dagger$-LDC is a $\dagger$-LDC which is a symmetric LDC and for which the following additional diagrams commute:

* Interaction of $\lambda_\ox , \lambda_\oa$ with symmetry maps:

\[
\begin{tabular}{cc}
\xymatrix{
A^\dag \ox B^\dag                          \ar@{->}[r]^{\lambda_\ox} \ar@{->}[d]_{c_\ox}
& (A\oa B)^\dag                          \ar@{->}[d]^{c_\oa^\dag}\\
B^\dag \ox A^\dag                          \ar@{->}[r]_{\lambda_\ox}
& (B\oa A)^\dag\\
} & \xymatrix{
A^\dag \oa  B^\dag                          \ar@{->}[r]^{\lambda_\oa} \ar@{->}[d]_{c_\oa}
& (A\ox B)^\dag                          \ar@{->}[d]^{c_\ox^\dag}\\
B^\dag \oa A^\dag                          \ar@{->}[r]_{\lambda_\oa}
& (B\ox A)^\dag\\
\end{tabular}
\]

A $\dagger$-mix category is a $\dagger$-LDC which has a mix map and satisfies the following additional coherence:

\[ \mbox{\bf [$\dagger$-\text{mix}]}  ~~~~\begin{array}[c]{c}
\xymatrix{
\bot                 \ar@{->}[r]^{{\sf m}} \ar@{->}[d]_{\lambda_\bot}
& \top             \ar@{->}[d]^{\lambda_\top}\\
\top^\dag            \ar@{->}[r]_{{\sf m}^\dag}
& \bot^\dag
\end{array} \]

If ${\sf m}$ is an isomorphism, then $\X$ is an $\dagger$-isomix category and, since $(\_)^\dagger$ is normal, $(\_)^\dagger$ is an isomix Frobenius functor.

Suppose $\X$ is a $\dagger$-mix category then the following diagram commutes:

\[
\xymatrix{ A^\dag \oa B^\dag  \ar[r]^{\mx} \ar[d]_{\lambda_\oa}&  A^\dag \ox B^\dag \ar[d]^{\lambda_\ox} \\
(A \ox B)^\dag \ar[r]_{\mx^\dag}  & (A \oa B)^\dag }
\]

The proof follows directly from Lemma <ref>.

Suppose $\X$ is a $\dagger$-mix category and $A \in \Core(\X)$ then $A^\dagger \in$ $\Core(\X)$.

The natural transformation $A^\dagger \ox X \xrightarrow{\mx} A^\dagger \oa X$ is an isomorphism as:

\[
\xymatrix{
A^\dagger \ox X \ar[r]^{1 \ox \iota} \ar[d]_{\mx}<EMAIL_ADDRESS>(nat. {\sf mx})}}
& A^\dagger \ox X^{\dagger\dagger} \ar[r]^{\lambda_\ox} \ar[d]_{\mx}<EMAIL_ADDRESS>{lem. \ref{Lemma: mixdagger}}}}
& (A \oa X^\dagger)^\dagger \ar[d]^{\mx^\dagger} \\
A^\dagger \oa X \ar[r]_{1 \oa \iota}
& A^\dagger \oa A^{\dagger \dagger} \ar[r]_{\lambda_\oa}
&(A \ox X^\dagger)^\dagger
\]

Let $\X$ be $\dagger$-LDC. If $A \dashvv B$ then $B^\dagger \dashvv A^\dagger$.

The statement  follows from Lemma <ref>: Frobenius functors preserve linear adjoints. Explicitly, if $(\eta,\epsilon): A \dashvv B$ then $(\lambda_\top\epsilon^\dag\lambda_\oa^{-1},\lambda_\ox\eta^\dagger \lambda_\bot^{-1}): B^\dagger \dashvv A^\dagger$.

Suppose $\X$ is a $\dagger$-$*$-autonomous category and $(\eta*, \epsilon*): A^* \dashvv A$, then $((\epsilon*)^\dagger, (\eta*)^\dagger): A^\dagger \dashvv (A^*)^\dagger$, where $((\epsilon*)^\dagger, (\eta*)^\dagger) :=   (\lambda_\top\epsilon*^\dag\lambda_\oa^{-1},\lambda_\ox\eta*^\dagger \lambda_\bot^{-1})$. We draw $(\epsilon*)^\dagger$ and $(*\epsilon)^\dagger$ as dagger cups, and $(\eta*)^\dagger$ and $(*\eta)^\dagger$ as dagger caps which are pictorially represented as follows:

\[
\begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (-1, 2) {};
\node [style=none] (1) at (1, 2) {};
\node [style=none] (2) at (-1, 0.5) {};
\node [style=none] (3) at (1, 0.5) {};
\node [style=none] (4) at (-1.5, 1.5) {$X^\dagger$};
\node [style=none] (5) at (1.5, 1.5) {$(^*X)^\dagger$};
\node [style=none] (6) at (0, -1) {$(*\eta)^\dagger$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (2.center) to (0.center);
\draw [bend right=90, looseness=2.00] (2.center) to (3.center);
\draw (3.center) to (1.center);
\end{pgfonlayer}
\end{tikzpicture} ~~~~~~~~~ \begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (-1, 2) {};
\node [style=none] (1) at (1, 2) {};
\node [style=none] (2) at (-1, 0.5) {};
\node [style=none] (3) at (1, 0.5) {};
\node [style=none] (4) at (-1.5, 1.5) {$X^{*\dagger}$};
\node [style=none] (5) at (1.5, 1.5) {$X^\dagger$};
\node [style=none] (6) at (0, -1) {$(\eta*)^\dagger$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (2.center) to (0.center);
\draw [bend right=90, looseness=2.00] (2.center) to (3.center);
\draw (3.center) to (1.center);
\end{pgfonlayer}
\end{tikzpicture} ~~~~~~~~~ \begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (-1, -1) {};
\node [style=none] (1) at (1, -1) {};
\node [style=none] (2) at (-1, 0.5) {};
\node [style=none] (3) at (1, 0.5) {};
\node [style=none] (4) at (-1.5, -0.5) {$X^\dagger$};
\node [style=none] (5) at (1.5, -0.5) {$(^*X)^\dagger$};
\node [style=none] (6) at (0, 2) {$(*\epsilon)^\dagger$ };
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (2.center) to (0.center);
\draw [bend left=90, looseness=2.00] (2.center) to (3.center);
\draw (3.center) to (1.center);
\end{pgfonlayer}
\end{tikzpicture} ~~~~~~~~~ \begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (-1, -1) {};
\node [style=none] (1) at (1, -1) {};
\node [style=none] (2) at (-1, 0.5) {};
\node [style=none] (3) at (1, 0.5) {};
\node [style=none] (4) at (-1.5, -0.5) {$X^{*^\dagger}$};
\node [style=none] (5) at (1.5, -0.5) {$X^\dagger$};
\node [style=none] (6) at (0, 2) {$(\epsilon*)^\dagger$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (2.center) to (0.center);
\draw [bend left=90, looseness=2.00] (2.center) to (3.center);
\draw (3.center) to (1.center);
\end{pgfonlayer}
\end{tikzpicture}
\]

A $\dagger$-$*$-autonomous category is a cyclic $\dagger$-$*$-autonomous category when the dagger preserves the cyclor:

\[ %last1
\begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (5.5, 2.75) {};
\node [style=none] (1) at (5.5, -0.9999999) {};
\node [style=none] (2) at (4, -0.9999999) {};
\node [style=none] (3) at (4, 0.9999999) {};
\node [style=none] (4) at (2.75, 0.9999999) {};
\node [style=circle, scale=1.2] (5) at (2.75, -0.9999999) {$\phi^\dagger$};
\node [style=circle] (6) at (2.75, -2.5) {$\phi^{{-1}^\dagger}$};
\node [style=none] (7) at (2.75, -4.25) {};
\node [style=none] (8) at (6, 2.25) {$(A^\dagger)^*$};
\node [style=none] (9) at (4.5, -2) {$\epsilon*$};
\node [style=none] (10) at (3, 2) {$(*\epsilon)^\dagger$};
\node [style=none] (11) at (2.25, -3.75) {$(^*A)^\dagger$};
\node [style=none] (12) at (4.5, -0) {$A^\dagger$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (0.center) to (1.center);
\draw [bend left=90, looseness=1.25] (1.center) to (2.center);
\draw (2.center) to (3.center);
\draw [bend right=90, looseness=1.25] (3.center) to (4.center);
\draw (4.center) to (5);
\draw (5) to (6);
\draw (6) to (7.center);
\end{pgfonlayer}
\end{tikzpicture} = %last2
\begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (5.5, -0.9999999) {};
\node [style=none] (1) at (4, -1) {};
\node [style=none] (2) at (4, -3) {};
\node [style=none] (3) at (2.5, -3) {};
\node [style=circle, scale=1.3] (4) at (2.5, -0.9999999) {$\phi$};
\node [style=circle] (5) at (5.5, -4) {$\phi^{{-1}^\dagger}$};
\node [style=none] (6) at (2.5, 0.9999999) {};
\node [style=none] (7) at (1.25, -0.25) {$(A^\dagger)^*$};
\node [style=none] (8) at (4.75, -0.25) {$(\epsilon*)^\dagger$};
\node [style=none] (9) at (3.25, -3.75) {$*\epsilon$};
\node [style=none] (10) at (6.999999, -5) {$(^*A(+)^\dagger$};
\node [style=none] (11) at (4.5, -2) {$A^\dagger$};
\node [style=none] (12) at (5.5, -5.25) {};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw [bend right=90, looseness=1.25] (0.center) to (1.center);
\draw (1.center) to (2.center);
\draw [bend left=90, looseness=1.25] (2.center) to (3.center);
\draw (3.center) to (4);
\draw (0.center) to (5);
\draw (5) to (12.center);
\draw (4) to (6.center);
\end{pgfonlayer}
\end{tikzpicture} \]

In a cyclic, $\dagger$-$*$-autonomous category,

\[ %last3
\begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (5.999999, 0.9999999) {};
\node [style=none] (1) at (3.999998, 0.9999999) {};
\node [style=none] (2) at (4, -1.75) {};
\node [style=none] (3) at (2, -1.75) {};
\node [style=circle, scale=1.25] (4) at (2, -1) {$\phi$};
\node [style=none] (5) at (2, 2.25) {};
\node [style=none] (6) at (4.999999, 2) {$(*\epsilon)^\dagger$};
\node [style=none] (7) at (3, -2.75) {$*\epsilon$};
\node [style=none] (8) at (6, -3) {};
\node [style=circle] (9) at (3.999998, -0.7499999) {$\phi^\dagger$};
\node [style=none] (10) at (1.5, 2) {$A^{*\dagger*}$};
\node [style=none] (11) at (6.499999, -2.75) {$A^\dagger$};
\node [style=none] (12) at (1.25, -1.5) {$~^*(A^{\dagger*})$};
\node [style=none] (13) at (4.5, -1.25) {$A^{\dagger*}$};
\node [style=none] (14) at (4.499998, 0.4999999) {$~^*(A^\dagger)$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw [bend right=90, looseness=1.25] (0.center) to (1.center);
\draw [bend left=90, looseness=1.25] (2.center) to (3.center);
\draw (3.center) to (4);
\draw (4) to (5.center);
\draw (0.center) to (8.center);
\draw (1.center) to (9);
\draw (9) to (2.center);
\end{pgfonlayer}
\end{tikzpicture} = %last4
\begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (6, -2.75) {};
\node [style=none] (1) at (4, -2.75) {};
\node [style=none] (2) at (4, -0.5) {};
\node [style=none] (3) at (2, -0.5) {};
\node [style=none] (4) at (3, 0.4999999) {$(\epsilon*)^\dagger$};
\node [style=none] (5) at (5, -3.75) {$\epsilon*$};
\node [style=none] (6) at (6, 1.25) {};
\node [style=none] (7) at (6.75, 0.7499999) {$A^{*\dagger*}$};
\node [style=none] (8) at (1.25, -3) {$A^\dagger$};
\node [style=none] (9) at (2, -4.25) {};
\node [style=none] (10) at (4.5, -1.75) {$A^{*\dagger}$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw [bend left=90, looseness=1.25] (0.center) to (1.center);
\draw [bend right=90, looseness=1.25] (2.center) to (3.center);
\draw (0.center) to (6.center);
\draw (2.center) to (1.center);
\draw (3.center) to (9.center);
\end{pgfonlayer}
\end{tikzpicture}
\]

Proved by direct application of Lemma <ref>.

§.§ Functors for $\dagger$-LDCs

Clearly the functors and transformations between $\dagger$-LDCs must “preserve” the dagger in some sense.  More precisely we have:

$F: \X \to \Y$ is a $\dagger$-linear functor between $\dagger$-LDCs when $F$ is a linear functor equipped with a linear natural isomorphism
$\rho^F= (\rho_\ox^F: F_\ox(A^\dagger) \to F_\oa(A)^\dagger ,\rho_\oa^F:  F_\ox(A)^\dagger \to F_\oa(A^\dagger))$ called the preservator,
such that  the following diagrams commute:

\[
\xymatrix{
F_\ox(X) \ar[r]^{\iota} \ar[d]_{F_\ox(\iota)} \ar@{}[dr]|{\mbox{\tiny {\bf [$\dagger$-LF.1]}}} &
F_\ox(X)^{\dagger \dagger} \ar@{<-}[d]^{(\rho^F_\oa)^\dagger} \\
F_\ox(X^{\dagger \dagger}) \ar[r]_{\rho^F_\ox} & F_\oa(X^\dagger)^\dagger
} ~~~~~~~~~ \xymatrix{
F_\oa(X) \ar[r]^{\iota} \ar[d]_{F_\oa(\iota)}  \ar@{}[dr]|{\mbox{\tiny {\bf [$\dagger$-LF.2]}}} & F_\oa(X)^{\dagger \dagger} \ar[d]^{(\rho^F_\ox)^\dagger} \\
F_\oa(X^{\dagger \dagger}) \ar@{<-}[r]_{\rho^F_\oa} & F_\ox(X^\dagger)^\dagger
\]

Observe that in the case $F$ is a normal mix functor between $\dagger$-isomix categories, then $F_\ox= F_\oa$ and the preservators become inverses, $\rho^F_\ox = (\rho^F_\oa)^{-1}$.
This means the squares [$\dagger$-LF.1] and [$\dagger$-LF.2] coincide to give a single condition for the tensor preservator:

\[ \xymatrix{
F(X) \ar[r]^{\iota} \ar[d]_{F(\iota)} \ar@{}[dr]|{\mbox{\tiny {\bf [$\dagger$-isomix]}}} &
F(X)^{\dagger \dagger} \ar@{->}[d]^{(\rho^F_\ox)^\dagger} \\
F(X^{\dagger \dagger}) \ar[r]_{\rho^F_\ox} & F(X^\dagger)^\dagger
} \]

For linear natural transformations $\beta: F \to G$ between $\dagger$-linear functors we demand that $\beta_\ox$ and $\beta_\oa$ are related by:

\[ \xymatrix{F_\ox(A^\dagger) \ar[d]_{\rho^F_\ox} \ar[rr]^{\beta_\ox} && G_\ox(A^\dagger)  \ar[d]^{\rho^G_\ox} \\
(F_\oa(X))^\dagger \ar[rr]_{\beta_\oa^\dagger} & &  (G_\oa(X))^\dagger}
\xymatrix{(G_\ox(X))^\dagger \ar[d]_{\rho^G_\oa} \ar[rr]^{\beta_\ox^\dagger} &&  (F_\ox(X))^\dagger \ar[d]^{\rho^F_\oa} \\
G_\oa(A^\dagger) \ar[rr]_{\beta_\oa} & &  F_\oa(A^\dagger)} \]

Notice that this means that $\beta_\ox$ is completely determined by $\beta_\oa$ in the following sense:

\[ \xymatrix{ F_\ox(A) \ar[d]_{F_\ox(\iota)}  \ar[rr]^{\beta_\ox} && G_\ox(A) \ar[d]^{G_\ox(\iota)} \\
F_\ox(A^{\dagger\dagger})  \ar[d]_{\rho^F_\ox} \ar[rr]^{\beta_\ox} & & G_\ox(A^{\dagger\dagger}) \ar[d]^{\rho^G_\ox}  \\
F_\oa(A^\dagger)^\dagger \ar[rr]_{\beta_\oa^\dagger} && G_\oa(A^\dagger)^\dagger } \]

Because the vertical maps are isomorphisms, this diagram can be used to express $\beta_\ox$ in terms of $\beta_\oa$.  Similarly $\beta_\oa$ can be expressed in terms
of $\beta_\ox$.  Thus, it is possible to express the coherences in terms of just one of these transformations.

§ DAGGERS, DUALS, AND CONJUGATION

The goal of this section is to review the interaction of the dualizing, conjugation and dagger functors. In dagger compact closed categories, $(\_)^\dagger$ and the dualizing functor $(\_)^*$ commute with each other and their composite gives the conjugate functor $(\_)_*$. Similary, $(\_)_*$ and $(\_)^*$ when composed gives the dagger functor.  Our aim is to  generalize these interactions to $\dagger$-LDCs and to achieve this at a reasonable level of abstraction.   To achieve this we shall need the notion which we here refer to as “conjugation” but was investigated by Egger in [13] under the moniker of “involution” (which clashes with our usage).

§.§ Duals

The reverse of an LDC, $\X$, written $\X^\rev := (\X, \ox, \top, \oa, \bot)^{\sf rev} = (\X, \ox^{\sf rev}, \top, \oa^{\sf rev}, \bot)$ where,

\[ A \ox^{\sf rev} B := B \ox A ~~~~~~~~~~~ A \oa^{\sf rev} B := B \oa A \]

and the associators and distributors are adjusted accordingly.  Similar to the opposite of an LDC, we have $(\X^{\sf rev})^{\sf rev} = \X$.

In a $*$-autonomous category, taking the left (or right) linear dual of an object extends to a Frobenius linear functor as follows:

\begin{align*}
(\_)^*: (\X^{\sf op})^{\sf rev} &\to \X  ; ~~ A \mapsto A^* ; ~~
\begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (0, 2) {};
\node [style=none] (1) at (-0.5, 1) {};
\node [style=none] (2) at (0.5, 1) {};
\node [style=none] (3) at (-0.5, -0) {};
\node [style=none] (4) at (0.5, -0) {};
\node [style=none] (5) at (0, 1) {};
\node [style=none] (6) at (0, -1) {};
\node [style=none] (7) at (0, -0) {};
\node [style=none] (8) at (0, 0.5) {$f$};
\node [style=none] (9) at (0.25, 1.75) {$A$};
\node [style=none] (10) at (0.25, -0.75) {$B$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (1.center) to (3.center);
\draw (3.center) to (4.center);
\draw (4.center) to (2.center);
\draw (2.center) to (1.center);
\draw (0.center) to (5.center);
\draw (7.center) to (6.center);
\end{pgfonlayer}
\end{tikzpicture} \mapsto  \begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (0, 1.5) {};
\node [style=none] (1) at (-0.5, 1) {};
\node [style=none] (2) at (0.5, 1) {};
\node [style=none] (3) at (-0.5, -0) {};
\node [style=none] (4) at (0.5, -0) {};
\node [style=none] (5) at (0, 1) {};
\node [style=none] (6) at (0, -0.5) {};
\node [style=none] (7) at (0, -0) {};
\node [style=none] (8) at (-1, 1.5) {};
\node [style=none] (9) at (-1, -1) {};
\node [style=none] (10) at (1, -0.5) {};
\node [style=none] (11) at (1, 2) {};
\node [style=none] (12) at (0, 0.5) {$f$};
\node [style=none] (13) at (1.25, 1.75) {$B^*$};
\node [style=none] (14) at (-1.25, -0.75) {$A^*$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (1.center) to (3.center);
\draw (3.center) to (4.center);
\draw (4.center) to (2.center);
\draw (2.center) to (1.center);
\draw (0.center) to (5.center);
\draw (7.center) to (6.center);
\draw [bend right=90, looseness=1.25] (0.center) to (8.center);
\draw (8.center) to (9.center);
\draw [bend right=90, looseness=1.25] (6.center) to (10.center);
\draw (10.center) to (11.center);
\end{pgfonlayer}
\end{tikzpicture}
\end{align*}

The $(\_)^*$ functor is both contravariant and reverses the tensors with the monoidal and comonoidal components defined as follows:

\[ m_{\ox}:  A^* \ox B^* \to (B \oa A)^* :=  \begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (-0.25, 2) {};
\node [style=ox] (1) at (-0.25, 1) {};
\node [style=none] (2) at (-0.5, 0.25) {};
\node [style=none] (3) at (0.25, -0) {};
\node [style=none] (4) at (-1.25, 0.25) {};
\node [style=none] (5) at (-2, -0) {};
\node [style=oa] (6) at (-1.5, 1) {};
\node [style=none] (7) at (-1.5, 1.5) {};
\node [style=none] (8) at (-2.25, 1.5) {};
\node [style=none] (9) at (-2.25, -1) {};
\node [style=none] (10) at (0.5, 1.75) {$B^* \ox A^*$};
\node [style=none] (11) at (-0.8, 0.5) {$B^*$};
\node [style=none] (12) at (0.5, 0.5) {$A^*$};
\node [style=none] (13) at (-3.2, -0.75) {$(A \oa B)^* $};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw [in=90, out=-45, looseness=1.00] (1) to (3.center);
\draw [in=90, out=-135, looseness=1.00] (1) to (2.center);
\draw [bend left=90, looseness=1.25] (2.center) to (4.center);
\draw [in=-60, out=90, looseness=1.00] (4.center) to (6);
\draw (6) to (7.center);
\draw [bend right=90, looseness=1.25] (7.center) to (8.center);
\draw (8.center) to (9.center);
\draw [in=90, out=-135, looseness=0.75] (6) to (5.center);
\draw [in=-90, out=-90, looseness=1.00] (5.center) to (3.center);
\draw (1) to (0.center);
\end{pgfonlayer}
\end{tikzpicture}
~~~~~~~~~~~~~~~ m_\top: \top \to \bot^* :=  \begin{tikzpicture} %pic2
\begin{pgfonlayer}{nodelayer}
\node [style=circle] (0) at (0, 1.75) {$\top$};
\node [style=none] (1) at (0, 3) {};
\node [style=circle, scale=0.5] (2) at (-1, 1) {};
\node [style=circle] (3) at (-1, -0.25) {$\bot$};
\node [style=none] (4) at (-2, -1) {};
\node [style=none] (5) at (-2, 1.5) {};
\node [style=none] (6) at (-1, 1.5) {};
\node [style=none] (7) at (0.25, 2.75) {$\top$};
\node [style=none] (8) at (-2.5, -0.75) {$\bot^*$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (1.center) to (0);
\draw (3) to (6.center);
\draw [bend left=90, looseness=2.00] (5.center) to (6.center);
\draw (5.center) to (4.center);
\draw [in=0, out=-90, looseness=1.50, dotted] (0) to (2);
\end{pgfonlayer}
\end{tikzpicture} \]

\[ n_{\oa}:  (A \ox B)^* \to B^* \oa A^* :=  \begin{tikzpicture} %pic3
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (2, 2) {};
\node [style=ox] (1) at (1, 0.25) {};
\node [style=none] (2) at (2, -0.5) {};
\node [style=none] (3) at (1, -0.5) {};
\node [style=none] (4) at (0.5, 0.75) {};
\node [style=none] (5) at (1.5, 0.75) {};
\node [style=oa] (6) at (-0.75, 0.25) {};
\node [style=none] (7) at (-0.75, -1.75) {};
\node [style=none] (8) at (-0.25, 0.75) {};
\node [style=none] (9) at (-1.25, 0.75) {};
\node [style=none] (10) at (2, 2.25) {$(A \ox B)^*$};
\node [style=none] (11) at (-0.75, -2) {$B^* \oa A^*$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (0.center) to (2.center);
\draw [bend left=90, looseness=1.50] (2.center) to (3.center);
\draw (3.center) to (1);
\draw (6) to (7.center);
\draw [in=150, out=-90, looseness=1.00] (9.center) to (6);
\draw [in=-90, out=11, looseness=1.00] (6) to (8.center);
\draw [in=165, out=-90, looseness=1.25] (4.center) to (1);
\draw [in=-90, out=15, looseness=1.25] (1) to (5.center);
\draw [bend left=90, looseness=2.00] (8.center) to (4.center);
\draw [bend left=90, looseness=1.25] (9.center) to (5.center);
\end{pgfonlayer}
\end{tikzpicture} ~~~~~~~~~~~~~~~ n_\bot: \top^* \to \bot :=  \begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=circle] (0) at (-2, 1) {$\top$};
\node [style=none] (1) at (-1, 2) {};
\node [style=none] (2) at (-2, -0) {};
\node [style=none] (3) at (-1, -0) {};
\node [style=circle] (4) at (0, -1) {$\bot$};
\node [style=circle, scale=0.5] (5) at (-1, 1) {};
\node [style=none] (6) at (0, -2) {};
\node [style=none] (7) at (-0.6, 1.75) {$\top^*$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (0) to (2.center);
\draw [bend right=90, looseness=1.75] (2.center) to (3.center);
\draw (3.center) to (1.center);
\draw [in=90, out=-15, looseness=1.25, dotted] (5) to (4);
\draw (6.center) to (4);
\end{pgfonlayer}
\end{tikzpicture} \]

These maps are isomorphisms and tensor reversing laxors which satisfy the obvious coherences. Thus, $(\_)^*$ is a strong Frobenius linear functor.

$(\_)^*: \X^{\op\rev} \to \X$ is a strong Frobenius functor which, when $\X$ is an isomix category, is a strong isomix Frobenius functor .

To prove that $(\_)^*$ preserves mix we need  to show that $n_\bot \!~\m~ m_\top = \m^* : \top^* \to \bot^* $:

\[
n_\bot \m m_\top = \begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=circle] (0) at (-3, 2.75) {$\top$};
\node [style=none] (1) at (-2, 2) {};
\node [style=none] (2) at (-2, 3) {};
\node [style=circle] (3) at (-1, 1.25) {$\bot$};
\node [style=map] (4) at (-1, 0.5) {};
\node [style=circle] (5) at (-1, -0.25) {$\top$};
\node [style=circle] (6) at (-2, -2) {$\bot$};
\node [style=none] (7) at (-3, -1.25) {};
\node [style=none] (8) at (-3, -2.25) {};
\node [style=circle, scale=0.5] (9) at (-2, 1.75) {};
\node [style=circle, scale=0.5] (10) at (-2, -0.75) {};
\node [style=none] (11) at (-3, 2) {};
\node [style=none] (12) at (-2, -1.25) {};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (1.center) to (2.center);
\draw (7.center) to (8.center);
\draw [bend left, looseness=1.00, dotted] (9) to (3);
\draw [bend left=45, looseness=1.00, dotted] (5) to (10);
\draw (3) to (4);
\draw (4) to (5);
\draw [bend right=90, looseness=3.25] (11.center) to (1.center);
\draw (0) to (11.center);
\draw [bend left=90, looseness=3.75] (7.center) to (12.center);
\draw (12.center) to (6);
\end{pgfonlayer}
\end{tikzpicture} =\begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=circle] (0) at (1.25, 3) {$\top$};
\node [style=none] (1) at (0.25, 3) {};
\node [style=circle] (2) at (-1, 1.25) {$\bot$};
\node [style=map] (3) at (-1, 0.5) {};
\node [style=circle] (4) at (-1, -0.25) {$\top$};
\node [style=circle] (5) at (-2, -2.25) {$\bot$};
\node [style=none] (6) at (-3, -2.25) {};
\node [style=circle, scale=0.5] (7) at (0.25, 2) {};
\node [style=circle, scale=0.5] (8) at (-2, -0.75) {};
\node [style=none] (9) at (0.25, 1.5) {};
\node [style=none] (10) at (1.25, 1.5) {};
\node [style=none] (11) at (-2, -0.25) {};
\node [style=none] (12) at (-3, -0.25) {};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw [dotted, bend right, looseness=1.25] (7) to (2);
\draw [dotted, bend left=45, looseness=1.00] (4) to (8);
\draw (2) to (3);
\draw (3) to (4);
\draw (1.center) to (9.center);
\draw [bend right=90, looseness=2.00] (9.center) to (10.center);
\draw (10.center) to (0);
\draw (5) to (11.center);
\draw (12.center) to (6.center);
\draw [bend left=90, looseness=1.75] (12.center) to (11.center);
\end{pgfonlayer}
\end{tikzpicture} = \begin{tikzpicture} %m3
\begin{pgfonlayer}{nodelayer}
\node [style=circle] (0) at (1.25, 3) {$\top$};
\node [style=none] (1) at (0.25, 2.75) {};
\node [style=circle] (2) at (-1, 1.25) {$\bot$};
\node [style=map] (3) at (-1, 0.5) {};
\node [style=circle] (4) at (-1, -0.25) {$\top$};
\node [style=circle] (5) at (-2, -2.25) {$\bot$};
\node [style=none] (6) at (-3, -2) {};
\node [style=circle, scale=0.5] (7) at (0.25, 2) {};
\node [style=circle, scale=0.5] (8) at (-2, -0.75) {};
\node [style=none] (9) at (0.25, -1.75) {};
\node [style=none] (10) at (1.25, -1.75) {};
\node [style=none] (11) at (-2, 2.5) {};
\node [style=none] (12) at (-3, 2.5) {};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw [dotted, bend right, looseness=1.25] (7) to (2);
\draw [dotted, bend left=45, looseness=1.00] (4) to (8);
\draw (2) to (3);
\draw (3) to (4);
\draw (1.center) to (9.center);
\draw [bend right=90, looseness=2.00] (9.center) to (10.center);
\draw (10.center) to (0);
\draw (5) to (11.center);
\draw (12.center) to (6.center);
\draw [bend left=90, looseness=1.75] (12.center) to (11.center);
\end{pgfonlayer}
\end{tikzpicture} = \begin{tikzpicture} %m3
\begin{pgfonlayer}{nodelayer}
\node [style=circle] (0) at (1.25, 3) {$\top$};
\node [style=none] (1) at (0.25, 2.75) {};
\node [style=circle] (2) at (-0.75, 1.25) {$\bot$};
\node [style=map] (3) at (-0.75, 0.5) {};
\node [style=circle] (4) at (-0.75, -0.25) {$\top$};
\node [style=circle] (5) at (-2, -2.25) {$\bot$};
\node [style=none] (6) at (-3, -2) {};
\node [style=circle, scale=0.5] (7) at (-2, 2) {};
\node [style=circle, scale=0.5] (8) at (0.25, -0.75) {};
\node [style=none] (9) at (0.25, -1.75) {};
\node [style=none] (10) at (1.25, -1.75) {};
\node [style=none] (11) at (-2, 2.5) {};
\node [style=none] (12) at (-3, 2.5) {};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw [dotted, bend left, looseness=1.25] (7) to (2);
\draw [dotted, bend right=45, looseness=1.00] (4) to (8);
\draw (2) to (3);
\draw (3) to (4);
\draw (1.center) to (9.center);
\draw [bend right=90, looseness=2.00] (9.center) to (10.center);
\draw (10.center) to (0);
\draw (5) to (11.center);
\draw (12.center) to (6.center);
\draw [bend left=90, looseness=1.75] (12.center) to (11.center);
\end{pgfonlayer}
\end{tikzpicture} = \begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=map] (0) at (-0.75, 1) {};
\node [style=none] (1) at (-1.75, -1.75) {};
\node [style=none] (2) at (-0.75, -0.25) {};
\node [style=none] (3) at (0.25, -0.25) {};
\node [style=none] (4) at (-0.75, 2.25) {};
\node [style=none] (5) at (-1.75, 2.25) {};
\node [style=none] (6) at (0.25, 3.25) {};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw [bend right=90, looseness=2.00] (2.center) to (3.center);
\draw (5.center) to (1.center);
\draw [bend left=90, looseness=1.75] (5.center) to (4.center);
\draw (4.center) to (0);
\draw (0) to (2.center);
\draw (6.center) to (3.center);
\end{pgfonlayer}
\end{tikzpicture} = \m^*
\]

$(\eta, \epsilon): (\_)^* \dashvv ~ {^*(\_)^{\op\rev}}$

\[
\eta_\ox: X \to ~^*(X^*) := \begin{tikzpicture} %snakea
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (1, -2) {};
\node [style=none] (1) at (1, 0.75) {};
\node [style=none] (2) at (0, 0.75) {};
\node [style=none] (12) at (0.5, 1.75) {$*\eta$};
\node [style=none] (3) at (0, -0.25) {};
\node [style=none] (4) at (-1, -0.25) {};
\node [style=none] (12) at (-0.5, -1.5) {$\epsilon*$};
\node [style=none] (5) at (-1, 2.5) {};
\node [style=none] (6) at (-1.25, 2) {$X$};
\node [style=none] (7) at (-0.35, 0.5) {$X^*$};
\node [style=none] (8) at (1.6, -1.75) {$^*(X^*)$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (4.center) to (5.center);
\draw [bend right=90, looseness=3.25] (4.center) to (3.center);
\draw (3.center) to (2.center);
\draw [bend left=90, looseness=2.50] (2.center) to (1.center);
\draw (1.center) to (0.center);
\end{pgfonlayer}
\end{tikzpicture} \in \X
~~~~~~~~~~~~ \eta_\oa := \eta_\ox^{-1} \]

\[
\epsilon_\ox: (^*X)^* \to X := \begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (-0.75, -2) {};
\node [style=none] (1) at (-0.75, 0.75) {};
\node [style=none] (2) at (0.25, 0.75) {};
\node [style=none] (12) at (-0.5, 1.75) {$\eta*$};
\node [style=none] (3) at (0.25, -0.25) {};
\node [style=none] (4) at (1.25, -0.25) {};
\node [style=none] (34) at (0.65, -1.5) {$*\epsilon$};
\node [style=none] (5) at (1.25, 2.5) {};
\node [style=none] (6) at (1.65, 2) {$X$};
\node [style=none] (7) at (0.6, 0.5) {$^*X$};
\node [style=none] (8) at (-1.25, -1.75) {$(^*X)^*$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (4.center) to (5.center);
\draw [bend left=90, looseness=3.25] (4.center) to (3.center);
\draw (3.center) to (2.center);
\draw [bend right=90, looseness=2.50] (2.center) to (1.center);
\draw (1.center) to (0.center);
\end{pgfonlayer}
\end{tikzpicture} \in \X ~~~~~~~~~~~ \epsilon_\oa := \epsilon_\ox^{-1}
\]

is a linear equivalence of Frobenius linear functors.

The proof is straightforward in the graphical calculus.

When the $*$-autonomous category is cyclic, so there is a cyclor $\psi: A^* \to^{\varphi} \!~^{*}\!A$, then we may straighten out this equivalence to be a dualizing involutive equivalence
(i.e. so that the unit and counit are equal):

$(\eta', \epsilon'): (\_)^* \dashvv  ((\_)^{*})^{\op\rev}$  where $\eta'_\ox = {\eta'_\oa}^{-1} := \eta_\ox \varphi^{-1}$, $\epsilon'_\ox = \epsilon'_\oa:= \epsilon \varphi^*$ and $\eta' = \epsilon'$.

The unit and counit are drawn as follows:

\[
\eta_\ox' =  \begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (-3, 3) {};
\node [style=none] (1) at (-3, 1) {};
\node [style=none] (2) at (-2, 1) {};
\node [style=none] (3) at (-2, 2) {};
\node [style=none] (4) at (-1, 2) {};
\node [style=circle] (5) at (-1, -0) {$\phi^{-1}$};
\node [style=none] (6) at (-1, -1) {};
\node [style=none] (7) at (-2.5, 0.25) {$\epsilon*$};
\node [style=none] (8) at (-1.5, 2.75) {$~^*\eta$};
\node [style=none] (9) at (-3.25, 2.75) {$X$};
\node [style=none] (10) at (-0.5, 1.75) {$~^*(X^*)$};
\node [style=none] (11) at (-0.5, -0.7) {$X^{**}$};
\node [style=none] (12) at (-2.35, 1.5) {$X^*$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (0.center) to (1.center);
\draw [bend right=90, looseness=1.75] (1.center) to (2.center);
\draw (2.center) to (3.center);
\draw [bend left=90, looseness=2.00] (3.center) to (4.center);
\draw (4.center) to (5);
\draw (5) to (6.center);
\end{pgfonlayer}
\end{tikzpicture} \in \X ~~~~~~~~~~ \epsilon_\ox' = \begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (-0.75, -0.5) {};
\node [style=none] (1) at (-0.75, 2.25) {};
\node [style=none] (2) at (0.25, 2.25) {};
\node [style=none] (3) at (0.25, 1) {};
\node [style=none] (4) at (1.25, 1) {};
\node [style=none] (5) at (1.25, 3) {};
\node [style=none] (6) at (0.75, 0.25) {$*\epsilon$};
\node [style=none] (7) at (-0.25, 3) {$\eta*$};
\node [style=none] (8) at (1.5, 2.5) {$X^*$};
\node [style=none] (9) at (-1.75, -0.5) {};
\node [style=circle, scale=2] (10) at (-1.75, 0.5) {};
\node [style=none] (11) at (-1.75, 1.25) {};
\node [style=none] (12) at (-2.75, 1.25) {};
\node [style=none] (13) at (-2.75, -1.25) {};
\node [style=none] (14) at (-1.25, -1.25) {$\epsilon*$};
\node [style=none] (15) at (-2.25, 2) {$\eta*$};
\node [style=none] (16) at (-1.75, 0.5) {$\phi$};
\node [style=none] (17) at (-3.25, -0.75) {$X^{**}$};
\node [style=none] (18) at (-0.25, -0) {$~^*(X^*)$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw [bend left=90, looseness=2.00] (1.center) to (2.center);
\draw (2.center) to (3.center);
\draw [bend right=90, looseness=2.00] (3.center) to (4.center);
\draw (4.center) to (5.center);
\draw (1.center) to (0.center);
\draw [bend right=90, looseness=1.75] (9.center) to (0.center);
\draw (11.center) to (10);
\draw (10) to (9.center);
\draw [bend right=90, looseness=1.75] (11.center) to (12.center);
\draw (12.center) to (13.center);
\end{pgfonlayer}
\end{tikzpicture} = %dualizor1
\begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (-0.75, 3) {};
\node [style=none] (1) at (-0.75, -0) {};
\node [style=none] (2) at (-1.75, -0) {};
\node [style=none] (3) at (-1.75, 2) {};
\node [style=none] (4) at (-2.75, 2) {};
\node [style=none] (5) at (-2.75, -1) {};
\node [style=none] (6) at (-1.25, -0.75) {$*\epsilon$};
\node [style=none] (7) at (-2.25, 2.75) {$\eta^*$};
\node [style=none] (8) at (-0.5, 2.75) {$X$};
\node [style=none] (9) at (-3.25, -0.5) {$X^{**}$};
\node [style=circle] (10) at (-1.75, 1) {$\phi$};
\node [style=none] (11) at (-2.25, 0.25) {$~^*X$};
\node [style=none] (12) at (-2.1, 1.7) {$X^*$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (0.center) to (1.center);
\draw [bend left=90, looseness=1.75] (1.center) to (2.center);
\draw [bend right=90, looseness=2.00] (3.center) to (4.center);
\draw (4.center) to (5.center);
\draw (3.center) to (10);
\draw (10) to (2.center);
\end{pgfonlayer}
\end{tikzpicture} \stackrel{{\bf \tiny [C.2]}}{=} %dualizor1
\begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (-3, 3) {};
\node [style=none] (1) at (-3, 1) {};
\node [style=none] (2) at (-2, 1) {};
\node [style=none] (3) at (-2, 2) {};
\node [style=none] (4) at (-1, 2) {};
\node [style=circle] (5) at (-1, -0) {$\phi^{-1}$};
\node [style=none] (6) at (-1, -1) {};
\node [style=none] (7) at (-2.5, 0.25) {$\epsilon*$};
\node [style=none] (8) at (-1.5, 2.75) {$~^*\eta$};
\node [style=none] (9) at (-3.25, 2.75) {$X$};
\node [style=none] (10) at (-0.5, 1.75) {$~^*(X^*)$};
\node [style=none] (11) at (-0.5, -0.7) {$X^{**}$};
\node [style=none] (12) at (-2.35, 1.5) {$X^*$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (0.center) to (1.center);
\draw [bend right=90, looseness=1.75] (1.center) to (2.center);
\draw (2.center) to (3.center);
\draw [bend left=90, looseness=2.00] (3.center) to (4.center);
\draw (4.center) to (5);
\draw (5) to (6.center);
\end{pgfonlayer}
\end{tikzpicture} \in \X
\]

The cyclor is a linear transformation which is an isomorphism as it monoidal with respect to both tensor and par ( see ) and adjoints are determined only upto isomorphism. It remains to check that the triangle identities hold:

\[
\eta_{\ox'_{X^*}}(\epsilon_\ox')^* =
\begin{tikzpicture} %triangle1
\begin{pgfonlayer}{nodelayer}
\node [style=circle] (0) at (0.75, 0.25) {$\phi^{-1}$};
\node [style=none] (1) at (0.75, -2.5) {};
\node [style=none] (2) at (0.75, 2.25) {};
\node [style=none] (3) at (-0.25, 2.25) {};
\node [style=none] (4) at (-0.25, 1) {};
\node [style=none] (5) at (-1.25, 1) {};
\node [style=none] (6) at (-1.25, 3) {};
\node [style=none] (7) at (1.5, -0.5) {$X^{***}$};
\node [style=none] (8) at (-0.75, 0.25) {$\epsilon*$};
\node [style=none] (9) at (0.25, 3) {$*\eta$};
\node [style=none] (10) at (-1.5, 2.5) {$X^*$};
\node [style=none] (11) at (-1, -2.5) {};
\node [style=circle] (12) at (-1, -1.5) {$\phi^{-1}$};
\node [style=none] (13) at (-1, -0.75) {};
\node [style=none] (14) at (-2, -0.75) {};
\node [style=none] (15) at (-2, -3.25) {};
\node [style=none] (16) at (-1.5, -0.1) {$*\eta$};
\node [style=none] (17) at (0, -3.35) {$\epsilon*$};
\node [style=none] (18) at (-2.5, -3) {};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (2.center) to (0);
\draw (0) to (1.center);
\draw [bend right=90, looseness=2.00] (2.center) to (3.center);
\draw (3.center) to (4.center);
\draw [bend left=90, looseness=2.00] (4.center) to (5.center);
\draw (5.center) to (6.center);
\draw [bend right=75, looseness=1.25] (11.center) to (1.center);
\draw (11.center) to (12);
\draw (12) to (13.center);
\draw [bend right=90, looseness=1.50] (13.center) to (14.center);
\draw (14.center) to (15.center);
\end{pgfonlayer}
\end{tikzpicture} = \begin{tikzpicture} %triangle2
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (0, -2.5) {};
\node [style=none] (1) at (0, 2.5) {};
\node [style=none] (2) at (1, 2.5) {};
\node [style=none] (3) at (1, 1.25) {};
\node [style=none] (4) at (2, 1.25) {};
\node [style=none] (5) at (2, 3.25) {};
\node [style=none] (6) at (-0.5, 1.25) {$X^{***}$};
\node [style=none] (7) at (1.5, 0.5) {$*\epsilon$};
\node [style=none] (8) at (0.5, 3.25) {$\eta*$};
\node [style=none] (9) at (2.25, 2.75) {$X^*$};
\node [style=none] (10) at (-1, -2.5) {};
\node [style=circle] (11) at (-1, -1.5) {$\phi^{-1}$};
\node [style=none] (12) at (-1, -0.75) {};
\node [style=none] (13) at (-2, -0.75) {};
\node [style=none] (14) at (-2, -3.25) {};
\node [style=none] (15) at (-1.5, -0) {$*\eta$};
\node [style=none] (16) at (-0.5, -3) {$\epsilon*$};
\node [style=circle] (17) at (1, 2) {$\phi$};
\node [style=none] (18) at (-2.25, -2.75) {$X^*$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw [bend left=90, looseness=2.00] (1.center) to (2.center);
\draw [bend right=90, looseness=2.00] (3.center) to (4.center);
\draw (4.center) to (5.center);
\draw [bend right=75, looseness=1.25] (10.center) to (0.center);
\draw (10.center) to (11);
\draw (11) to (12.center);
\draw [bend right=90, looseness=1.50] (12.center) to (13.center);
\draw (13.center) to (14.center);
\draw (1.center) to (0.center);
\draw (2.center) to (17);
\draw (17) to (3.center);
\end{pgfonlayer}
\end{tikzpicture} = \begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (-1, -1) {};
\node [style=none] (1) at (0, -1) {};
\node [style=none] (2) at (0, 3.25) {};
\node [style=none] (3) at (-0.5, -1.75) {$*\epsilon$};
\node [style=none] (4) at (0.25, 2.75) {$X^*$};
\node [style=circle] (5) at (-1, 1.5) {$\phi^{-1}$};
\node [style=none] (6) at (-1, 2.25) {};
\node [style=none] (7) at (-2, 2.25) {};
\node [style=none] (8) at (-2, -3.25) {};
\node [style=none] (9) at (-1.5, 3) {$*\eta$};
\node [style=circle] (10) at (-1, -0.25) {$\phi$};
\node [style=none] (11) at (-2.25, -2.75) {$X^*$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw [bend right=90, looseness=2.00] (0.center) to (1.center);
\draw (1.center) to (2.center);
\draw (5) to (6.center);
\draw [bend right=90, looseness=1.50] (6.center) to (7.center);
\draw (7.center) to (8.center);
\draw (10) to (0.center);
\draw (5) to (10);
\end{pgfonlayer}
\end{tikzpicture} = ~ \begin{tikzpicture} \draw (2, 3.25) -- (2,-3.5); \end{tikzpicture} ~ = ~ 1
\]
The other triangle identity holds similarly.

The equality of $\eta'$ and $\epsilon'$ is immediate from [C.2] for cyclors, the map $\eta'=\epsilon'$ is the dualizor.   In the symmetric case, the dualizor of this
equivalence may be drawn as:

\[
\begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (-3, 3) {};
\node [style=none] (1) at (-3, 1) {};
\node [style=none] (2) at (-2, 1) {};
\node [style=none] (3) at (-2, 2) {};
\node [style=none] (4) at (-1, 2) {};
\node [style=circle] (5) at (-1, -0) {$\phi^{-1}$};
\node [style=none] (6) at (-1, -1) {};
\node [style=none] (7) at (-2.5, 0.25) {$\epsilon*$};
\node [style=none] (8) at (-1.5, 2.75) {$*\eta$};
\node [style=none] (9) at (-3.25, 2.75) {$A$};
\node [style=none] (10) at (-0.5, 1.75) {$~^*(A^*)$};
\node [style=none] (11) at (-0.5, -0.7) {$A^{**}$};
\node [style=none] (12) at (-2.25, 1.5) {$A^*$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (0.center) to (1.center);
\draw [bend right=90, looseness=1.75] (1.center) to (2.center);
\draw (2.center) to (3.center);
\draw [bend left=90, looseness=2.00] (3.center) to (4.center);
\draw (4.center) to (5);
\draw (5) to (6.center);
\end{pgfonlayer}
\end{tikzpicture} =
\begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (-1.75, 2) {};
\node [style=none] (1) at (-1.75, -0) {};
\node [style=none] (2) at (0, -0) {};
\node [style=none] (12) at (-0.75, -1) {$\epsilon*$};
\node [style=none] (3) at (0, 1) {};
\node [style=none] (4) at (-1, 1) {};
\node [style=none] (34) at (-0.5, 1.75) {$\eta*$};
\node [style=none] (5) at (-1, -2.75) {};
\node [style=none] (6) at (-2, 1.75) {$A$};
\node [style=none] (8) at (-1.5, -2.25) {$A^{**}$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (0.center) to (1.center);
\draw [bend right=90, looseness=1.50] (1.center) to (2.center);
\draw (2.center) to (3.center);
\draw [bend right=90, looseness=1.75] (3.center) to (4.center);
\draw (4.center) to (5.center);
\end{pgfonlayer}
\end{tikzpicture} = %dualizor2
\begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (-0.75, 3) {};
\node [style=none] (1) at (-0.75, -0) {};
\node [style=none] (2) at (-1.75, -0) {};
\node [style=none] (3) at (-1.75, 2) {};
\node [style=none] (4) at (-2.75, 2) {};
\node [style=none] (5) at (-2.75, -1) {};
\node [style=none] (6) at (-1.25, -0.75) {$*\epsilon$};
\node [style=none] (7) at (-2.25, 2.75) {$\eta*$};
\node [style=none] (8) at (-0.5, 2.75) {$A$};
\node [style=none] (9) at (-3.25, -0.5) {$A^{**}$};
\node [style=circle] (10) at (-1.75, 1) {$\phi$};
\node [style=none] (11) at (-2.25, 0.25) {$~^*A$};
\node [style=none] (12) at (-2, 1.7) {$A^*$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (0.center) to (1.center);
\draw [bend left=90, looseness=1.75] (1.center) to (2.center);
\draw [bend right=90, looseness=2.00] (3.center) to (4.center);
\draw (4.center) to (5.center);
\draw (3.center) to (10);
\draw (10) to (2.center);
\end{pgfonlayer}
\end{tikzpicture}
\]

§.§ Conjugation

Recall the following structure from Egger [13]:

A conjugation for a monoidal category $(X, \otimes, I)$ consists of a functor $\overline{(\_)}: \X^\rev \to \X$ with natural isomorphisms:

\[ \bar{A} \otimes \bar{B} \to^{\chi} \bar{B \otimes A} ~~~~~~~~~~~~~ \bar{\bar{A}} \to^{\varepsilon} A  \]

called respectively the (tensor reversing) conjugating laxor and the conjugator
such that

\[\bar{\bar{\bar{A}}} \to^{\bar{\varepsilon_A} = \varepsilon_{\bar{A}} } \bar{A} \]

\[
\xymatrix{
(\bar{A} \ox \bar{B}) \ox \bar{C} \ar[rr]^{a_\ox} \ar[d]_{\chi \ox 1}  \ar@{}[ddrr]|{\bf [CF.1]_\ox}  & & \bar{A} \ox (\bar{B} \ox \bar{C}) \ar[d]^{1 \ox \chi} \\
\bar{(B \ox A)} \ox \bar{C} \ar[d]_{\chi} & & \bar{A} \ox \bar{(C \ox B)} \ar[d]^{\chi} \\
\bar{C \ox (B \ox A)} \ar[rr]_{\bar{a_\otimes^{-1}}} & & \bar{(C \ox B) \ox A}
} ~~~~~~~~ \xymatrix{
\bar{\bar{A}} \ox \bar{\bar{B}} \ar[rr]^{\chi} \ar[dd]_{\varepsilon \ox \varepsilon}  \ar@{}[ddrr]|{\bf [CF.2]_\ox}  & & \bar{\bar{B} \ox \bar{A}} \ar[dd]^{\bar{\chi}} \\
& & \\
A \ox B & & \bar{\bar{A \ox B}} \ar[ll]^{\varepsilon}
\]

A monoidal category is conjugative when it has a conjugation.

A symmetric monoidal category, which is conjugative, is symmetric conjugative in case it satisfies the additional coherence:

\[
\xymatrix{
\bar{A} \otimes \bar{B} \ar[d]_{c_\otimes} \ar[rr]^{\chi}  \ar@{}[drr]|{\bf [CF.3]_\ox}  &  & \bar{B \otimes A} \ar[d]^{\bar{c_\otimes}} \\
\bar{B} \otimes \bar{A} \ar[rr]_{\chi} &  & \bar{A \otimes B}
\]

Notice that we have not specified any coherence for the unit $I$ this is because the expected coherences are automatic:

For every conjugative monoidal category, there exists a unique isomorphism $I \xrightarrow{\chi^{\!\!\!\circ}} \bar{I}$ such that

\[
\xymatrix{
I \otimes \bar{A} \ar[rr]^{\chi^{\!\!\!\circ} \otimes 1} \ar[d]_{u_\otimes}  \ar@{}[drr]|{\bf [CF.4]_\top}  & & \bar{I} \otimes \bar{A} \ar[d]^{\chi} \\
\bar{A} \ar[rr]_{\bar{u_\otimes^{-1}}} & & \bar{A \otimes I } } ~~~~~
\xymatrix{ \bar{A} \ox I \ar[rr]^{1 \otimes \chi^{\!\!\!\circ}} \ar[d]_{u_\otimes}  \ar@{}[drr]|{\bf [CF.5]_\top}  & & \bar{A} \ox \bar{I} \ar[d]^{\chi} \\
\bar{A} \ar[rr]_{\bar{u_\otimes^{-1}}} & & \bar{I \otimes A} } ~~~~~
\xymatrix{
I \ar[rr]^{\chi^{\!\!\!\circ}} \ar@{=}[d]  \ar@{}[drr]|{\bf [CF.6]_\top}  & & \bar{I} \ar[d]^{\bar{\chi^{\!\!\!\circ}}} \\
I \ar[rr]_{\varepsilon^{-1}} & & \bar{\bar{I}}
\]

A conjugative LDC is a linearly distributive category $(\X, \ox, \top, \oa, \bot)$ together with a conjugating functor $\bar{(\_)}: \X \to \X$ and natural isomorphisms:

\[ \bar{A} \ox \bar{B} \xrightarrow{\chi_\ox} \bar{B \ox A} ~~~~~~~~~~~~ \bar{A \oa B} \xrightarrow{\chi_\oa} \bar{B} \oa \bar{A} ~~~~~~~~~~~~ \bar{\bar{A}} \xrightarrow{\varepsilon} A \]

such that $(\X, \ox, \top, \chi_\ox, \varepsilon)$ and $(\X, \oa, \bot, \chi_\oa^{-1}, \varepsilon)$ are conjugative (symmetric) monoidal categories with respect to the conjugating functor and  the following diagrams commute:

\[
\xymatrix{
\bar{B \oa C} \ox \bar{A} \ar[rr]^{\chi_\oa \ox 1} \ar[d]_{\chi_\ox}  \ar@{}[ddrr]|{\bf [CF.7]}  & & (\bar{C} \oa \bar{B}) \ox \bar{A} \ar[d]^{\delta} \\
\bar{(A \ox (B \oa C))} \ar[d]_{\bar{\delta}} & & \bar{C} \oa ( \bar{B} \ox \bar{A}) \ar[d]^{1 \oa \chi_\ox} \\
\bar{((A \ox B) \oa C)} \ar[rr]_{\chi_\oa} & & \bar{C} \oa \bar{A \ox B}
} ~~~~~~~~~~
\xymatrix{
\bar{A} \ox \bar{C \oa B} \ar[rr]^{\chi_\ox} \ar[d]_{1 \ox \chi_\oa} \ar@{}[ddrr]|{\bf [CF.8]}   & & \bar{(C \oa B) \ox A} \ar[d]^{\bar{\delta}} \\
\bar{A} \ox (\bar{B} \oa \bar{C}) \ar[d]_{\delta} & & \bar{C \oa (B \ox A)} \ar[d]^{\chi_\oa} \\
(\bar{A} \ox \bar{B}) \oa \bar{C} \ar[rr]_{\chi_\ox \oa 1} & & \bar{(B \ox A)} \oa \bar{C}
\]

Note, by Lemma <ref>, there exists canonical isomorphisms $\top \xrightarrow{\chi^{\!\!\!\circ}_\top} \bar{\top}$ and $\bot \xrightarrow{\chi^{\!\!\!\circ}_\bot} \bar{\bot}$ thes ensure conjugation is a normal functor.  However, if the category is a mix category there is no guarantee that conjugation is a mix functor.   To ensure this we must demand that
conjugation is a mix functor.  Explicitly this means that the following extra condition must be satisfied:

\[ {\bf \small [CF.9]}~~~~~ \xymatrix{\overline{\bot} \ar[rd]_{(\chi^{\!\!\!\circ}_\bot)^{-1}} \ar@/^/[rrr]^{\overline{{\sf m}}} & & & \overline{\top} \\ & \bot \ar[r]_{{\sf m}} & \top \ar[ur]_{\chi^{\!\!\!\circ}_\top} } \]

A conjugative LDC is precisely a LDC $\X$, with a Frobenius adjoint $(\epsilon^{-1}, \epsilon): \overline{(\_)} \dashv \overline{(\_)}^\rev: \X^\rev \to \X$ where $\epsilon := (\varepsilon,\varepsilon^{-1})$.  Furthermore, if the category is an isomix category and conjugation is a mix functor then conjugation is an isomix equivalence.

It is clear that $\overline{(\_)}$ is a strong Frobenius functor so being mix implies being isomix.   Also $\varepsilon$ is clearly monoidal for tensor and par.  The triangle equalities give $\varepsilon \overline{\varepsilon^{-1}} = 1: \overline{A} \to \overline{A}$ which shows $\varepsilon = \overline{\varepsilon}$.

Clearly conjugation should flip left duals into right duals:

If $B \dashvv A$ is a linear dual then $\bar{A} \dashvv \bar{B}$ is a linear dual.

Suppose $(\eta, \varepsilon): B \dashvv A$. Then, $(\chi^{\!\!\!\circ}_\top \bar{\eta} \chi_\oa,\chi_\ox \bar{\varepsilon} \chi^{\!\!\!\circ}_\bot): \bar{A} \dashvv \bar{B}$.

When a $*$-autonomous category is cyclic one expects that conjugation should interact with the cyclor in a coherent fashion:

A conjugative cyclic $*$-autonomous category is a conjugative $*$-autonomous category together with a cyclor $A^* \to^{\psi} \!\!~^{*}\!A$ such that

\[
\xymatrix{
(\bar{A})^* \ar[rr]^{\psi} \ar[d]_{\simeq}  & & ^{*}(\bar{A}) \ar[d]^{\simeq} \\
\bar{(^{*}A)} \ar[rr]_{\bar{\psi^{-1}}} & & \bar{(A^*)}
\]

which gives a map $\sigma: (\overline{A})^{*} \to \overline{(A^{*})}$.

The above condition is drawn as follows:

\[ \sigma =
\begin{tikzpicture} %cca1
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (-1, 0.75) {$\overline{\psi^{-1}}$};
\node [style=circle, scale=2.5] (0) at (-1, 0.75) {};
\node [style=none] (1) at (-1, -0.5) {};
\node [style=none] (2) at (-1, 2.25) {};
\node [style=none] (3) at (0, 2.25) {};
\node [style=none] (4) at (0, 1) {};
\node [style=none] (5) at (1, 1) {};
\node [style=none] (6) at (1, 3) {};
\node [style=none] (7) at (1.5, 2.75) {$(\overline{A})^*$};
\node [style=none] (8) at (0.5, 0.2) {$\epsilon^*$};
\node [style=none] (9) at (-0.5, 3.1) {$\overline{~^*\eta}$};
\node [style=none] (10) at (-1.5, -0.25) {$\overline{A^*}$};
\node [style=none] (12) at (-0.25, 1.5) {$\overline{A}$};
\node [style=none] (11) at (-1.5, 1.75) {$\overline{~^*A}$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (2.center) to (0);
\draw (0) to (1.center);
\draw [bend left=90, looseness=2.00] (2.center) to (3.center);
\draw (3.center) to (4.center);
\draw [bend right=90, looseness=2.00] (4.center) to (5.center);
\draw (5.center) to (6.center);
\end{pgfonlayer}
\end{tikzpicture} = \begin{tikzpicture} %cca1
\begin{pgfonlayer}{nodelayer}
\node [style=circle] (0) at (-1, 2.5) {$\psi$};
\node [style=none] (1) at (-1, 3.25) {};
\node [style=none] (2) at (-1, 0.5) {};
\node [style=none] (3) at (0, 0.5) {};
\node [style=none] (4) at (0, 1.75) {};
\node [style=none] (5) at (1, 1.75) {};
\node [style=none] (6) at (1, -0.25) {};
\node [style=none] (7) at (-1.75, 3.25) {$(\overline{A})^*$};
\node [style=none] (8) at (0.5, 2.6) {$\overline{\eta^*}$};
\node [style=none] (9) at (-0.5, -0.35) {$~^*\epsilon$};
\node [style=none] (10) at (1.5, 0.25) {$\overline{A^*}$};
\node [style=none] (11) at (-1.75, 1.5) {$~^*(\overline{A})$};
\node [style=none] (12) at (-0.25, 1.25) {$\overline{A}$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (2.center) to (0);
\draw (0) to (1.center);
\draw [bend right=90, looseness=2.00] (2.center) to (3.center);
\draw (3.center) to (4.center);
\draw [bend left=90, looseness=2.00] (4.center) to (5.center);
\draw (5.center) to (6.center);
\end{pgfonlayer}
\end{tikzpicture}
\]

When the $*$-autonomous category is symmetric, (symmetric) conjugation automatically preserves the canonical cyclor.

In a conjugative $*$-autonomous category,

\[ %epsi1
\begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=circle] (0) at (0, 1) {$\varepsilon$};
\node [style=none] (1) at (0, -0) {};
\node [style=none] (2) at (-1.75, -0) {};
\node [style=none] (3) at (-1.75, 2) {};
\node [style=none] (4) at (0, 2) {};
\node [style=none] (5) at (-1, 3) {$\overline{\overline{\eta*}}$};
\node [style=none] (6) at (-2.25, 0.3) {$\overline{\overline{X^*}}$};
\node [style=none] (7) at (0.5, 1.7) {$\overline{\overline{X}}$};
\node [style=none] (8) at (0.5, 0.25) {$X$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (4.center) to (0);
\draw (0) to (1.center);
\draw [bend left=90, looseness=1.50] (3.center) to (4.center);
\draw (3.center) to (2.center);
\end{pgfonlayer}
\end{tikzpicture} = %epsi2
\begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=circle] (0) at (-1.75, 1) {$\varepsilon^{-1}$};
\node [style=none] (1) at (-1.75, -0) {};
\node [style=none] (2) at (0, -0) {};
\node [style=none] (3) at (0, 2) {};
\node [style=none] (4) at (-1.75, 2) {};
\node [style=none] (5) at (-1, 3) {$\eta*$};
\node [style=none] (6) at (-2.5, 0.3) {$\overline{\overline{X^*}}$};
\node [style=none] (7) at (0.5, 0.5) {$X$};
\node [style=none] (8) at (-2.25, 1.7) {$X^*$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (4.center) to (0);
\draw (0) to (1.center);
\draw [bend right=90, looseness=1.50] (3.center) to (4.center);
\draw (3.center) to (2.center);
\end{pgfonlayer}
\end{tikzpicture}
\]

\[
\chi_\top^{\!\!\!\circ}~ \overline{\chi_\top^{\!\!\!\circ}} ~ \overline{\overline{\eta*}} ~ \overline{\chi_\oa}^{-1} \chi_\oa^{-1} (1 \oa \varepsilon) = \eta* (\varepsilon^{-1} \oa 1)  : \top \to \overline{\overline{X^*}} \oa X
\]

\begin{align*}
\chi_\top^{\!\!\!\circ} ~ \overline{\chi_\top^{\!\!\!\circ}} ~ \overline{\overline{\eta*}} ~ \overline{\chi}^{-1} \chi^{-1} (1 \oa \varepsilon) &=  \chi_\top^{\!\!\!\circ} ~ \overline{\chi_\top^{\!\!\!\circ}} ~ \overline{\overline{\eta*}} ~ \overline{\chi_\top}^{-1} \chi_\top^{-1} (\varepsilon \varepsilon^{-1} \oa \varepsilon) \\
&=\chi_\top^{\!\!\!\circ} ~ \overline{\chi_\top^{\!\!\!\circ}}  ~ \overline{\overline{\eta*}} ~ \overline{\chi}^{-1} \chi^{-1} (\varepsilon  \oa \varepsilon) (\varepsilon^{-1} \oa 1) \\
&\stackrel{{\bf \small [CF.2]_\oa}}{=} \chi^{\!\!\!\circ} ~ \overline{\chi_\top^{\!\!\!\circ}} ~ \overline{\overline{\eta*}} \varepsilon (\varepsilon^{-1} \oa 1) \\
&\stackrel{{\bf \small nat.}}{=} \chi_\top^{\!\!\!\circ} ~ \overline{\chi_\top^{\!\!\!\circ}} ~  \varepsilon \eta\!* (\varepsilon^{-1} \oa 1) \\
&\stackrel{{\bf \small [CF.6]_\top}}{=} \eta\!* (\varepsilon^{-1} \oa 1)
\end{align*}

§.§ Dagger and conjugation

The interaction of the dagger and conjugation, in the presence of the dualizing functor for cyclic $*$-autonomous categories is illustrated by the following diagram:

\[
\xymatrixcolsep{5pc}
\xymatrixrowsep{5pc}
\xymatrix{
\X^{\op} \ar@/^1pc/[rr]^{(\_)^\dagger} \ar@/^1pc/[dr]|{((\_)^*)^\rev} \ar@{}[rr]|{\bot} &~ \ar@{}[d]|{\cong} &
\X  \ar@/^1pc/[ll]|{((\_)^{\dagger})^{\op}} \ar@/_1pc/[dl]|{\overline{(\_)}^\rev} \ar@{}[dl]|{\dashv} \\
& \X^\rev \ar@/^1pc/[ul]^{(\_)^{*^{\op}}} \ar@/_1pc/[ur]_{\overline{(\_)}} \ar@{}[ul]|{\dashv} &
\]

Specifically we have:

Every cyclic, conjugative $*$-autonomous category  is also a $\dagger$-$*$-autonomous category.

Let $\X$ be a cyclic, conjugative $*$-autonomous category then  $\bar{(\_)^*} \dashv \bar{(\_)}^*$ is an equivalence. To build a dagger we need an equivalence on the same
functor: we obtain this by using the natural equivalence $\sigma: \bar{(\_)^*} \to \bar{(\_)}^*$ from Definition <ref>.  An involutive equivalence, in addition,
requires the unit and counit of the (contravariant) equivalence to be the same map (which we called the involutor, $\iota$). We show that this is the case:

The unit and counit of the equivalence is given by (a) and (b) respectively;

\[ \mbox{\em (a)}~~~~~~~~~  \xymatrix{
\X^{\op} \ar@{=}[rrrr] \ar[dr]_{(\_)^{*^{\sf rev}}} &
\ar@{}[d]|{\Downarrow ~ \eta_\ox'}&
\X^{\op} \ar@{<-}[ld]^{(\_)^{*^{\sf op}}}
& \\
\X^{\sf rev} \ar@{=}[rr] \ar[dr]_{\bar{(\_)}} &
\ar@{}[d]|{\Downarrow ~ \varepsilon^{-1}} &
\X^{\sf rev} \ar@{<-}[ld]^{\bar{(\_)}^{\sf rev}} \ar@{}[rr]_{\sigma}  \ar@{}[rr]^{\Longrightarrow}  &
\X^{\sf oprev} \ar@{<-}@/^1pc/[llld]^{(\_)^{*^{\sf oprev}}} \ar@/_1pc/[ul]_{(\_)^\op}  \\
& & \X & &
\]

\[
\mbox{\em (b)}~~~~~~~~~~~~~~ \xymatrix{
& & &
\X^{\op}  \ar@{<-}@/_1pc/[llld]_{\bar{(\_)}^\op} \ar@{<-}[dl]_{(\_)^{*^{\op}}} \ar[dr]^{(\_)^{*^{\sf rev}}} \ar@{}[d]|{\Downarrow ~ \epsilon'_\ox} & &\\
\X^{\sf op rev} \ar@{<-}[rd]_{(\_)^{*^{\sf oprev}}} \ar@{}[rr]_{\sigma^{-1}}  \ar@{}[rr]^{\Longrightarrow}  &  &
\X^{\sf rev} \ar@{=}[rr] \ar@{<-}[dl]^{\bar{(\_)}^{\sf rev}} & \ar@{}[d]|{\Downarrow ~ \varepsilon} &
\X^{\sf rev} \ar[dr]^{\bar{(\_)}} \\
& \X \ar@{=}[rrrr]&  & & & \X }
\]
where $\sigma: \bar{A}^* \to \bar{A^*}$ is given in Definition <ref>.  Below we show that the unit and counit coincide as maps in $\X$.

\[
(a)~~~~~ %big1
\begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (-2, 3.5) {};
\node [style=circle, scale=2.5] (1) at (-1, 2.75) {};
\node [style=none] (2) at (-2, 2) {};
\node [style=none] (3) at (-1, 2) {};
\node [style=none] (4) at (-1, 3.5) {};
\node [style=none] (5) at (-1, -1.25) {};
\node [style=none] (6) at (-2, -1.25) {};
\node [style=circle, scale=2.5] (7) at (-2, -0.5) {};
\node [style=none] (8) at (-2, 0.25) {};
\node [style=none] (9) at (-3, 0.25) {};
\node [style=circle, scale=2.5] (10) at (-3, -2.5) {};
\node [style=none] (11) at (-3, -3.5) {};
\node [style=none] (12) at (-2, -3.5) {};
\node [style=none] (13) at (-2, -3) {};
\node [style=none] (14) at (-1, -3) {};
\node [style=none] (15) at (-1, -5) {};
\node [style=none] (16) at (-2.75, 2) {};
\node [style=none] (17) at (-2.75, 4.5) {};
\node [style=none] (18) at (-1, 2.75) {$\phi^{-1}$};
\node [style=none] (19) at (-2, -0.5) {$\varepsilon^{-1}$};
\node [style=none] (20) at (-3, -2.5) {$\phi$};
\node [style=none] (21) at (-3.25, 4) {$\bar{\left(\bar{X^*}\right)^*}$};
\node [style=none] (22) at (-2.5, 1.5) {$\bar{\epsilon*}$};
\node [style=none] (23) at (-2.25, 2.75) {$\bar{\bar{X^*}}$};
\node [style=none] (24) at (-1.5, 4.25) {$*\eta$};
\node [style=none] (25) at (-0.4, 3.5) {$~^*\!\!\left(\bar{\bar{X^*}}\right)$};
\node [style=none] (26) at (-0.4, 2) {$\left(\bar{\bar{X^*}}\right)^*$};
\node [style=none] (27) at (-1.75, -2) {$\epsilon*$};
\node [style=none] (28) at (-1, -2.5) {$\eta*$};
\node [style=none] (29) at (-2.5, 1) {$\eta*$};
\node [style=none] (30) at (-3.5, -1) {$X^{**}$};
\node [style=none] (31) at (-1.5, -0) {$X^*$};
\node [style=none] (32) at (-1.5, -1.25) {$\bar{\bar{X^*}}$};
\node [style=none] (33) at (-2.5, -4.25) {$*\epsilon$};
\node [style=none] (34) at (-3.75, -3.25) {$~^*(X^*)$};
\node [style=none] (35) at (-2.5, -3.25) {$X^*$};
\node [style=none] (36) at (-0.5, -4.75) {$X$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (14.center) to (15.center);
\draw [bend right=90, looseness=1.50] (14.center) to (13.center);
\draw (13.center) to (12.center);
\draw [bend left=90, looseness=1.50] (12.center) to (11.center);
\draw (10) to (11.center);
\draw (10) to (9.center);
\draw [bend left=90, looseness=1.75] (9.center) to (8.center);
\draw (8.center) to (7);
\draw (7) to (6.center);
\draw [bend right=90, looseness=1.75] (6.center) to (5.center);
\draw (3.center) to (5.center);
\draw (3.center) to (1);
\draw (1) to (4.center);
\draw [bend right=90, looseness=1.75] (4.center) to (0.center);
\draw (0.center) to (2.center);
\draw [bend left=75, looseness=1.50] (2.center) to (16.center);
\draw (16.center) to (17.center);
\end{pgfonlayer}
\end{tikzpicture}\stackrel{{\bf [C.2]}}{=} %big2
\begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (-2, 3.5) {};
\node [style=circle, scale=2.5] (1) at (-1, 2.75) {};
\node [style=none] (2) at (-2, 2) {};
\node [style=none] (3) at (-1, 2) {};
\node [style=none] (4) at (-1, 3.5) {};
\node [style=none] (5) at (-1, -1.25) {};
\node [style=none] (6) at (-2, -1.25) {};
\node [style=circle, scale=2.5] (7) at (-2, -0.5) {};
\node [style=none] (8) at (-2, 0.25) {};
\node [style=none] (9) at (-3, 0.25) {};
\node [style=none] (10) at (-3, -4.5) {};
\node [style=none] (11) at (-4, -4.5) {};
\node [style=none] (12) at (-4, -3) {};
\node [style=none] (13) at (-5, -3) {};
\node [style=none] (14) at (-5, -5.25) {};
\node [style=none] (15) at (-2.75, 2) {};
\node [style=none] (16) at (-2.75, 4.5) {};
\node [style=none] (17) at (-1, 2.75) {$\phi^{-1}$};
\node [style=none] (18) at (-2, -0.5) {$\varepsilon^{-1}$};
\node [style=none] (19) at (-3.25, 4) {$\bar{\left(\bar{X^*}\right)^*}$};
\node [style=none] (20) at (-2.5, 1.5) {$\bar{\epsilon*}$};
\node [style=none] (21) at (-2.25, 2.75) {$\bar{\bar{X^*}}$};
\node [style=none] (22) at (-1.5, 4.25) {$*\eta$};
\node [style=none] (23) at (-0.4, 3.5) {$~^*\!\!\left(\bar{\bar{X^*}}\right)$};
\node [style=none] (24) at (-0.4, 2) {$\left(\bar{\bar{X^*}} \right)^*$};
\node [style=none] (25) at (-1.75, -2) {$\epsilon*$};
\node [style=none] (26) at (-2.5, 1) {$\eta*$};
\node [style=none] (27) at (-2.5, -3.5) {$X^{**}$};
\node [style=none] (28) at (-1.5, -0) {$X^*$};
\node [style=none] (29) at (-1.5, -1.25) {$\bar{\bar{X^*}}$};
\node [style=none] (30) at (-3.5, -5.25) {$\epsilon*$};
\node [style=none] (31) at (-4.5, -4.35) {$X^*$};
\node [style=none] (32) at (-5.25, -4.75) {$X$};
\node [style=circle, scale=2.5] (33) at (-4, -3.75) {};
\node [style=none] (34) at (-4, -3.75) {$\varphi^{-1}$};
\node [style=none] (35) at (-4.5, -2.3) {$*\eta$};
\node [style=none] (36) at (-3.75, -3) {$~^*X$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (13.center) to (14.center);
\draw [bend left=90, looseness=1.50] (13.center) to (12.center);
\draw [bend right=90, looseness=1.50] (11.center) to (10.center);
\draw [bend left=90, looseness=1.75] (9.center) to (8.center);
\draw (8.center) to (7);
\draw (7) to (6.center);
\draw [bend right=90, looseness=1.75] (6.center) to (5.center);
\draw (3.center) to (5.center);
\draw (3.center) to (1);
\draw (1) to (4.center);
\draw [bend right=90, looseness=1.75] (4.center) to (0.center);
\draw (0.center) to (2.center);
\draw [bend left=75, looseness=1.50] (2.center) to (15.center);
\draw (15.center) to (16.center);
\draw (9.center) to (10.center);
\draw (12.center) to (33);
\draw (33) to (11.center);
\end{pgfonlayer}
\end{tikzpicture} = %big3
\begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (-2, 3.5) {};
\node [style=circle, scale=2.5] (1) at (-1, 2.75) {};
\node [style=none] (2) at (-2, 2) {};
\node [style=none] (3) at (-1, 2) {};
\node [style=none] (4) at (-1, 3.5) {};
\node [style=none] (5) at (-1, -3.5) {};
\node [style=none] (6) at (-2, -3.5) {};
\node [style=circle, scale=2.5] (7) at (-2, -2.75) {};
\node [style=none] (8) at (-2, -2) {};
\node [style=none] (9) at (-2, -2) {};
\node [style=none] (10) at (-2, -0.5) {};
\node [style=none] (11) at (-3, -0.5) {};
\node [style=none] (12) at (-3, -5.25) {};
\node [style=none] (13) at (-2.75, 2) {};
\node [style=none] (14) at (-2.75, 4.5) {};
\node [style=none] (15) at (-1, 2.75) {$\psi^{-1}$};
\node [style=none] (16) at (-2, -2.75) {$\varepsilon^{-1}$};
\node [style=none] (17) at (-3.25, 4) {$\bar{\left(\bar{X^*}\right)^*}$};
\node [style=none] (18) at (-2.5, 1.5) {$\bar{\epsilon*}$};
\node [style=none] (19) at (-2.25, 2.75) {$\bar{\bar{X^*}}$};
\node [style=none] (20) at (-1.5, 4.25) {$*\eta$};
\node [style=none] (21) at (-0.5, 3.5) {$~^*(\bar{\bar{X^*}})$};
\node [style=none] (22) at (-0.5, 2) {$(\bar{\bar{X^*}})^*$};
\node [style=none] (23) at (-1.75, -4.25) {$\epsilon*$};
\node [style=none] (24) at (-1.5, -2.25) {$X^*$};
\node [style=none] (25) at (-1.5, -3.5) {$\bar{\bar{X^*}}$};
\node [style=none] (26) at (-2.5, -1.75) {$X^*$};
\node [style=none] (27) at (-3.25, -4.75) {$X$};
\node [style=circle, scale=2.5] (28) at (-2, -1.25) {};
\node [style=none] (29) at (-2, -1.25) {$\varphi^{-1}$};
\node [style=none] (30) at (-2.5, 0.25) {$*\eta$};
\node [style=none] (31) at (-1.75, -0.5) {$~^*X$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (11.center) to (12.center);
\draw [bend left=90, looseness=1.50] (11.center) to (10.center);
\draw (8.center) to (7);
\draw (7) to (6.center);
\draw [bend right=90, looseness=1.75] (6.center) to (5.center);
\draw (3.center) to (5.center);
\draw (3.center) to (1);
\draw (1) to (4.center);
\draw [bend right=90, looseness=1.75] (4.center) to (0.center);
\draw (0.center) to (2.center);
\draw [bend left=75, looseness=1.50] (2.center) to (13.center);
\draw (13.center) to (14.center);
\draw (10.center) to (28);
\draw (28) to (9.center);
\end{pgfonlayer}
\end{tikzpicture} = %big3
\begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (-2, 3.5) {};
\node [style=circle, scale=2.5] (1) at (-1, 2.75) {};
\node [style=none] (2) at (-2, 2) {};
\node [style=none] (3) at (-1, 2) {};
\node [style=none] (4) at (-1, 3.5) {};
\node [style=none] (5) at (-1, -3.5) {};
\node [style=none] (6) at (-3, -3.5) {};
\node [style=none] (7) at (-3, -2) {};
\node [style=none] (8) at (-3, -2) {};
\node [style=none] (9) at (-3, -0.5) {};
\node [style=none] (10) at (-4, -0.5) {};
\node [style=none] (11) at (-4, -5.25) {};
\node [style=none] (12) at (-2.75, 2) {};
\node [style=none] (13) at (-2.75, 4.5) {};
\node [style=none] (14) at (-1, 2.75) {$\psi^{-1}$};
\node [style=none] (15) at (-1, -1) {$\varepsilon^{-1^*}$};
\node [style=none] (16) at (-3.25, 4) {$\bar{\left(\bar{X^*}\right)^*}$};
\node [style=none] (17) at (-2.5, 1.5) {$\bar{\epsilon*}$};
\node [style=none] (18) at (-2.25, 2.75) {$\bar{\bar{X^*}}$};
\node [style=none] (19) at (-1.5, 4.25) {$*\eta$};
\node [style=none] (20) at (-0.5, 3.5) {$~^*(\bar{\bar{X^*}})$};
\node [style=none] (21) at (-0.5, -0) {$(\bar{\bar{X^*}})^*$};
\node [style=none] (22) at (-2, -4.75) {$\epsilon*$};
\node [style=none] (23) at (-2.5, -2) {$X^*$};
\node [style=none] (24) at (-4.25, -4.75) {$X$};
\node [style=circle, scale=2.5] (25) at (-3, -1.25) {};
\node [style=none] (26) at (-3, -1.25) {$\varphi^{-1}$};
\node [style=none] (27) at (-3.5, 0.25) {$*\eta$};
\node [style=none] (28) at (-2.75, -0.5) {$~^*X$};
\node [style=circle, scale=2.5] (29) at (-1, -1) {};
\node [style=none] (30) at (-0.5, -2) {$X^{**}$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (10.center) to (11.center);
\draw [bend left=90, looseness=1.50] (10.center) to (9.center);
\draw [bend right=90, looseness=1.75] (6.center) to (5.center);
\draw (3.center) to (1);
\draw (1) to (4.center);
\draw [bend right=90, looseness=1.75] (4.center) to (0.center);
\draw (0.center) to (2.center);
\draw [bend left=75, looseness=1.50] (2.center) to (12.center);
\draw (12.center) to (13.center);
\draw (9.center) to (25);
\draw (25) to (8.center);
\draw (7.center) to (6.center);
\draw (3.center) to (29);
\draw (29) to (5.center);
\end{pgfonlayer}
\end{tikzpicture} = %big4
\begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (-2, 3.5) {};
\node [style=circle, scale=2.5] (1) at (-1, 2.5) {};
\node [style=none] (2) at (-2, 2) {};
\node [style=none] (3) at (-1, 2) {};
\node [style=none] (4) at (-1, 3.5) {};
\node [style=none] (5) at (-1, -3.5) {};
\node [style=none] (6) at (-3, -3.5) {};
\node [style=none] (7) at (-3, -2) {};
\node [style=none] (8) at (-3, -2) {};
\node [style=none] (9) at (-3, -0.5) {};
\node [style=none] (10) at (-4, -0.5) {};
\node [style=none] (11) at (-4, -5.25) {};
\node [style=none] (12) at (-2.75, 2) {};
\node [style=none] (13) at (-2.75, 4.5) {};
\node [style=none] (14) at (-3.25, 4) {$\bar{\left(\bar{X^*}\right)^*}$};
\node [style=none] (15) at (-2.5, 1.5) {$\bar{\epsilon*}$};
\node [style=none] (16) at (-2.25, 2.75) {$\bar{\bar{X^*}}$};
\node [style=none] (17) at (-1.5, 4.25) {$*\eta$};
\node [style=none] (18) at (-0.5, 3.5) {$~^*(\bar{\bar{X^*}})$};
\node [style=none] (19) at (-2, -4.75) {$\epsilon*$};
\node [style=none] (20) at (-2.5, -2) {$X^*$};
\node [style=none] (21) at (-4.25, -4.75) {$X$};
\node [style=circle, scale=2.5] (22) at (-3, -1.25) {};
\node [style=none] (23) at (-3, -1.25) {$\psi^{-1}$};
\node [style=none] (24) at (-3.5, 0.25) {$*\eta$};
\node [style=none] (25) at (-2.75, -0.5) {$~^*X$};
\node [style=circle, scale=2.5] (26) at (-1, -1) {};
\node [style=none] (27) at (-1, -1) {$\psi^{-1}$};
\node [style=none] (28) at (-1, 2.5) {$~^*\varepsilon^{-1}$};
\node [style=none] (29) at (-0.5, 0.75) {$~^*(X^*)$};
\node [style=none] (30) at (-0.5, -2.5) {$X^{**}$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (10.center) to (11.center);
\draw [bend left=90, looseness=1.50] (10.center) to (9.center);
\draw [bend right=90, looseness=1.75] (6.center) to (5.center);
\draw (3.center) to (1);
\draw (1) to (4.center);
\draw [bend right=90, looseness=1.75] (4.center) to (0.center);
\draw (0.center) to (2.center);
\draw [bend left=75, looseness=1.50] (2.center) to (12.center);
\draw (12.center) to (13.center);
\draw (9.center) to (22);
\draw (22) to (8.center);
\draw (7.center) to (6.center);
\draw (3.center) to (26);
\draw (26) to (5.center);
\end{pgfonlayer}
\end{tikzpicture} =
\]

\[
\begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (-3, 3.5) {};
\node [style=none] (1) at (-3, 2) {};
\node [style=none] (2) at (0.5, 0.25) {};
\node [style=none] (3) at (-1, 3.5) {};
\node [style=none] (4) at (0.5, -1.75) {};
\node [style=none] (5) at (-3, -1.75) {};
\node [style=none] (6) at (-3, -2) {};
\node [style=none] (7) at (-3, -2) {};
\node [style=none] (8) at (-3, -0.5) {};
\node [style=none] (9) at (-4, -0.5) {};
\node [style=none] (10) at (-4, -5.25) {};
\node [style=none] (11) at (-3.75, 2) {};
\node [style=none] (12) at (-3.75, 4.5) {};
\node [style=none] (13) at (-4.25, 4) {$\bar{\left(\bar{X^*}\right)^*}$};
\node [style=none] (14) at (-3.5, 1.5) {$\bar{\epsilon*}$};
\node [style=none] (15) at (-3.25, 2.75) {$\bar{\bar{X^*}}$};
\node [style=none] (16) at (-2, 4.75) {$*\eta$};
\node [style=none] (17) at (-0.5, 3.5) {$~^*(\bar{\bar{X^*}})$};
\node [style=none] (18) at (-1, -4) {$\epsilon*$};
\node [style=none] (19) at (-2.5, -2) {$X^*$};
\node [style=none] (20) at (-4.25, -4.75) {$X$};
\node [style=circle, scale=2.5] (21) at (-3, -1.25) {};
\node [style=none] (22) at (-3, -1.25) {$\psi^{-1}$};
\node [style=none] (23) at (-3.5, 0.25) {$*\eta$};
\node [style=none] (24) at (-2.75, -0.5) {$~^*X$};
\node [style=circle, scale=2.5] (25) at (0.5, -1) {};
\node [style=none] (26) at (0.5, -1) {$\psi^{-1}$};
\node [style=none] (27) at (0.75, -0.25) {$~^*(X^*)$};
\node [style=none] (28) at (1, -2) {$X^{**}$};
\node [style=circle, scale=2.5] (29) at (-0.25, 1.75) {};
\node [style=none] (30) at (-0.25, 2.5) {};
\node [style=none] (31) at (-0.25, 1) {};
\node [style=none] (32) at (-1, 1) {};
\node [style=none] (33) at (0.5, 2.5) {};
\node [style=none] (34) at (0.5, 0.25) {};
\node [style=none] (35) at (-1, 3.5) {};
\node [style=none] (36) at (-0.25, 1.75) {$\varepsilon^{-1}$};
\node [style=none] (37) at (0.25, 3) {$~^*\eta$};
\node [style=none] (38) at (-0.75, 0.5) {$~^*\epsilon$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (9.center) to (10.center);
\draw [bend left=90, looseness=1.50] (9.center) to (8.center);
\draw [bend right=90, looseness=1.75] (5.center) to (4.center);
\draw [bend right=90, looseness=1.75] (3.center) to (0.center);
\draw (0.center) to (1.center);
\draw [bend left=75, looseness=1.50] (1.center) to (11.center);
\draw (11.center) to (12.center);
\draw (8.center) to (21);
\draw (21) to (7.center);
\draw (6.center) to (5.center);
\draw (2.center) to (25);
\draw (25) to (4.center);
\draw (29) to (31.center);
\draw [bend left=90, looseness=1.25] (31.center) to (32.center);
\draw (32.center) to (35.center);
\draw (30.center) to (29);
\draw [bend left=90, looseness=1.50] (30.center) to (33.center);
\draw (33.center) to (34.center);
\end{pgfonlayer}
\end{tikzpicture}
= %big6
\begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (0.5, 0.25) {};
\node [style=none] (1) at (0.5, -1.75) {};
\node [style=none] (2) at (-3, -1.75) {};
\node [style=none] (3) at (-3, -2) {};
\node [style=none] (4) at (-3, -2) {};
\node [style=none] (5) at (-3, -0.5) {};
\node [style=none] (6) at (-4, -0.5) {};
\node [style=none] (7) at (-4, -5.25) {};
\node [style=none] (8) at (-1.5, 2.75) {$\bar{\left(\bar{X^*}\right)^*}$};
\node [style=none] (9) at (-1, -4) {$\epsilon*$};
\node [style=none] (10) at (-2.5, -2) {$X^*$};
\node [style=none] (11) at (-4.25, -4.75) {$X$};
\node [style=circle, scale=2.5] (12) at (-3, -1.25) {};
\node [style=none] (13) at (-3, -1.25) {$\psi^{-1}$};
\node [style=none] (14) at (-3.5, 0.25) {$*\eta$};
\node [style=none] (15) at (-2.75, -0.5) {$~^*X$};
\node [style=circle, scale=2.5] (16) at (0.5, -1) {};
\node [style=none] (17) at (0.5, -1) {$\psi^{-1}$};
\node [style=none] (18) at (1, -0.25) {$~^*(X^*)$};
\node [style=none] (19) at (1, -2) {$X^{**}$};
\node [style=circle, scale=2.5] (20) at (-0.25, 1.75) {};
\node [style=none] (21) at (-0.25, 2.5) {};
\node [style=none] (22) at (-0.25, 1) {};
\node [style=none] (23) at (-1, 1) {};
\node [style=none] (24) at (0.5, 2.5) {};
\node [style=none] (25) at (0.5, 0.25) {};
\node [style=none] (26) at (-1, 3.5) {};
\node [style=none] (27) at (-0.25, 1.75) {$\varepsilon^{-1}$};
\node [style=none] (28) at (0.25, 3) {$~^*\eta$};
\node [style=none] (29) at (-0.75, 0.5) {$\bar{\epsilon*}$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (6.center) to (7.center);
\draw [bend left=90, looseness=1.50] (6.center) to (5.center);
\draw [bend right=90, looseness=1.75] (2.center) to (1.center);
\draw (5.center) to (12);
\draw (12) to (4.center);
\draw (3.center) to (2.center);
\draw (0.center) to (16);
\draw (16) to (1.center);
\draw (20) to (22.center);
\draw [bend left=90, looseness=1.25] (22.center) to (23.center);
\draw (23.center) to (26.center);
\draw (21.center) to (20);
\draw [bend left=90, looseness=1.50] (21.center) to (24.center);
\draw (24.center) to (25.center);
\end{pgfonlayer}
\end{tikzpicture}  \stackrel{{\bf \small [C.2](inv)}}{=} %big7
\begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (0.5, -0) {};
\node [style=none] (1) at (0.5, -2) {};
\node [style=none] (2) at (1.5, -2) {};
\node [style=none] (3) at (1.5, -0.5) {};
\node [style=none] (4) at (2.5, -0.5) {};
\node [style=none] (5) at (2.5, -5.25) {};
\node [style=none] (6) at (-1.5, 2.75) {$\bar{\left(\bar{X^*}\right)^*}$};
\node [style=none] (7) at (2.75, -4.75) {$X$};
\node [style=circle, scale=2.5] (8) at (-0.25, 1.75) {};
\node [style=none] (9) at (-0.25, 2.5) {};
\node [style=none] (10) at (-0.25, 1) {};
\node [style=none] (11) at (-1, 1) {};
\node [style=none] (12) at (0.5, 2.5) {};
\node [style=none] (13) at (0.5, -0) {};
\node [style=none] (14) at (-1, 3.5) {};
\node [style=none] (15) at (-0.25, 1.75) {$\varepsilon$};
\node [style=none] (16) at (0.25, 3) {$*\eta$};
\node [style=none] (17) at (-0.75, 0.5) {$\bar{\epsilon*}$};
\node [style=none] (18) at (-0.2, -1) {$~^*(X^*)$};
\node [style=none] (19) at (-0.5, 2.25) {};
\node [style=none] (20) at (1, -2.75) {$*\epsilon$};
\node [style=none] (21) at (1.85, -1) {$X^*$};
\node [style=none] (22) at (2, 0.25) {$\eta*$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (4.center) to (5.center);
\draw [bend right=90, looseness=1.50] (4.center) to (3.center);
\draw [bend left=90, looseness=1.75] (2.center) to (1.center);
\draw (8) to (10.center);
\draw [bend left=90, looseness=1.25] (10.center) to (11.center);
\draw (11.center) to (14.center);
\draw (9.center) to (8);
\draw [bend left=90, looseness=1.50] (9.center) to (12.center);
\draw (12.center) to (13.center);
\draw (0.center) to (1.center);
\draw (2.center) to (3.center);
\end{pgfonlayer}
\end{tikzpicture} = %big8
\begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (1.25, 0.5) {};
\node [style=none] (1) at (1.25, 2) {};
\node [style=none] (2) at (2.5, 2) {};
\node [style=none] (3) at (2.5, -5.25) {};
\node [style=none] (4) at (-0.75, 2.75) {$\bar{\left(\bar{X^*}\right)^*}$};
\node [style=none] (5) at (2.75, -4.75) {$X$};
\node [style=circle, scale=2.5] (6) at (1.25, -0.25) {};
\node [style=none] (7) at (1.25, 0.5) {};
\node [style=none] (8) at (1.25, -1) {};
\node [style=none] (9) at (0, -1) {};
\node [style=none] (10) at (0, 3.5) {};
\node [style=none] (11) at (1.25, -0.25) {$\varepsilon^{-1}$};
\node [style=none] (12) at (0.75, -1.75) {$\bar{\epsilon*}$};
\node [style=none] (13) at (1, 0.25) {};
\node [style=none] (14) at (1.5, 1.5) {$X^*$};
\node [style=none] (15) at (1.75, 2.75) {$\eta*$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (2.center) to (3.center);
\draw [bend right=90, looseness=1.50] (2.center) to (1.center);
\draw (6) to (8.center);
\draw [bend left=90, looseness=1.25] (8.center) to (9.center);
\draw (9.center) to (10.center);
\draw (7.center) to (6);
\draw (0.center) to (1.center);
\end{pgfonlayer}
\end{tikzpicture} =: \iota^{-1}
\]

\[
(b)~~~~ \begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (0, 4.75) {};
\node [style=none] (1) at (0, -0.5) {};
\node [style=none] (2) at (-0.75, -0.5) {};
\node [style=none] (3) at (-0.75, 2) {};
\node [style=none] (4) at (-1.5, 2) {};
\node [style=none] (5) at (-1.5, -0) {};
\node [style=none] (6) at (-2.5, -0) {};
\node [style=circle, scale=2.5] (7) at (-2.5, 1) {};
\node [style=none] (8) at (-2.5, 2.5) {};
\node [style=none] (9) at (-3.75, 2.5) {};
\node [style=none] (10) at (-3.75, -2.75) {};
\node [style=none] (11) at (-2.5, 1) {$\psi$};
\node [style=none] (12) at (-0.5, -1.25) {$\epsilon*$};
\node [style=none] (13) at (-1.25, 2.75) {$\bar{\eta*}$};
\node [style=none] (14) at (-2, -0.75) {$*\epsilon$};
\node [style=none] (15) at (-3, 3.5) {$\eta*$};
\node [style=circle, scale=2.5] (16) at (-3.75, -3.75) {};
\node [style=none] (17) at (-3.75, -4.75) {};
\node [style=none] (18) at (-2.5, -4.75) {};
\node [style=none] (19) at (-2.5, -3.5) {};
\node [style=none] (20) at (-1.25, -3.5) {};
\node [style=circle, scale=2.5] (21) at (-1.25, -6.75) {};
\node [style=none] (22) at (-1.25, -8) {};
\node [style=none] (23) at (-3.75, -3.75) {$\psi$};
\node [style=none] (24) at (-1.25, -6.75) {$\varepsilon$};
\node [style=none] (25) at (-2, -2.75) {$\eta*$};
\node [style=none] (26) at (-3, -5.5) {$*\epsilon$};
\node [style=none] (27) at (-4.75, 3.75) {};
\node [style=none] (28) at (1.25, 3.75) {};
\node [style=none] (29) at (-4.75, -1.5) {};
\node [style=none] (30) at (1.25, -1.5) {};
\node [style=none] (31) at (-5, -2.25) {};
\node [style=none] (32) at (-0.25, -2.25) {};
\node [style=none] (33) at (-0.25, -6) {};
\node [style=none] (34) at (-5, -6) {};
\node [style=none] (35) at (0.5, 4.5) {$\bar{\left( \bar{X^*} \right)^*}$};
\node [style=none] (36) at (-2.75, -2) {$\bar{\left(\bar{X} \right)^{**}}$};
\node [style=none] (37) at (-0.75, -7.5) {$X$};
\node [style=none] (38) at (-0.75, -5.25) {$\bar{X}$};
\node [style=none] (39) at (-2, -4) {$\bar{X}^*$};
\node [style=none] (40) at (-4.25, -4.5) {$~^*(\bar{X}^*)$};
\node [style=none] (41) at (-4.25, -3) {$\bar{X}^{**}$};
\node [style=none] (42) at (-4, 2) {$\bar{X}^{**}$};
\node [style=none] (43) at (0.5, 2.5) {$\bar{X^*}^*$};
\node [style=none] (44) at (-1.25, 1) {$\bar{X^*}$};
\node [style=none] (45) at (-3, 0.25) {$~^*\left(\bar{X^*} \right)$};
\node [style=none] (46) at (-3, 2) {$\left(\bar{X^*} \right)^*$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (0.center) to (1.center);
\draw [bend left=90, looseness=2.00] (1.center) to (2.center);
\draw (2.center) to (3.center);
\draw [bend right=90, looseness=1.50] (3.center) to (4.center);
\draw (4.center) to (5.center);
\draw [bend left=90, looseness=1.25] (5.center) to (6.center);
\draw (6.center) to (7);
\draw (7) to (8.center);
\draw [bend right=90, looseness=1.75] (8.center) to (9.center);
\draw (9.center) to (10.center);
\draw (10.center) to (16);
\draw (16) to (17.center);
\draw [bend right=90, looseness=1.50] (17.center) to (18.center);
\draw (18.center) to (19.center);
\draw [bend left=90, looseness=1.50] (19.center) to (20.center);
\draw (20.center) to (21);
\draw (21) to (22.center);
\draw (27.center) to (28.center);
\draw (28.center) to (30.center);
\draw (30.center) to (29.center);
\draw (29.center) to (27.center);
\draw (31.center) to (34.center);
\draw (34.center) to (33.center);
\draw (32.center) to (33.center);
\draw (32.center) to (31.center);
\end{pgfonlayer}
\end{tikzpicture} = %big10
\begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (0, 4.75) {};
\node [style=none] (1) at (0, -0.5) {};
\node [style=none] (2) at (-0.75, -0.5) {};
\node [style=none] (3) at (-0.75, 2) {};
\node [style=none] (4) at (-1.5, 2) {};
\node [style=none] (5) at (-1.5, -0) {};
\node [style=none] (6) at (-2.5, -0) {};
\node [style=circle, scale=2.5] (7) at (-2.5, 1) {};
\node [style=none] (8) at (-2.5, 2.5) {};
\node [style=none] (9) at (-3.75, 2.5) {};
\node [style=none] (10) at (-3.75, -2.75) {};
\node [style=none] (11) at (-2.5, 1) {$\psi$};
\node [style=none] (12) at (-0.5, -1.25) {$\epsilon*$};
\node [style=none] (13) at (-1.25, 2.75) {$\bar{\eta*}$};
\node [style=none] (14) at (-2, -0.75) {$*\epsilon$};
\node [style=none] (15) at (-3, 3.5) {$\eta*$};
\node [style=circle, scale=2.5] (16) at (-3.75, -3.75) {};
\node [style=none] (17) at (-3.75, -4.75) {};
\node [style=none] (18) at (-2.5, -4.75) {};
\node [style=none] (19) at (-2.5, -3.5) {};
\node [style=none] (20) at (-1.25, -3.5) {};
\node [style=circle, scale=2.5] (21) at (-1.25, -6.75) {};
\node [style=none] (22) at (-1.25, -8) {};
\node [style=none] (23) at (-3.75, -3.75) {$\psi$};
\node [style=none] (24) at (-1.25, -6.75) {$\varepsilon$};
\node [style=none] (25) at (-2, -2.75) {$\eta*$};
\node [style=none] (26) at (-3, -5.5) {$*\epsilon$};
\node [style=none] (27) at (-5.5, 3.75) {};
\node [style=none] (28) at (1.25, 3.75) {};
\node [style=none] (29) at (1.25, 3.75) {};
\node [style=none] (30) at (1.25, -6) {};
\node [style=none] (31) at (-5.5, -6) {};
\node [style=none] (32) at (0.5, 4.5) {$\bar{\left( \bar{X^*} \right)^*}$};
\node [style=none] (33) at (-2.75, -2) {$\bar{\left(\bar{X} \right)^{**}}$};
\node [style=none] (34) at (-0.75, -7.5) {$X$};
\node [style=none] (35) at (-0.75, -5.25) {$\bar{X}$};
\node [style=none] (36) at (-2, -4) {$\left(\bar{X}\right)^*$};
\node [style=none] (37) at (-4.5, -4.5) {$~^*(\left(\bar{X}\right)^*)$};
\node [style=none] (38) at (-4.5, -3) {$(\bar{X}^{**}$};
\node [style=none] (39) at (-4, 2) {$\bar{X}^{**}$};
\node [style=none] (40) at (0.5, 2.5) {$\bar{X^*}^*$};
\node [style=none] (41) at (-1.25, 1) {$\bar{X^*}$};
\node [style=none] (42) at (-3, 0.25) {$~^*\left(\bar{X^*} \right)$};
\node [style=none] (43) at (-3, 2) {$\left(\bar{X^*} \right)^*$};
\node [style=none] (44) at (0.75, -5.5) {$\bar{(\_)}$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (0.center) to (1.center);
\draw [bend left=90, looseness=2.00] (1.center) to (2.center);
\draw (2.center) to (3.center);
\draw [bend right=90, looseness=1.50] (3.center) to (4.center);
\draw (4.center) to (5.center);
\draw [bend left=90, looseness=1.25] (5.center) to (6.center);
\draw (6.center) to (7);
\draw (7) to (8.center);
\draw [bend right=90, looseness=1.75] (8.center) to (9.center);
\draw (9.center) to (10.center);
\draw (10.center) to (16);
\draw (16) to (17.center);
\draw [bend right=90, looseness=1.50] (17.center) to (18.center);
\draw (18.center) to (19.center);
\draw [bend left=90, looseness=1.50] (19.center) to (20.center);
\draw (20.center) to (21);
\draw (21) to (22.center);
\draw (27.center) to (28.center);
\draw (31.center) to (30.center);
\draw (29.center) to (30.center);
\draw (27.center) to (31.center);
\end{pgfonlayer}
\end{tikzpicture} \stackrel{{\bf [C.2]}}{=} %big11
\begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (0, 4.75) {};
\node [style=none] (1) at (0, -0.5) {};
\node [style=none] (2) at (-0.75, -0.5) {};
\node [style=none] (3) at (-0.75, 1.25) {};
\node [style=none] (4) at (-4.5, 1.25) {};
\node [style=none] (5) at (-4.5, -0.25) {};
\node [style=none] (6) at (-1.75, -4.75) {};
\node [style=none] (7) at (-1.75, -3.5) {};
\node [style=none] (8) at (-0.5, -3.5) {};
\node [style=circle, scale=2.5] (9) at (-0.5, -6.75) {};
\node [style=none] (10) at (-0.5, -8) {};
\node [style=none] (11) at (-0.5, -6.75) {$\varepsilon$};
\node [style=none] (12) at (-1.25, -2.75) {$\eta*$};
\node [style=none] (13) at (-5, 3.75) {};
\node [style=none] (14) at (1.25, 3.75) {};
\node [style=none] (15) at (1.25, 3.75) {};
\node [style=none] (16) at (1.25, -6) {};
\node [style=none] (17) at (-5, -6) {};
\node [style=none] (18) at (0.5, 4.5) {$\bar{\left( \bar{X^*} \right)^*}$};
\node [style=none] (19) at (0, -7.5) {$X$};
\node [style=none] (20) at (0, -5.25) {$\bar{X}$};
\node [style=none] (21) at (-1.25, -4) {$\left(\bar{X}\right)^*$};
\node [style=none] (22) at (0.5, 2.5) {$\bar{X^*}^*$};
\node [style=none] (23) at (0.75, -5.5) {$\bar{(\_)}$};
\node [style=none] (24) at (-2.25, -4.75) {};
\node [style=none] (25) at (-2.25, -1.25) {};
\node [style=none] (26) at (-3.25, -1.25) {};
\node [style=none] (27) at (-3.25, -2.5) {};
\node [style=none] (28) at (-4.5, -2.5) {};
\node [style=none] (29) at (-0.5, -1.25) {$\epsilon*$};
\node [style=none] (30) at (-2.5, 3.25) {$\bar{\eta*}$};
\node [style=none] (31) at (-4, -3.75) {$\epsilon*$};
\node [style=none] (32) at (-2.75, -0.75) {$*\eta$};
\node [style=none] (33) at (-2, -5.25) {$*\epsilon$};
\node [style=none] (34) at (-1.25, 0.75) {$\bar{X^*}$};
\node [style=none] (35) at (-4, 1) {$\bar{X}$};
\node [style=none] (36) at (-3.5, -2) {$\bar{X}^*$};
\node [style=none] (37) at (-1.75, -2.25) {$~^*(\bar{X}^*)$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (0.center) to (1.center);
\draw [bend left=90, looseness=2.00] (1.center) to (2.center);
\draw (2.center) to (3.center);
\draw [bend right=90, looseness=1.50] (3.center) to (4.center);
\draw (4.center) to (5.center);
\draw (6.center) to (7.center);
\draw [bend left=90, looseness=1.50] (7.center) to (8.center);
\draw (8.center) to (9);
\draw (9) to (10.center);
\draw (13.center) to (14.center);
\draw (17.center) to (16.center);
\draw (15.center) to (16.center);
\draw (13.center) to (17.center);
\draw [bend left=90, looseness=1.75] (6.center) to (24.center);
\draw (24.center) to (25.center);
\draw (27.center) to (26.center);
\draw [bend left=90, looseness=1.25] (26.center) to (25.center);
\draw [bend right=90, looseness=2.50] (28.center) to (27.center);
\draw (5.center) to (28.center);
\end{pgfonlayer}
\end{tikzpicture} = %big12
\begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (0, 4.75) {};
\node [style=none] (1) at (0, -0.5) {};
\node [style=none] (2) at (-0.75, -0.5) {};
\node [style=none] (3) at (-0.75, 1.25) {};
\node [style=none] (4) at (-4.5, 1.25) {};
\node [style=none] (5) at (-4.5, -0.25) {};
\node [style=circle, scale=2.5] (6) at (-2.25, -6.75) {};
\node [style=none] (7) at (-2.25, -8) {};
\node [style=none] (8) at (-2.25, -6.75) {$\varepsilon$};
\node [style=none] (9) at (-5, 3.75) {};
\node [style=none] (10) at (1.25, 3.75) {};
\node [style=none] (11) at (1.25, 3.75) {};
\node [style=none] (12) at (1.25, -6) {};
\node [style=none] (13) at (-5, -6) {};
\node [style=none] (14) at (0.5, 4.5) {$\bar{\left( \bar{X^*} \right)^*}$};
\node [style=none] (15) at (-1.75, -7.5) {$X$};
\node [style=none] (16) at (0.5, 2.5) {$\bar{X^*}^*$};
\node [style=none] (17) at (0.75, -5.5) {$\bar{(\_)}$};
\node [style=none] (18) at (-2.25, -1.25) {};
\node [style=none] (19) at (-3.25, -1.25) {};
\node [style=none] (20) at (-3.25, -2.5) {};
\node [style=none] (21) at (-4.5, -2.5) {};
\node [style=none] (22) at (-0.5, -1.25) {$\epsilon*$};
\node [style=none] (23) at (-2.5, 3.25) {$\bar{\eta*}$};
\node [style=none] (24) at (-4, -3.75) {$\epsilon*$};
\node [style=none] (25) at (-2.75, -0.75) {$\eta*$};
\node [style=none] (26) at (-1.25, 0.75) {$\bar{X^*}$};
\node [style=none] (27) at (-4, 1) {$\bar{X}$};
\node [style=none] (28) at (-3.5, -2) {$\bar{X}^*$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (0.center) to (1.center);
\draw [bend left=90, looseness=2.00] (1.center) to (2.center);
\draw (2.center) to (3.center);
\draw [bend right=90, looseness=1.50] (3.center) to (4.center);
\draw (4.center) to (5.center);
\draw (6) to (7.center);
\draw (9.center) to (10.center);
\draw (13.center) to (12.center);
\draw (11.center) to (12.center);
\draw (9.center) to (13.center);
\draw (20.center) to (19.center);
\draw [bend left=90, looseness=1.25] (19.center) to (18.center);
\draw [bend right=90, looseness=2.50] (21.center) to (20.center);
\draw (5.center) to (21.center);
\draw (18.center) to (6);
\end{pgfonlayer}
\end{tikzpicture}= \]

\[%big 14
\begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (0, 4.75) {};
\node [style=none] (1) at (0, -0.5) {};
\node [style=none] (2) at (-0.75, -0.5) {};
\node [style=none] (3) at (-0.75, 2) {};
\node [style=none] (4) at (-2.25, 2) {};
\node [style=circle, scale=2.5] (5) at (-2.25, -2.75) {};
\node [style=none] (6) at (-2.25, -4) {};
\node [style=none] (7) at (-2.25, -2.75) {$\varepsilon$};
\node [style=none] (8) at (-5, 3.75) {};
\node [style=none] (9) at (1.25, 3.75) {};
\node [style=none] (10) at (1.25, 3.75) {};
\node [style=none] (11) at (1.25, -2) {};
\node [style=none] (12) at (-5, -2) {};
\node [style=none] (13) at (0.75, 4.5) {$\bar{\left( \bar{X^*} \right)^*}$};
\node [style=none] (14) at (-1.75, -3.5) {$X$};
\node [style=none] (15) at (0.5, 2.5) {$\bar{X^*}^*$};
\node [style=none] (16) at (0.7499999, -1.5) {$\bar{(\_)}$};
\node [style=none] (17) at (-2.25, -1.25) {};
\node [style=none] (18) at (-0.5, -1.25) {$\epsilon*$};
\node [style=none] (19) at (-1.5, 3) {$\bar{\eta*}$};
\node [style=none] (20) at (-1.25, 0.75) {$\bar{X^*}$};
\node [style=none] (21) at (-1.75, 1.75) {$\bar{X}$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (0.center) to (1.center);
\draw [bend left=90, looseness=2.00] (1.center) to (2.center);
\draw (2.center) to (3.center);
\draw [bend right=90, looseness=1.50] (3.center) to (4.center);
\draw (5) to (6.center);
\draw (8.center) to (9.center);
\draw (12.center) to (11.center);
\draw (10.center) to (11.center);
\draw (8.center) to (12.center);
\draw (17.center) to (5);
\draw (4.center) to (17.center);
\end{pgfonlayer}
\end{tikzpicture} = %big15
\begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (-2.5, 4.75) {};
\node [style=none] (1) at (-2.5, -0.5) {};
\node [style=none] (2) at (-1, -0.5) {};
\node [style=none] (3) at (-1, 2) {};
\node [style=none] (4) at (0.5, 2) {};
\node [style=circle, scale=2.5] (5) at (0.4999999, -1.25) {};
\node [style=none] (6) at (0.4999999, -2.5) {};
\node [style=none] (7) at (0.4999999, -1.25) {$\varepsilon$};
\node [style=none] (8) at (-3, 4.5) {$\bar{\left( \bar{X^*} \right)^*}$};
\node [style=none] (9) at (0.9999999, -2) {$X$};
\node [style=none] (10) at (0.5, -1.25) {};
\node [style=none] (11) at (-1.75, -1.75) {$\bar{\epsilon*}$};
\node [style=none] (12) at (-0.25, 3) {$\bar{\bar{\eta*}}$};
\node [style=none] (13) at (-1.5, 1) {$\bar{\bar{X^*}}$};
\node [style=none] (14) at (1, 1) {$\bar{\bar{X}}$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (0.center) to (1.center);
\draw [bend right=90, looseness=2.00] (1.center) to (2.center);
\draw (2.center) to (3.center);
\draw [bend left=90, looseness=1.50] (3.center) to (4.center);
\draw (5) to (6.center);
\draw (10.center) to (5);
\draw (4.center) to (10.center);
\end{pgfonlayer}
\end{tikzpicture} \stackrel{\ref{Lemma: varepsi monoidal}}{=}
\begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=none] (0) at (1.25, 0.5) {};
\node [style=none] (1) at (1.25, 2) {};
\node [style=none] (2) at (2.5, 2) {};
\node [style=none] (3) at (2.5, -2.5) {};
\node [style=none] (4) at (-0.75, 2.75) {$\bar{\bar{X^*}^*}$};
\node [style=none] (5) at (2.75, -2) {$X$};
\node [style=circle, scale=2.5] (6) at (1.25, -0.25) {};
\node [style=none] (7) at (1.25, 0.5) {};
\node [style=none] (8) at (1.25, -1) {};
\node [style=none] (9) at (0, -1) {};
\node [style=none] (10) at (0, 3.5) {};
\node [style=none] (11) at (1.25, -0.25) {$\varepsilon^{-1}$};
\node [style=none] (12) at (0.75, -1.75) {$\bar{\epsilon*}$};
\node [style=none] (13) at (1, 0.25) {};
\node [style=none] (14) at (1.5, 1.5) {$X^*$};
\node [style=none] (15) at (1.75, 2.75) {$\eta*$};
\end{pgfonlayer}
\begin{pgfonlayer}{edgelayer}
\draw (2.center) to (3.center);
\draw [bend right=90, looseness=1.50] (2.center) to (1.center);
\draw (6) to (8.center);
\draw [bend left=90, looseness=1.25] (8.center) to (9.center);
\draw (9.center) to (10.center);
\draw (7.center) to (6);
\draw (0.center) to (1.center);
\end{pgfonlayer}
\end{tikzpicture} =: \iota^{-1}
\]