no-eta-equality for monads speeds up Voevodsky

src/Cat/Category/Monad/Kleisli.agda

@@ -230,6 +230,7 @@ record IsMonad (raw : RawMonad) : Set ℓ where
     m ∎
 
 record Monad : Set ℓ where
+  no-eta-equality
   field
     raw : RawMonad
     isMonad : IsMonad raw

src/Cat/Category/Monad/Monoidal.agda

@@ -123,6 +123,7 @@ record IsMonad (raw : RawMonad) : Set ℓ where
         ∎
 
 record Monad : Set ℓ where
+  no-eta-equality
   field
     raw     : RawMonad
     isMonad : IsMonad raw

src/Cat/Category/Monad/Voevodsky.agda

@@ -25,6 +25,7 @@ module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
 
   module §2-3 (omap : Object → Object) (pure : {X : Object} → Arrow X (omap X)) where
     record §1 : Set ℓ where
+      no-eta-equality
       open M
 
       field
@@ -75,12 +76,11 @@ module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
         isMonad : IsMonad rawMnd
 
       toMonad : Monad
-      toMonad = record
+      toMonad .Monad.raw = rawMnd
-        { raw     = rawMnd
+      toMonad .Monad.isMonad = isMonad
-        ; isMonad = isMonad
-        }
 
     record §2 : Set ℓ where
+      no-eta-equality
       open K
 
       field
@@ -97,28 +97,24 @@ module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
         isMonad : IsMonad rawMnd
 
       toMonad : Monad
-      toMonad = record
+      toMonad .Monad.raw     = rawMnd
-        { raw     = rawMnd
+      toMonad .Monad.isMonad = isMonad
-        ; isMonad = isMonad
-        }
 
-  §1-fromMonad : (m : M.Monad) → §2-3.§1 (M.Monad.Romap m) (λ {X} → M.Monad.pureT m X)
+  module _ (m : M.Monad) where
-  §1-fromMonad m = record
-    { fmap       = Functor.fmap R
-    ; RisFunctor = Functor.isFunctor R
-    ; pureN      = pureN
-    ; join       = λ {X} → joinT X
-    ; joinN      = joinN
-    ; isMonad    = M.Monad.isMonad m
-    }
-    where
     open M.Monad m
 
+    §1-fromMonad : §2-3.§1 (M.Monad.Romap m) (λ {X} → M.Monad.pureT m X)
+    §1-fromMonad .§2-3.§1.fmap       = Functor.fmap R
+    §1-fromMonad .§2-3.§1.RisFunctor = Functor.isFunctor R
+    §1-fromMonad .§2-3.§1.pureN      = pureN
+    §1-fromMonad .§2-3.§1.join      {X} = joinT X
+    §1-fromMonad .§2-3.§1.joinN      = joinN
+    §1-fromMonad .§2-3.§1.isMonad    = M.Monad.isMonad m
+
+
   §2-fromMonad : (m : K.Monad) → §2-3.§2 (K.Monad.omap m) (K.Monad.pure m)
-  §2-fromMonad m = record
+  §2-fromMonad m .§2-3.§2.bind    = K.Monad.bind    m
-    { bind    = K.Monad.bind    m
+  §2-fromMonad m  .§2-3.§2.isMonad = K.Monad.isMonad m
-    ; isMonad = K.Monad.isMonad m
-    }
 
   -- | In the following we seek to transform the equivalence `Monoidal≃Kleisli`
   -- | to talk about voevodsky's construction.
@@ -145,65 +141,43 @@ module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
       back = §1-fromMonad ∘ Kleisli→Monoidal ∘ §2-3.§2.toMonad
 
       forthEq : ∀ m → (forth ∘ back) m ≡ m
-      forthEq m = begin
+      forthEq m = trans
-        (forth ∘ back) m ≡⟨⟩
+                  (trans (cong-d (§2-fromMonad ∘ Monoidal→Kleisli) (lemmaz (Kleisli→Monoidal (§2-3.§2.toMonad m))))
-        -- In full gory detail:
+                         (cong-d (\ φ → §2-fromMonad (φ (§2-3.§2.toMonad m))) re-ve))
-        ( §2-fromMonad
+                         lemma
-        ∘ Monoidal→Kleisli
-        ∘ §2-3.§1.toMonad
-        ∘ §1-fromMonad
-        ∘ Kleisli→Monoidal
-        ∘ §2-3.§2.toMonad
-        ) m ≡⟨⟩ -- fromMonad and toMonad are inverses
-        ( §2-fromMonad
-        ∘ Monoidal→Kleisli
-        ∘ Kleisli→Monoidal
-        ∘ §2-3.§2.toMonad
-        ) m ≡⟨ cong (λ φ → φ m) t ⟩
-        -- Monoidal→Kleisli and Kleisli→Monoidal are inverses
-        -- I should be able to prove this using congruence and `lem` below.
-        ( §2-fromMonad
-        ∘ §2-3.§2.toMonad
-        ) m ≡⟨⟩
-        (  §2-fromMonad
-        ∘ §2-3.§2.toMonad
-        ) m ≡⟨⟩ -- fromMonad and toMonad are inverses
-        m ∎
         where
