Prove other identity-law for monads

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

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))