From f15664b37b4a7c34edb09f874d654735d6c0aea1 Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Thu, 15 Oct 2020 13:32:04 +0100
Subject: [PATCH 1/2] Add Monad for List

---
 src/Categories/Examples/Monad/Sets.agda | 32 +++++++++++++++++++++++++
 1 file changed, 32 insertions(+)
 create mode 100644 src/Categories/Examples/Monad/Sets.agda

diff --git a/src/Categories/Examples/Monad/Sets.agda b/src/Categories/Examples/Monad/Sets.agda
new file mode 100644
index 0000000..e16fd0d
--- /dev/null
+++ b/src/Categories/Examples/Monad/Sets.agda
@@ -0,0 +1,32 @@
+{-# OPTIONS --safe --without-K #-}
+module Categories.Examples.Monad.Sets where
+
+import Data.List as List
+import Data.List.Properties
+open import Relation.Binary.PropositionalEquality using (refl; sym)
+
+open import Categories.Category.Instance.Sets
+open import Categories.Monad using (Monad)
+open import Categories.NaturalTransformation using (ntHelper)
+
+import Categories.Examples.Functor.Sets as F
+
+List : ∀ {o} → Monad (Sets o)
+List = record
+  { F = F.List
+  ; η = record
+    { η = λ _ → List.[_]
+    ; commute = λ _ → refl
+    ; sym-commute = λ _ → refl
+    }
+  ; μ = ntHelper record
+    { η = λ _ → List.concat
+    ; commute = λ _ {x} → concat-map x
+    }
+  ; assoc = λ {_} {x} → concat-concat x
+  ; sym-assoc = λ {_} {x} → sym (concat-concat x)
+  ; identityˡ = concat-[-] _
+  ; identityʳ = ++-identityʳ _
+  }
+  where
+    open Data.List.Properties

From 43dc47eeade583738bf0fb598eb9671c62a359d4 Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Thu, 15 Oct 2020 13:33:23 +0100
Subject: [PATCH 2/2] Add function to turn proper Monads on Sets into RawMonads
 for do-notation

---
 src/Categories/Examples/Monad/Sets.agda | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/Categories/Examples/Monad/Sets.agda b/src/Categories/Examples/Monad/Sets.agda
index e16fd0d..f9665e5 100644
--- a/src/Categories/Examples/Monad/Sets.agda
+++ b/src/Categories/Examples/Monad/Sets.agda
@@ -1,6 +1,7 @@
 {-# OPTIONS --safe --without-K #-}
 module Categories.Examples.Monad.Sets where
 
+open import Category.Monad using (RawMonad)
 import Data.List as List
 import Data.List.Properties
 open import Relation.Binary.PropositionalEquality using (refl; sym)
@@ -11,6 +12,12 @@ open import Categories.NaturalTransformation using (ntHelper)
 
 import Categories.Examples.Functor.Sets as F
 
+Raw : ∀ {o} (M : Monad (Sets o)) → RawMonad (Monad.F.F₀ M)
+Raw M = record
+  { return = Monad.η.η M _
+  ; _>>=_ = λ Ma f → Monad.μ.η M _ (Monad.F.F₁ M f Ma)
+  }
+
 List : ∀ {o} → Monad (Sets o)
 List = record
   { F = F.List