Monad: add join

Author: liyishuai

theories/Structures/Monad.v

@@ -1,3 +1,5 @@
+From Coq Require Import
+     Basics.
 Require Import ExtLib.Core.Any.
 Require Import ExtLib.Structures.Functor.
 Require Import ExtLib.Structures.Applicative.
@@ -47,6 +49,8 @@ Section monadic.
              (f: T -> m U) (g: U -> m V): (T -> m V) :=
     fun x => bind (f x) g.
 
+  Definition join {m a} `{Monad m} : m (m a) -> m a := flip bind id.
+
 End monadic.
 
 Module MonadBaseNotation.