Bundled monad morphisms as cslib's IsMonadHom

PolyFun's MonadHom bundles a family of maps with its pure and bind laws; cslib's IsMonadHom is the unbundled predicate on such a family, requiring preservation of every Functor / Applicative / Monad operator. For lawful monads the two agree, and this module supplies the direction PolyFun consumes: every bundled morphism satisfies the predicate, so cslib's transport lemmas (IsMonadHom.map_listMapM, IsMonadHom.map_pfunctorFreeMLiftM, …) apply to it. It is separate from PolyFun.Control.Monad.Hom so consumers of the base morphism API do not acquire the cslib dependency unless they use it.

theorem MonadHom.isMonadHom {m : Type u → Type v} {n : Type u → Type w} [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n] (F : m →ᵐ n) : Cslib.IsMonadHom m n fun {x : Type u} (x_1 : m x) => (fun {α : Type u} (x : m α) => F.toFun α x) x_1

A bundled monad morphism between lawful monads is a monad morphism in cslib's sense.