From f2164a6717be967a4a725a71c34a98981a4d58ba Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Thu, 1 Mar 2018 20:12:49 +0100
Subject: [PATCH] Prove equality principle for monads

---
 src/Cat/Category/Monad.agda | 39 +++++++++++++++++++++++++++++--------
 1 file changed, 31 insertions(+), 8 deletions(-)

diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda
index 26347a2..e582d63 100644
--- a/src/Cat/Category/Monad.agda
+++ b/src/Cat/Category/Monad.agda
@@ -7,7 +7,7 @@ open import Data.Product
 
 open import Cubical
 
-open import Cat.Category
+open import Cat.Category hiding (propIsAssociative)
 open import Cat.Category.Functor as F
 open import Cat.Category.NaturalTransformation
 open import Cat.Categories.Fun
@@ -103,13 +103,36 @@ module Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
       isMonad : IsMonad raw
     open IsMonad isMonad public
 
-  postulate propIsMonad : ∀ {raw} → isProp (IsMonad raw)
-  Monad≡ : {m n : Monad} → Monad.raw m ≡ Monad.raw n → m ≡ n
-  Monad.raw     (Monad≡ eq i) = eq i
-  Monad.isMonad (Monad≡ {m} {n} eq i) = res i
-    where
-      -- TODO: PathJ nightmare + `propIsMonad`.
-      postulate res : (λ i → IsMonad (eq i)) [ Monad.isMonad m ≡ Monad.isMonad n ]
+  private
+    module _ {m : RawMonad} where
+      open RawMonad m
+      propIsAssociative : isProp IsAssociative
+      propIsAssociative x y i {X}
+        = Category.arrowsAreSets ℂ _ _ (x {X}) (y {X}) i
+      propIsInverse : isProp IsInverse
+      propIsInverse x y i {X} = e1 i , e2 i
+        where
+        xX = x {X}
+        yX = y {X}
+        e1 = Category.arrowsAreSets ℂ _ _ (proj₁ xX) (proj₁ yX)
+        e2 = Category.arrowsAreSets ℂ _ _ (proj₂ xX) (proj₂ yX)
+    open IsMonad
+    propIsMonad : (raw : _) → isProp (IsMonad raw)
+    IsMonad.isAssociative (propIsMonad raw a b i) j
+      = propIsAssociative {raw}
+        (isAssociative a) (isAssociative b) i j
+    IsMonad.isInverse     (propIsMonad raw a b i)
+      = propIsInverse {raw}
+        (isInverse a) (isInverse b) i
+
+  module _ {m n : Monad} (eq : Monad.raw m ≡ Monad.raw n) where
+    open import Cubical.NType.Properties
+    eqIsMonad : (λ i → IsMonad (eq i)) [ Monad.isMonad m ≡ Monad.isMonad n ]
+    eqIsMonad = lemPropF propIsMonad eq
+
+    Monad≡ : m ≡ n
+    Monad.raw     (Monad≡ i) = eq i
+    Monad.isMonad (Monad≡ i) = eqIsMonad i
 
 -- "A monad in the Kleisli form" [voe]
 module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where