diff --git a/src/Cat/Categories/Rel.agda b/src/Cat/Categories/Rel.agda
index 3aa4e59..f334c30 100644
--- a/src/Cat/Categories/Rel.agda
+++ b/src/Cat/Categories/Rel.agda
@@ -2,6 +2,7 @@
 module Cat.Categories.Rel where
 
 open import Cat.Prelude hiding (Rel)
+open import Cat.Equivalence
 
 open import Cat.Category
 
@@ -61,15 +62,9 @@ module _ {A B : Set} {S : Subset (A × B)} (ab : A × B) where
           lem0 = (λ a'' a≡a'' → ∀ a''b∈S → (forwards ∘ backwards) (a'' , a≡a'' , a''b∈S) ≡ (a'' , a≡a'' , a''b∈S))
           lem1 = (λ z₁ → cong (\ z → a , refl , z) (pathJprop (\ y _ → y) z₁))
 
-      isequiv : isEquiv
-        (Σ[ a' ∈ A ] (a , a') ∈ Diag A × (a' , b) ∈ S)
-        ((a , b) ∈ S)
-        backwards
-      isequiv y = gradLemma backwards forwards fwd-bwd bwd-fwd y
-
       equi : (Σ[ a' ∈ A ] (a , a') ∈ Diag A × (a' , b) ∈ S)
         ≃ (a , b) ∈ S
-      equi = backwards , isequiv
+      equi = fromIsomorphism _ _ (backwards , forwards , funExt bwd-fwd , funExt fwd-bwd)
 
     ident-r : (Σ[ a' ∈ A ] (a , a') ∈ Diag A × (a' , b) ∈ S)
       ≡ (a , b) ∈ S
@@ -95,15 +90,9 @@ module _ {A B : Set} {S : Subset (A × B)} (ab : A × B) where
           lem0 = (λ b'' b≡b'' → (ab''∈S : (a , b'') ∈ S) → (forwards ∘ backwards) (b'' , ab''∈S , sym b≡b'') ≡ (b'' , ab''∈S , sym b≡b''))
           lem1 = (λ ab''∈S → cong (λ φ → b , φ , refl) (pathJprop (λ y _ → y) ab''∈S))
 
-      isequiv : isEquiv
-        (Σ[ b' ∈ B ] (a , b') ∈ S × (b' , b) ∈ Diag B)
-        ((a , b) ∈ S)
-        backwards
-      isequiv ab∈S = gradLemma backwards forwards bwd-fwd fwd-bwd ab∈S
-
       equi : (Σ[ b' ∈ B ] (a , b') ∈ S × (b' , b) ∈ Diag B)
         ≃ ab ∈ S
-      equi = backwards , isequiv
+      equi = fromIsomorphism _ _ (backwards , (forwards , funExt fwd-bwd , funExt bwd-fwd))
 
     ident-l : (Σ[ b' ∈ B ] (a , b') ∈ S × (b' , b) ∈ Diag B)
       ≡ ab ∈ S
@@ -133,15 +122,9 @@ module _ {A B C D : Set} {S : Subset (A × B)} {R : Subset (B × C)} {Q : Subset
     bwd-fwd : (x : Q⊕⟨R⊕S⟩) → (bwd ∘ fwd) x ≡ x
     bwd-fwd x = refl
 
-    isequiv : isEquiv
-      (Σ[ c ∈ C ] (Σ[ b ∈ B ] (a , b) ∈ S × (b , c) ∈ R) × (c , d) ∈ Q)
-      (Σ[ b ∈ B ] (a , b) ∈ S × (Σ[ c ∈ C ] (b , c) ∈ R × (c , d) ∈ Q))
-      fwd
-    isequiv = gradLemma fwd bwd fwd-bwd bwd-fwd
-
     equi : (Σ[ c ∈ C ] (Σ[ b ∈ B ] (a , b) ∈ S × (b , c) ∈ R) × (c , d) ∈ Q)
       ≃ (Σ[ b ∈ B ] (a , b) ∈ S × (Σ[ c ∈ C ] (b , c) ∈ R × (c , d) ∈ Q))
-    equi = fwd , isequiv
+    equi = fromIsomorphism _ _ (fwd , bwd , funExt bwd-fwd , funExt fwd-bwd)
 
     -- isAssociativec : Q + (R + S) ≡ (Q + R) + S
   is-isAssociative : (Σ[ c ∈ C ] (Σ[ b ∈ B ] (a , b) ∈ S × (b , c) ∈ R) × (c , d) ∈ Q)
diff --git a/src/Cat/Category/Monad/Kleisli.agda b/src/Cat/Category/Monad/Kleisli.agda
index 463d3ab..0fd6e3d 100644
--- a/src/Cat/Category/Monad/Kleisli.agda
+++ b/src/Cat/Category/Monad/Kleisli.agda
@@ -5,6 +5,7 @@ The Kleisli formulation of monads
 open import Agda.Primitive
 
 open import Cat.Prelude
+open import Cat.Equivalence
 
 open import Cat.Category
 open import Cat.Category.Functor as F
@@ -328,13 +329,15 @@ module _ where
       module M = Monad m
 
     e : Monad' ≃ Monad
-    e = toMonad , gradLemma toMonad fromMonad
+    e = fromIsomorphism _ _ (toMonad , fromMonad , (funExt λ _ → refl) , funExt eta-refl)
+      where
       -- Monads don't have eta-equality
-      (λ x → λ
-        { i .Monad.raw → Monad.raw x
-        ; i .Monad.isMonad → Monad.isMonad x}
-      )
-      λ _ → refl
+      eta-refl : (x : Monad) → toMonad (fromMonad x) ≡ x
+      eta-refl =
+        (λ x → λ
+          { i .Monad.raw → Monad.raw x
+          ; i .Monad.isMonad  → Monad.isMonad x}
+        )
 
   grpdMonad : isGrpd Monad
   grpdMonad = equivPreservesNType
diff --git a/src/Cat/Category/Monad/Voevodsky.agda b/src/Cat/Category/Monad/Voevodsky.agda
index 8d3b75f..7bedab1 100644
--- a/src/Cat/Category/Monad/Voevodsky.agda
+++ b/src/Cat/Category/Monad/Voevodsky.agda
@@ -1,11 +1,11 @@
 {-
 This module provides construction 2.3 in [voe]
 -}
-{-# OPTIONS --cubical --caching #-}
+{-# OPTIONS --cubical --allow-unsolved-metas #-}
 module Cat.Category.Monad.Voevodsky where
 
-
 open import Cat.Prelude
+open import Cat.Equivalence
 
 open import Cat.Category
 open import Cat.Category.Functor as F
@@ -203,8 +203,8 @@ module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
         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
-
     equiv-2-3 : §2-3.§1 omap pure ≃ §2-3.§2 omap pure
-    equiv-2-3 = forth , voe-isEquiv
+    equiv-2-3 = fromIsomorphism _ _
+      ( forth , back
+      , funExt backEq , funExt forthEq
+      )