From f7f8953a429aec43cd00382aeb5b8c562f1ef4c6 Mon Sep 17 00:00:00 2001
From: Andrea Vezzosi <sanzhiyan@gmail.com>
Date: Thu, 15 Mar 2018 13:39:42 +0000
Subject: [PATCH] Voe: Use the isomorphism directly for better computation

---
 src/Cat/Category/Monad.agda           |  5 +++++
 src/Cat/Category/Monad/Voevodsky.agda | 14 ++++----------
 2 files changed, 9 insertions(+), 10 deletions(-)

diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda
index d741ccd..3eef523 100644
--- a/src/Cat/Category/Monad.agda
+++ b/src/Cat/Category/Monad.agda
@@ -210,5 +210,10 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
     eqv : isEquiv M.Monad K.Monad forth
     eqv = gradLemma forth back fortheq backeq
 
+  open import Cat.Equivalence
+
+  Monoidal≅Kleisli : M.Monad ≅ K.Monad
+  Monoidal≅Kleisli = forth , (back , (record { verso-recto = funExt backeq ; recto-verso = funExt fortheq }))
+
   Monoidal≃Kleisli : M.Monad ≃ K.Monad
   Monoidal≃Kleisli = forth , eqv
diff --git a/src/Cat/Category/Monad/Voevodsky.agda b/src/Cat/Category/Monad/Voevodsky.agda
index 51cebec..5f27ed0 100644
--- a/src/Cat/Category/Monad/Voevodsky.agda
+++ b/src/Cat/Category/Monad/Voevodsky.agda
@@ -136,7 +136,7 @@ module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
   -- | to talk about voevodsky's construction.
   module _ (omap : Omap ℂ ℂ) (pure : {X : Object} → Arrow X (omap X)) where
     private
-      module E = Equivalence (Monoidal≃Kleisli ℂ)
+      module E = AreInverses (Monoidal≅Kleisli ℂ .proj₂ .proj₂)
 
       Monoidal→Kleisli : M.Monad → K.Monad
       Monoidal→Kleisli = E.obverse
@@ -184,22 +184,16 @@ module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
         where
         t' : ((Monoidal→Kleisli ∘ Kleisli→Monoidal) ∘ §2-3.§2.toMonad {omap} {pure})
           ≡ §2-3.§2.toMonad
-        t' = cong (\ φ → φ ∘ §2-3.§2.toMonad) {!re-ve!}
         cong-d : ∀ {ℓ} {A : Set ℓ} {ℓ'} {B : A → Set ℓ'} {x y : A}
           → (f : (x : A) → B x) → (eq : x ≡ y) → PathP (\ i → B (eq i)) (f x) (f y)
         cong-d f p = λ i → f (p i)
+        t' = cong (\ φ → φ ∘ §2-3.§2.toMonad) re-ve
         t : (§2-fromMonad ∘ (Monoidal→Kleisli ∘ Kleisli→Monoidal) ∘ §2-3.§2.toMonad {omap} {pure})
           ≡ (§2-fromMonad ∘ §2-3.§2.toMonad)
         t = cong-d (\ f → §2-fromMonad ∘ f) t'
         u : (§2-fromMonad ∘ (Monoidal→Kleisli ∘ Kleisli→Monoidal) ∘ §2-3.§2.toMonad) m
           ≡ (§2-fromMonad ∘ §2-3.§2.toMonad) m
-        u = cong (\ f → f m) t
-{-
-(K.RawMonad.omap (K.Monad.raw (?0 ℂ omap pure m i (§2-3.§2.toMonad m))) x)
-  = (omap x) : Object
-(K.RawMonad.pure (K.Monad.raw (?0 ℂ omap pure m x (§2-3.§2.toMonad x))))
-  = pure     : Arrow X (_350 ℂ omap pure m x x X)
--}
+        u = cong (\ φ → φ m) t
 
       backEq : ∀ m → (back ∘ forth) m ≡ m
       backEq m = begin
@@ -224,7 +218,7 @@ module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
         t : §1-fromMonad ∘ Kleisli→Monoidal ∘ Monoidal→Kleisli ∘ §2-3.§1.toMonad
           ≡ §1-fromMonad ∘ §2-3.§1.toMonad
         -- Why does `re-ve` not satisfy this goal?
-        t = cong (λ φ → §1-fromMonad ∘ φ ∘ §2-3.§1.toMonad) ({!ve-re!})
+        t i m = §1-fromMonad (ve-re i (§2-3.§1.toMonad m))
 
       voe-isEquiv : isEquiv (§2-3.§1 omap pure) (§2-3.§2 omap pure) forth
       voe-isEquiv = gradLemma forth back forthEq backEq