-        t' : ((Monoidal→Kleisli ∘ Kleisli→Monoidal) ∘ §2-3.§2.toMonad {omap} {pure})
+        lemma : (§2-fromMonad ∘ §2-3.§2.toMonad) m ≡ m
-          ≡ §2-3.§2.toMonad
+        §2-3.§2.bind (lemma i) = §2-3.§2.bind m
-        t' = cong (\ φ → φ ∘ §2-3.§2.toMonad) re-ve
+        §2-3.§2.isMonad (lemma i) = §2-3.§2.isMonad m
-        t : (§2-fromMonad ∘ (Monoidal→Kleisli ∘ Kleisli→Monoidal) ∘ §2-3.§2.toMonad {omap} {pure})
+        lemmaz : ∀ m → §2-3.§1.toMonad (§1-fromMonad m) ≡ m
-          ≡ (§2-fromMonad ∘ §2-3.§2.toMonad)
+        M.Monad.raw (lemmaz m i) = M.Monad.raw m
-        t = cong-d (\ f → §2-fromMonad ∘ f) t'
+        M.Monad.isMonad (lemmaz m i) = M.Monad.isMonad m
-        u : (§2-fromMonad ∘ (Monoidal→Kleisli ∘ Kleisli→Monoidal) ∘ §2-3.§2.toMonad) m
-          ≡ (§2-fromMonad ∘ §2-3.§2.toMonad) m
-        u = cong (\ φ → φ m) t
 
       backEq : ∀ m → (back ∘ forth) m ≡ m
-      backEq m = begin
+      backEq m = trans (cong-d (§1-fromMonad ∘ Kleisli→Monoidal) (lemma (Monoidal→Kleisli (§2-3.§1.toMonad m))))
-        (back ∘ forth) m ≡⟨⟩
+                 (trans (cong-d (\ φ → §1-fromMonad (φ (§2-3.§1.toMonad m))) ve-re)
-        ( §1-fromMonad
+                        lemmaz)
-        ∘ Kleisli→Monoidal
-        ∘ §2-3.§2.toMonad
-        ∘ §2-fromMonad
-        ∘ Monoidal→Kleisli
-        ∘ §2-3.§1.toMonad
-        ) m ≡⟨⟩ -- fromMonad and toMonad are inverses
-        ( §1-fromMonad
-        ∘ Kleisli→Monoidal
-        ∘ Monoidal→Kleisli
-        ∘ §2-3.§1.toMonad
-        ) m ≡⟨ cong (λ φ → φ m) t ⟩ -- Monoidal→Kleisli and Kleisli→Monoidal are inverses
-        ( §1-fromMonad
-        ∘ §2-3.§1.toMonad
-        ) m ≡⟨⟩ -- fromMonad and toMonad are inverses
-        m ∎
        where
-        t : §1-fromMonad ∘ Kleisli→Monoidal ∘ Monoidal→Kleisli ∘ §2-3.§1.toMonad
+        -- rhs = §1-fromMonad (Kleisli→Monoidal ((Monoidal→Kleisli (§2-3.§1.toMonad m))))
-          ≡ §1-fromMonad ∘ §2-3.§1.toMonad
+        -- foo : §1-fromMonad (Kleisli→Monoidal (§2-3.§2.toMonad (§2-fromMonad (Monoidal→Kleisli (§2-3.§1.toMonad m)))))
-        -- Why does `re-ve` not satisfy this goal?
+        --     ≡ §1-fromMonad (Kleisli→Monoidal ((Monoidal→Kleisli (§2-3.§1.toMonad m))))
-        t i m = §1-fromMonad (ve-re i (§2-3.§1.toMonad m))
+        -- §2-3.§1.fmap (foo i) = §2-3.§1.fmap rhs
+        -- §2-3.§1.join (foo i) = §2-3.§1.join rhs
+        -- §2-3.§1.RisFunctor (foo i) = §2-3.§1.RisFunctor rhs
+        -- §2-3.§1.pureN (foo i) = §2-3.§1.pureN rhs
+        -- §2-3.§1.joinN (foo i) = §2-3.§1.joinN  rhs
+        -- §2-3.§1.isMonad (foo i) = §2-3.§1.isMonad rhs
+
+        lemmaz : §1-fromMonad (§2-3.§1.toMonad m) ≡ m
+        §2-3.§1.fmap (lemmaz i) = §2-3.§1.fmap m
+        §2-3.§1.join (lemmaz i) = §2-3.§1.join m
+        §2-3.§1.RisFunctor (lemmaz i) = §2-3.§1.RisFunctor m
+        §2-3.§1.pureN (lemmaz i) = §2-3.§1.pureN m
+        §2-3.§1.joinN (lemmaz i) = §2-3.§1.joinN m
+        §2-3.§1.isMonad (lemmaz i) = §2-3.§1.isMonad m
+        lemma : ∀ m → §2-3.§2.toMonad (§2-fromMonad m) ≡ m
+        K.Monad.raw (lemma m i) = K.Monad.raw m
+        K.Monad.isMonad (lemma m i) = K.Monad.isMonad m
 
       voe-isEquiv : isEquiv (§2-3.§1 omap pure) (§2-3.§2 omap pure) forth
       voe-isEquiv = gradLemma forth back forthEq backEq