Corestriction functor for comodules (source code)

= Corestriction functor for comodules
{title2=$f_*$}

A <comonoid morphism> $f:H\to K$ induces a <functor> $f_*$ on right <comodules>, replacing $\rho$ by $(1\otimes f)\rho$ and preserving underlying objects and arrows. For <bimonoids>, it is strict monoidal exactly when $f$ is also a <monoid morphism>.