From e3eca8d90acf7330b6f91cabb93bd0c45ad6bc0d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Tue, 1 May 2018 11:33:12 +0200
Subject: [PATCH] Prove other identity-law for monads

---
 src/Cat/Category/Monad/Kleisli.agda | 15 ++++++++++++++-
 src/Cat/Category/Product.agda       |  2 --
 2 files changed, 14 insertions(+), 3 deletions(-)

diff --git a/src/Cat/Category/Monad/Kleisli.agda b/src/Cat/Category/Monad/Kleisli.agda
index 55e9cf5..bdb4966 100644
--- a/src/Cat/Category/Monad/Kleisli.agda
+++ b/src/Cat/Category/Monad/Kleisli.agda
@@ -50,13 +50,19 @@ record RawMonad : Set ℓ where
 
   -- There may be better names than what I've chosen here.
 
+  -- `pure` is the neutral element for `bind`
   IsIdentity     = {X : Object}
     → bind pure ≡ identity {omap X}
+  -- pure is the left-identity for the kleisli arrow.
   IsNatural      = {X Y : Object}   (f : ℂ [ X , omap Y ])
-    → pure >>> (bind f) ≡ f
+    → pure >=> f ≡ f
+  -- Composition interacts with bind in the following way.
   IsDistributive = {X Y Z : Object} (g : ℂ [ Y , omap Z ]) (f : ℂ [ X , omap Y ])
     → (bind f) >>> (bind g) ≡ bind (f >=> g)
 
+  RightIdentity = {A B : Object} {m : ℂ [ A , omap B ]}
+    → m >=> pure ≡ m
+
   -- | Functor map fusion.
   --
   -- This is really a functor law. Should we have a kleisli-representation of
@@ -215,6 +221,13 @@ record IsMonad (raw : RawMonad) : Set ℓ where
       bind pure ≡⟨ isIdentity ⟩
       identity ∎
 
+  rightIdentity : RightIdentity
+  rightIdentity {m = m} = begin
+    m >=> pure      ≡⟨⟩
+    m >>> bind pure ≡⟨ cong (m >>>_) isIdentity ⟩
+    m >>> identity  ≡⟨ ℂ.leftIdentity ⟩
+    m ∎
+
 record Monad : Set ℓ where
   field
     raw : RawMonad
diff --git a/src/Cat/Category/Product.agda b/src/Cat/Category/Product.agda
index 7f7ddbe..8dcc9a4 100644
--- a/src/Cat/Category/Product.agda
+++ b/src/Cat/Category/Product.agda
@@ -215,8 +215,6 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
               coe pA xa ≡⟨ ℂ.coe-dom iso ⟩
               xa ℂ.<<< fst f~ ≡⟨ fst (snd f~) ⟩
               ya ∎
-            helper : PathP (λ i → pA i) xa ya
-            helper = coe-lem-inv k1
           in iso , coe-lem-inv k1 , coe-lem-inv k0})
         , funExt (λ x → lemSig
             (λ x → propSig prop0 (λ _ → prop1))