fact: Record Monad : Type := mkMonad { monad_tyop :> Type -> Type ; monad_ret : forall A, A -> monad_tyop A ; monad_bind : forall A B, monad_tyop A -> (A -> monad_tyop B) -> monad_tyop B ; monad_law1 : forall A B a (f : A -> monad_tyop B), monad_bind (monad_ret a) f = f a ; monad_law2 : forall A c, monad_bind c (@monad_ret A) = c ; monad_law3 : forall A B C c (f : A -> monad_tyop B) (g : B -> monad_tyop C), monad_bind (monad_bind c f) g = monad_bind c (fun a => monad_bind (f a) g) }.
imports: Coq(ssreflect ssrfun FunctionalExtensionality) Mon(SPropBase) Coq(Relation_Definitions Morphisms)