From 5d9c820fa2a8c31d13f07bc55707129d4e47515f 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 15:25:07 +0100
Subject: [PATCH] Add note about haskell

---
 src/Cat/Category/Monad.agda | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda
index 31b4c47..d4084ef 100644
--- a/src/Cat/Category/Monad.agda
+++ b/src/Cat/Category/Monad.agda
@@ -88,7 +88,18 @@ module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
       -- Note name-change from [voe]
       ζ : {X : Object} → ℂ [ X , RR X ]
       rr : {X Y : Object} → ℂ [ X , RR Y ] → ℂ [ RR X , RR Y ]
-    -- Name suggestions are welcome!
+    -- Note the correspondance with Haskell:
+    --
+    --     RR ~ m
+    --     ζ  ~ pure
+    --     rr ~ flip (>>=)
+    --
+    -- Where those things have these types:
+    --
+    --     m : 𝓤 → 𝓤
+    --     pure : x → m x
+    --     flip (>>=) :: (a → m b) → m a → m b
+    --
     IsIdentity     = {X : Object}
       → rr ζ ≡ 𝟙 {RR X}
     IsNatural      = {X Y : Object}   (f : ℂ [ X , RR Y ])