 Corestriction functor for comodules

A comonoid morphism $f:H\to K$ induces a functor $f_{\ast }$ 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.