Monad on a left adjoint induces a comonad on its right adjoint (source code)

= Monad on a left adjoint induces a comonad on its right adjoint

If an endofunctor $F$ has a right adjoint $G$ and $(F,\eta,\mu)$ is a <monad>, the <mate correspondence> turns $\eta:1\to F$ and $\mu:F^2\to F$ into a counit $G\to1$ and comultiplication $G\to G^2$. The reversed mate correspondence turns the monad laws into the comonad laws and identifies $F$-algebras with $G$-coalgebras.