From e7abab0e4c6bf57a40df5742274a7f8cf9b1d61c 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 19:08:20 +0100
Subject: [PATCH] Add `pure` and `>=>` to kleisli category

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

diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda
index 9263c9b..2a4f0a3 100644
--- a/src/Cat/Category/Monad.agda
+++ b/src/Cat/Category/Monad.agda
@@ -84,6 +84,15 @@ module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
     --     pure : x → m x
     --     flip (>>=) :: (a → m b) → m a → m b
     --
+    pure : {X : Object} → ℂ [ X , RR X ]
+    pure = ζ
+    -- Why is (>>=) not implementable?
+    --
+    -- (>>=) : m a -> (a -> m b) -> m b
+    -- (>=>) : (a -> m b) -> (b -> m c) -> a -> m c
+    _>=>_ : {A B C : Object} → ℂ [ A , RR B ] → ℂ [ B , RR C ] → ℂ [ A , RR C ]
+    f >=> g = ℂ [ rr g ∘ f ]
+
     IsIdentity     = {X : Object}
       → rr ζ ≡ 𝟙 {RR X}
     IsNatural      = {X Y : Object}   (f : ℂ [ X , RR Y ])