fact: Record MonadAlgebra (M : Monad) : Type := mkMonadAlgebra { malg_carrier : Type ; malg_map :> M malg_carrier -> malg_carrier ; malg_ret : forall c, malg_map (ret c) = c ; malg_bind : forall X (m : M X) f, malg_map (bind m (fun x => ret (malg_map (f x)))) = malg_map (bind m f) }.
imports: Coq(ssreflect ssrfun FunctionalExtensionality) Mon(SPropBase) Coq(Relation_Definitions Morphisms)