us, because it is at the base of a more complicated result concerning *Frob* that we establish in Section 5.

This isomorphism is proved syntactically by defining first by induction a functor $I$ from $\cal  M$ to $\cal  B$ for which we have

=$I0=0$,=$I(n\pl
1)=GFIn$,=\
$I\varepsilon^\Diamond_n=\gamma_{In}$,$I\delta^\Diamond_n=G\varphi_{FIn}$,$I\mj_n=\mj_{In}$,\
$I(h_2\cirk h_1)=Ih_2\cirk Ih_1$,$IMh=GFIh$.

We verify that $I$ is indeed a functor by induction on the length of derivation of an equation of $\cal  M$.

Next we define by induction a functor $J$ from the category ${\cal
B}+{\cal A}$, which is the disjoint union of the categories $\cal
B$ and $\cal  A$ of the free adjunction, to the category $\cal M$. For $J$ we have

=$J0=0$,=$JGFB=JFB=JB\pl
1$,=\
$J\gamma_B=\varepsilon^\Diamond_{JB}$,$J\varphi_A=\delta^\Diamond_{JA-1}$, $J\mj_C=\mj_{JC}$,\
$J(h_2\cirk h_1)=Jh_2\cirk Jh_1$,$JGf=Jf$,$JFg=MJg$.

To verify that $J$ is indeed a functor, which is done by induction on the length of derivation of an equation, we had to define it from ${\cal B}+{\cal A}$, but there is an obvious functor $J_{\cal
B}$ from $\cal  B$ to $\cal  M$ obtained by restricting $J$.

It is straightforward to verify by induction on the complexity of objects and arrow terms that $I$ and $J_{\cal B}$ are inverse to each other. So the categories $\cal  M$ and $\cal  B$ are isomorphic.

