From 4ec13fe5094190519604730acfa8bb0d5d10940a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sat, 24 Feb 2018 14:00:52 +0100
Subject: [PATCH] Implement monads in the kleisli form

---
 BACKLOG.md                  |  8 ++++++++
 src/Cat/Category/Monad.agda | 37 +++++++++++++++++++++++++++++++++++--
 2 files changed, 43 insertions(+), 2 deletions(-)

diff --git a/BACKLOG.md b/BACKLOG.md
index c791f61..bfbb32b 100644
--- a/BACKLOG.md
+++ b/BACKLOG.md
@@ -4,3 +4,11 @@ Backlog
 Prove univalence for various categories
 
 Prove postulates in `Cat.Wishlist`
+
+* Functor ✓
+* Applicative Functor ✗
+  * Lax monoidal functor ✗
+    * Monoidal functor ✗
+  * Tensorial strength ✗
+* Category ✓
+  * Monoidal category ✗
\ No newline at end of file
diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda
index acd54fc..0400ba1 100644
--- a/src/Cat/Category/Monad.agda
+++ b/src/Cat/Category/Monad.agda
@@ -27,9 +27,10 @@ module Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
       -- (>=>)
       μNat : NaturalTransformation F[ R ∘ R ] R
 
-    module R  = Functor R
-    module RR = Functor F[ R ∘ R ]
+
     private
+      module R  = Functor R
+      module RR = Functor F[ R ∘ R ]
       module _ {X : Object} where
         -- module IdRX = Functor (F.identity {C = RX})
 
@@ -69,3 +70,35 @@ module Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
     field
       isAssociative : IsAssociative
       isInverse : IsInverse
+
+-- "A monad in the Kleisli form" [vlad]
+module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
+  private
+    ℓ = ℓa ⊔ ℓb
+
+  open Category ℂ hiding (IsIdentity)
+  record RawMonad : Set ℓ where
+    field
+      RR : Object → Object
+      η : {X : Object} → ℂ [ X , RR X ]
+      rr : {X Y : Object} → ℂ [ X , RR Y ] → ℂ [ RR X , RR Y ]
+    -- Name suggestions are welcome!
+    IsIdentity     = {X : Object}
+      → rr η ≡ 𝟙 {RR X}
+    IsNatural      = {X Y : Object}   (f : ℂ [ X , RR Y ])
+      → (ℂ [ rr f ∘ η ]) ≡ f
+    IsDistributive = {X Y Z : Object} (g : ℂ [ Y , RR Z ]) (f : ℂ [ X , RR Y ])
+      → ℂ [ rr g ∘ rr f ] ≡ rr (ℂ [ rr g ∘ f ])
+
+  record IsMonad (raw : RawMonad) : Set ℓ where
+    open RawMonad raw public
+    field
+      isIdentity     : IsIdentity
+      isNatural      : IsNatural
+      isDistributive : IsDistributive
+
+  record Monad : Set ℓ where
+    field
+      raw : RawMonad
+      isMonad : IsMonad raw
+    open IsMonad isMonad public