induction on the length of derivation of an equation that $H_{\cal C}$ and $K_{\cal C}$ are indeed functors. Next we verify by induction on the complexity of objects and arrow terms that $H_{\cal C}$ and $K_{\cal C}$ are inverse to each other. So the categories $\cal C$ and $\cal S_C$ are isomorphic.

Frobenius monads and self-adjunctions
=====================================

We want to prove the following result concerning the category *Frob* of the free Frobenius monad of Section 2 and the category $\cal S_A$ of the free self-adjunction of the preceding section.

We define first by induction a functor $I$ from *Frob* to $\cal S_A$:

=$I0=0$,=$I(n\pl
1)=GFIn$,=

$In=2n$,\
$I\varepsilon^\Box_n=\varphi_{2n}$,$I\delta^\Box_n=F\gamma_{2n+1}$,\
$I\varepsilon^\Diamond_n=\gamma_{2n}$,$I\delta^\Diamond_n=
F\varphi_{2n+1}$,$I\mj_n=\mj_{2n}$,\
$I(h_2\cirk h_1)=Ih_2\cirk Ih_1$,$IMh=FFIh$.

Next we define by induction a functor $J$ from $\cal S$ to *Frob*:

=$I0=0$,=$I(n\pl
1)=GFIn$,=

$J2n=n$,$J(2n\pl 1)=n\pl 1$,\
$J\varphi_{2n}=\varepsilon^\Box_n$,$J\gamma_{2n+1}=\delta^\Box_n$,\
$J\gamma_{2n}=\varepsilon^\Diamond_n$,$J\varphi_{2n+1}=\delta^\Diamond_n$, $J\mj_C\!=\mj_{JC}$,\
$J(h_2\cirk h_1)=Jh_2\cirk Jh_1$,$JFg=Jg$, for $g$ in $\cal
S_B$,$JF\!f\!=MJf$, for $f$ in $\cal S_A$.

We verify by induction on the length of derivation of an equation that $I$ and $J$ are indeed functors. We will not dwell on that verification for $I$, while for $J$ we have to verify first that $$J(h\cirk\varphi_n)=J(\varphi_m\cirk FFh).$$ If $h$ is from $\cal S_A$, then we use the equation ($\varepsilon^\Box$ [*nat*]{}) of Section 2. 