Cofree coalgebra (source code)

= Cofree coalgebra
{title2=$R(X)=(GX,\delta_X)$}

For a <comonad>, the cofree coalgebra on $X$ is $(GX,\delta_X)$. A map $UA\to X$ transposes to the coalgebra morphism $Gf\,a:A\to GX$. This gives the <adjunction> $U\dashv R$ with the <forgetful functor>.