Require Export
  HoTT.Classes.interfaces.canonical_names.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

Class Monad (M : Type -> Type) {Mret : Return M} {Mbind : Bind M} :=
  { monad_ret_bind : forall {A B} a (f : A -> M B), bind (ret a) f = f a
  ; monad_bind_ret : forall {A} (x : M A), bind x ret = x
  ; monad_bind_assoc : forall {A B C} x (f : A -> M B) (g : B -> M C),
    bind (bind x f) g = bind x (fun a => bind (f a) g) }.