diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda
index bcfb508..80b69e0 100644
--- a/src/Cat/Categories/Fun.agda
+++ b/src/Cat/Categories/Fun.agda
@@ -1,6 +1,7 @@
 {-# OPTIONS --allow-unsolved-metas --cubical --caching #-}
 module Cat.Categories.Fun where
 
+
 open import Cat.Prelude
 open import Cat.Equivalence
 open import Cat.Category
@@ -52,14 +53,14 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C
           lem : coe (pp {C}) 𝔻.identity ≡ f→g
           lem = trans (𝔻.9-1-9-right {b = Functor.omap F C} 𝔻.identity p*) 𝔻.rightIdentity
 
-      idToNatTrans : NaturalTransformation F G
-      idToNatTrans = (λ C → coe pp 𝔻.identity) , λ f → begin
-        coe pp 𝔻.identity 𝔻.<<< F.fmap f ≡⟨ cong (𝔻._<<< F.fmap f) lem ⟩
-        -- Just need to show that f→g is a natural transformation
-        -- I know that it has an inverse; g→f
-        f→g 𝔻.<<< F.fmap f ≡⟨ {!lem!} ⟩
-        G.fmap f 𝔻.<<< f→g ≡⟨ cong (G.fmap f 𝔻.<<<_) (sym lem) ⟩
-        G.fmap f 𝔻.<<< coe pp 𝔻.identity ∎
+      -- idToNatTrans : NaturalTransformation F G
+      -- idToNatTrans = (λ C → coe pp 𝔻.identity) , λ f → begin
+      --   coe pp 𝔻.identity 𝔻.<<< F.fmap f ≡⟨ cong (𝔻._<<< F.fmap f) lem ⟩
+      --   -- Just need to show that f→g is a natural transformation
+      --   -- I know that it has an inverse; g→f
+      --   f→g 𝔻.<<< F.fmap f ≡⟨ {!lem!} ⟩
+      --   G.fmap f 𝔻.<<< f→g ≡⟨ cong (G.fmap f 𝔻.<<<_) (sym lem) ⟩
+      --   G.fmap f 𝔻.<<< coe pp 𝔻.identity ∎
 
     module _ {A B : Functor ℂ 𝔻} where
       module A = Functor A
@@ -92,70 +93,70 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C
         U : (F : ℂ.Object → 𝔻.Object) → Set _
         U F = {A B : ℂ.Object} → ℂ [ A , B ] → 𝔻 [ F A , F B ]
 
-        module _
-          (omap : ℂ.Object → 𝔻.Object)
-          (p    : A.omap ≡ omap)
-          where
-          D : Set _
-          D = ( fmap : U omap)
-            → ( let
-                 raw-B : RawFunctor ℂ 𝔻
-                 raw-B = record { omap = omap ; fmap = fmap }
-              )
-            → (isF-B' : IsFunctor ℂ 𝔻 raw-B)
-            → ( let
-                B' : Functor ℂ 𝔻
-                B' = record { raw = raw-B ; isFunctor = isF-B' }
-              )
-            → (iso' : A ≊ B') → PathP (λ i → U (p i)) A.fmap fmap
-          -- D : Set _
-          -- D = PathP (λ i → U (p i)) A.fmap fmap
-          -- eeq : (λ f → A.fmap f) ≡ fmap
-          -- eeq = funExtImp (λ A → funExtImp (λ B → funExt (λ f → isofmap {A} {B} f)))
-          --   where
-          --   module _ {X : ℂ.Object} {Y : ℂ.Object} (f : ℂ [ X , Y ]) where
-          --     isofmap : A.fmap f ≡ fmap f
-          --     isofmap = {!ap!}
-        d : D A.omap refl
-        d = res
-          where
-          module _
-            ( fmap : U A.omap )
-            ( let
-              raw-B : RawFunctor ℂ 𝔻
-              raw-B = record { omap = A.omap ; fmap = fmap }
-            )
-            ( isF-B' : IsFunctor ℂ 𝔻 raw-B )
-            ( let
-              B' : Functor ℂ 𝔻
-              B' = record { raw = raw-B ; isFunctor = isF-B' }
-            )
-            ( iso' : A ≊ B' )
-            where
-            module _ {X Y : ℂ.Object} (f : ℂ [ X , Y ]) where
-              step : {!!} 𝔻.≊ {!!}
-              step = {!!}
-              resres : A.fmap {X} {Y} f ≡ fmap {X} {Y} f
-              resres = {!!}
-            res : PathP (λ i → U A.omap) A.fmap fmap
-            res i {X} {Y} f = resres f i
+      --   module _
+      --     (omap : ℂ.Object → 𝔻.Object)
+      --     (p    : A.omap ≡ omap)
+      --     where
+      --     D : Set _
+      --     D = ( fmap : U omap)
+      --       → ( let
+      --            raw-B : RawFunctor ℂ 𝔻
+      --            raw-B = record { omap = omap ; fmap = fmap }
+      --         )
+      --       → (isF-B' : IsFunctor ℂ 𝔻 raw-B)
+      --       → ( let
+      --           B' : Functor ℂ 𝔻
+      --           B' = record { raw = raw-B ; isFunctor = isF-B' }
+      --         )
+      --       → (iso' : A ≊ B') → PathP (λ i → U (p i)) A.fmap fmap
+      --     -- D : Set _
+      --     -- D = PathP (λ i → U (p i)) A.fmap fmap
+      --     -- eeq : (λ f → A.fmap f) ≡ fmap
+      --     -- eeq = funExtImp (λ A → funExtImp (λ B → funExt (λ f → isofmap {A} {B} f)))
+      --     --   where
+      --     --   module _ {X : ℂ.Object} {Y : ℂ.Object} (f : ℂ [ X , Y ]) where
+      --     --     isofmap : A.fmap f ≡ fmap f
+      --     --     isofmap = {!ap!}
+      --   d : D A.omap refl
+      --   d = res
+      --     where
+      --     module _
+      --       ( fmap : U A.omap )
+      --       ( let
+      --         raw-B : RawFunctor ℂ 𝔻
+      --         raw-B = record { omap = A.omap ; fmap = fmap }
+      --       )
+      --       ( isF-B' : IsFunctor ℂ 𝔻 raw-B )
+      --       ( let
+      --         B' : Functor ℂ 𝔻
+      --         B' = record { raw = raw-B ; isFunctor = isF-B' }
+      --       )
+      --       ( iso' : A ≊ B' )
+      --       where
+      --       module _ {X Y : ℂ.Object} (f : ℂ [ X , Y ]) where
+      --         step : {!!} 𝔻.≊ {!!}
+      --         step = {!!}
+      --         resres : A.fmap {X} {Y} f ≡ fmap {X} {Y} f
+      --         resres = {!!}
+      --       res : PathP (λ i → U A.omap) A.fmap fmap
+      --       res i {X} {Y} f = resres f i
 
-        fmapEq : PathP (λ i → U (omapEq i)) A.fmap B.fmap
-        fmapEq = pathJ D d B.omap omapEq B.fmap B.isFunctor iso
+      --   fmapEq : PathP (λ i → U (omapEq i)) A.fmap B.fmap
+      --   fmapEq = pathJ D d B.omap omapEq B.fmap B.isFunctor iso
 
-        rawEq : A.raw ≡ B.raw
-        rawEq i = record { omap = omapEq i ; fmap = fmapEq i }
+      --   rawEq : A.raw ≡ B.raw
+      --   rawEq i = record { omap = omapEq i ; fmap = fmapEq i }
 
-      private
-        f : (A ≡ B) → (A ≊ B)
-        f p = idToNatTrans p , idToNatTrans (sym p) , NaturalTransformation≡ A A (funExt (λ C → {!!})) , {!!}
-        g : (A ≊ B) → (A ≡ B)
-        g = Functor≡ ∘ rawEq
-        inv : AreInverses f g
-        inv = {!funExt λ p → ?!} , {!!}
-
-      iso : (A ≡ B) ≅ (A ≊ B)
-      iso = f , g , inv
+      -- private
+      --   f : (A ≡ B) → (A ≊ B)
+      --   f p = idToNatTrans p , idToNatTrans (sym p) , NaturalTransformation≡ A A (funExt (λ C → {!!})) , {!!}
+      --   g : (A ≊ B) → (A ≡ B)
+      --   g = Functor≡ ∘ rawEq
+      --   inv : AreInverses f g
+      --   inv = {!funExt λ p → ?!} , {!!}
+      postulate
+        iso : (A ≡ B) ≅ (A ≊ B)
+--      iso = f , g , inv
 
       univ : (A ≡ B) ≃ (A ≊ B)
       univ = fromIsomorphism _ _ iso
diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 139fba9..c6e624a 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -44,7 +44,7 @@ open Cat.Equivalence
 -- about these. The laws defined are the types the propositions - not the
 -- witnesses to them!
 record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
-  no-eta-equality
+--  no-eta-equality
   field
     Object   : Set ℓa
     Arrow    : Object → Object → Set ℓb
diff --git a/src/Cat/Category/Monad/Kleisli.agda b/src/Cat/Category/Monad/Kleisli.agda
index e0ebf86..366886b 100644
--- a/src/Cat/Category/Monad/Kleisli.agda
+++ b/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
diff --git a/src/Cat/Category/Monad/Monoidal.agda b/src/Cat/Category/Monad/Monoidal.agda
index c8ce5f2..9ae9f59 100644
--- a/src/Cat/Category/Monad/Monoidal.agda
+++ b/src/Cat/Category/Monad/Monoidal.agda
@@ -122,6 +122,7 @@ record IsMonad (raw : RawMonad) : Set ℓ where
       R.fmap a <<< R.fmap b <<< R.fmap c  ∎
 
 record Monad : Set ℓ where
+  no-eta-equality
   field
     raw     : RawMonad
     isMonad : IsMonad raw
diff --git a/src/Cat/Category/Monad/Voevodsky.agda b/src/Cat/Category/Monad/Voevodsky.agda
index efdd6de..8d3b75f 100644
--- a/src/Cat/Category/Monad/Voevodsky.agda
+++ b/src/Cat/Category/Monad/Voevodsky.agda
@@ -4,6 +4,7 @@ This module provides construction 2.3 in [voe]
 {-# OPTIONS --cubical --caching #-}
 module Cat.Category.Monad.Voevodsky where
 
+
 open import Cat.Prelude
 
 open import Cat.Category
@@ -26,6 +27,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
@@ -76,12 +78,11 @@ module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
         isMonad : IsMonad rawMnd
 
       toMonad : Monad
-      toMonad = record
-        { raw     = rawMnd
-        ; isMonad = isMonad
-        }
+      toMonad .Monad.raw = rawMnd
+      toMonad .Monad.isMonad = isMonad
 
     record §2 : Set ℓ where
+      no-eta-equality
       open K
 
       field
@@ -98,28 +99,24 @@ module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
         isMonad : IsMonad rawMnd
 
       toMonad : Monad
-      toMonad = record
-        { raw     = rawMnd
-        ; isMonad = isMonad
-        }
+      toMonad .Monad.raw     = rawMnd
+      toMonad .Monad.isMonad = isMonad
 
-  §1-fromMonad : (m : M.Monad) → §2-3.§1 (M.Monad.Romap m) (λ {X} → M.Monad.pureT m X)
-  §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
+  module _ (m : M.Monad) 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
-    { bind    = K.Monad.bind    m
-    ; isMonad = K.Monad.isMonad m
-    }
+  §2-fromMonad m .§2-3.§2.bind    = K.Monad.bind    m
+  §2-fromMonad m  .§2-3.§2.isMonad = K.Monad.isMonad m
 
   -- | In the following we seek to transform the equivalence `Monoidal≃Kleisli`
   -- | to talk about voevodsky's construction.
@@ -147,64 +144,64 @@ module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
 
       forthEq : ∀ m → (forth ∘ back) m ≡ m
       forthEq m = begin
-        (forth ∘ back) m ≡⟨⟩
-        -- In full gory detail:
-        ( §2-fromMonad
-        ∘ 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 ∎
+       §2-fromMonad
+         (Monoidal→Kleisli
+          (§2-3.§1.toMonad
+           (§1-fromMonad (Kleisli→Monoidal (§2-3.§2.toMonad m)))))
+         ≡⟨ cong-d (§2-fromMonad ∘ Monoidal→Kleisli) (lemmaz (Kleisli→Monoidal (§2-3.§2.toMonad m))) ⟩
+       §2-fromMonad
+         ((Monoidal→Kleisli ∘ Kleisli→Monoidal)
+          (§2-3.§2.toMonad m))
+         ≡⟨ (cong-d (\ φ → §2-fromMonad (φ (§2-3.§2.toMonad m))) re-ve) ⟩
+       (§2-fromMonad ∘ §2-3.§2.toMonad) m
+         ≡⟨ lemma ⟩
+       m ∎
         where
-        t' : ((Monoidal→Kleisli ∘ Kleisli→Monoidal) ∘ §2-3.§2.toMonad {omap} {pure})
-          ≡ §2-3.§2.toMonad
-        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 (\ φ → φ m) t
+        lemma : (§2-fromMonad ∘ §2-3.§2.toMonad) m ≡ m
+        §2-3.§2.bind (lemma i) = §2-3.§2.bind m
+        §2-3.§2.isMonad (lemma i) = §2-3.§2.isMonad m
+        lemmaz : ∀ m → §2-3.§1.toMonad (§1-fromMonad m) ≡ m
+        M.Monad.raw (lemmaz m i) = M.Monad.raw m
+        M.Monad.isMonad (lemmaz m i) = M.Monad.isMonad m
 
       backEq : ∀ m → (back ∘ forth) m ≡ m
       backEq m = begin
-        (back ∘ forth) m ≡⟨⟩
-        ( §1-fromMonad
-        ∘ 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
+        §1-fromMonad
+        (Kleisli→Monoidal
+        (§2-3.§2.toMonad
+        (§2-fromMonad (Monoidal→Kleisli (§2-3.§1.toMonad m)))))
+          ≡⟨ cong-d (§1-fromMonad ∘ Kleisli→Monoidal) (lemma (Monoidal→Kleisli (§2-3.§1.toMonad m))) ⟩
+        §1-fromMonad
+        ((Kleisli→Monoidal ∘ Monoidal→Kleisli)
+        (§2-3.§1.toMonad m))
+          ≡⟨ (cong-d (\ φ → §1-fromMonad (φ (§2-3.§1.toMonad m))) ve-re) ⟩
+        §1-fromMonad (§2-3.§1.toMonad m)
+          ≡⟨ lemmaz ⟩
         m ∎
-        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 i m = §1-fromMonad (ve-re i (§2-3.§1.toMonad m))
+       where
+        -- having eta equality on causes roughly the same work as checking this proof of foo,
+        -- which is quite expensive because it ends up reducing complex terms.
+
+        -- rhs = §1-fromMonad (Kleisli→Monoidal ((Monoidal→Kleisli (§2-3.§1.toMonad m))))
+        -- foo : §1-fromMonad (Kleisli→Monoidal (§2-3.§2.toMonad (§2-fromMonad (Monoidal→Kleisli (§2-3.§1.toMonad m)))))
+        --     ≡ §1-fromMonad (Kleisli→Monoidal ((Monoidal→Kleisli (§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
diff --git a/src/Cat/Category/Product.agda b/src/Cat/Category/Product.agda
index 41d10e2..418ec22 100644
--- a/src/Cat/Category/Product.agda
+++ b/src/Cat/Category/Product.agda
@@ -1,6 +1,7 @@
 {-# OPTIONS --cubical --caching #-}
 module Cat.Category.Product where
 
+
 open import Cat.Prelude as P hiding (_×_ ; fst ; snd)
 open import Cat.Equivalence
 
@@ -11,7 +12,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
 
   module _ (A B : Object) where
     record RawProduct : Set (ℓa ⊔ ℓb) where
-      no-eta-equality
+    --  no-eta-equality
       field
         object : Object
         fst  : ℂ [ object , A ]