diff --git a/Lists/Map/Map.agda b/Lists/Map/Map.agda
index 1668510..e249424 100644
--- a/Lists/Map/Map.agda
+++ b/Lists/Map/Map.agda
@@ -32,6 +32,10 @@ mapExtension : {a b : _} {A : Set a} {B : Set b} (l : List A) (f g : A → B) 
 mapExtension [] f g pr = refl
 mapExtension (x :: l) f g pr rewrite mapExtension l f g pr | pr {x} = refl
 
+mapConcat : {a b : _} {A : Set a} {B : Set b} (l1 l2 : List A) (f : A → B) → map f (l1 ++ l2) ≡ (map f l1) ++ (map f l2)
+mapConcat [] l2 f = refl
+mapConcat (x :: l1) l2 f rewrite mapConcat l1 l2 f = refl
+
 lengthMap : {a b : _} {A : Set a} {B : Set b} → (l : List A) → {f : A → B} → length l ≡ length (map f l)
 lengthMap [] {f} = refl
 lengthMap (x :: l) {f} rewrite lengthMap l {f} = refl
diff --git a/Lists/Monad.agda b/Lists/Monad.agda
index 85f468e..db047ef 100644
--- a/Lists/Monad.agda
+++ b/Lists/Monad.agda
@@ -26,3 +26,32 @@ flatten=flatten' (l :: ls) = applyEquality (l ++_) (flatten=flatten' ls)
 lengthFlatten : {a : _} {A : Set a} (l : List (List A)) → length (flatten l) ≡ (fold _+N_ zero (map length l))
 lengthFlatten [] = refl
 lengthFlatten (l :: ls) rewrite lengthConcat l (flatten ls) | lengthFlatten ls = refl
+
+flattenConcat : {a : _} {A : Set a} (l1 l2 : List (List A)) → flatten (l1 ++ l2) ≡ (flatten l1) ++ (flatten l2)
+flattenConcat [] l2 = refl
+flattenConcat (l1 :: ls) l2 rewrite flattenConcat ls l2 | concatAssoc l1 (flatten ls) (flatten l2) = refl
+
+pure : {a : _} {A : Set a} → A → List A
+pure a = [ a ]
+
+bind : {a b : _} {A : Set a} {B : Set b} → (f : A → List B) → List A → List B
+bind f l = flatten (map f l)
+
+private
+  leftIdentLemma : {a : _} {A : Set a} (xs : List A) → flatten (map pure xs) ≡ xs
+  leftIdentLemma [] = refl
+  leftIdentLemma (x :: xs) rewrite leftIdentLemma xs = refl
+
+leftIdent : {a b : _} {A : Set a} {B : Set b} → (f : A → List B) → {x : A} → bind pure (f x) ≡ f x
+leftIdent f {x} with f x
+leftIdent f {x} | [] = refl
+leftIdent f {x} | y :: ys rewrite leftIdentLemma ys = refl
+
+rightIdent : {a b : _} {A : Set a} {B : Set b} → (f : A → List B) → {x : A} → bind f (pure x) ≡ f x
+rightIdent f {x} with f x
+rightIdent f {x} | [] = refl
+rightIdent f {x} | y :: ys rewrite appendEmptyList ys = refl
+
+associative : {a b c : _} {A : Set a} {B : Set b} {C : Set c} → (f : A → List B) (g : B → List C) → {x : List A} → bind g (bind f x) ≡ bind (λ a → bind g (f a)) x
+associative f g {[]} = refl
+associative f g {x :: xs} rewrite mapConcat (f x) (flatten (map f xs)) g | flattenConcat (map g (f x)) (map g (flatten (map f xs))) = applyEquality (flatten (map g (f x)) ++_) (associative f g {xs})