Solution (source code)

= Solution

For the <monad> $(T,\eta,\mu)$, an <algebra for a monad> is $(A,a:TA\to A)$ with $a\eta_A=1_A$ and $aT(a)=a\mu_A$. A <morphism of algebras for a monad> $f:(A,a)\to(B,b)$ satisfies $fa=bTf$. These objects and arrows form the <Eilenberg-Moore category> $\mathcal C^T$.

The <free algebra functor> sends $A$ to $(TA,\mu_A)$ and $f$ to $Tf$. The monad identities verify the algebra laws. For the forgetful <functor> $U$, the free adjunction is
$$
\mathcal C^T((TA,\mu_A),(B,b))\cong\mathcal C(A,B),\qquad h\mapsto h\eta_A,
$$
with inverse $v\mapsto bTv$. The algebra law makes the latter an <monad algebra morphism>. The identities $h\eta_A\mapsto bT(h\eta_A)=h\mu_AT\eta_A=h$ and $bTv\eta_A=b\eta_Bv=v$ prove the <bijection>.

In the <category of adjunctions inducing a fixed monad>, objects are adjunctions $F\dashv G$ with their induced monad identified with $T$. A <morphism> to $F'\dashv G'$ is a <functor> $H$ between the right-hand <categories> satisfying $G'H=G$, $HF=F'$ and compatibility with units and counits. With these strict identifications, define
$$
K(B)=(GB,G\varepsilon_B),\qquad K(f)=Gf.
$$
The triangle identities give the unit algebra law; naturality of $\varepsilon$ at $\varepsilon_B$ gives the multiplication law. Naturality at $f$ makes $Gf$ an <monad algebra morphism>. Moreover $UK=G$, $KF=F^T$ because $G\varepsilon_{FA}=\mu_A$, and $K\varepsilon_B$ is the free-adjunction counit at $K(B)$. Hence $K$ is a <morphism> into the Eilenberg-Moore adjunction.

For any other such $H$, its underlying object at $B$ must be $GB$. Counit compatibility forces its algebra action to be $G\varepsilon_B$, and the forgetful <functor>, which is a <faithful functor>, forces $H(f)=Gf$. Thus $H=K$. This proves <terminality of the Eilenberg-Moore adjunction>. If adjunctions are specified only up to coherent <isomorphisms>, the same argument gives uniqueness up to the corresponding compatible <natural isomorphism>.