diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda
index ccf3e05..af52c8b 100644
--- a/src/Cat/Categories/Sets.agda
+++ b/src/Cat/Categories/Sets.agda
@@ -42,91 +42,16 @@ module _ (ℓ : Level) where
       IsPreCategory.isIdentity    isPreCat {A} {B} = isIdentity    {A} {B}
       IsPreCategory.arrowsAreSets isPreCat {A} {B} = arrowsAreSets {A} {B}
 
-    open IsPreCategory isPreCat hiding (_<<<_)
-
-    isIso = TypeIsomorphism
-    module _ {hA hB : hSet ℓ} where
-      open Σ hA renaming (fst to A ; snd to sA)
-      open Σ hB renaming (fst to B ; snd to sB)
-      lem1 : (f : A → B) → isSet A → isSet B → isProp (isIso f)
-      lem1 f sA sB = res
-        where
-        module _ (x y : isIso f) where
-          module x = Σ x renaming (fst to inverse ; snd to areInverses)
-          module y = Σ y renaming (fst to inverse ; snd to areInverses)
-          -- I had a lot of difficulty using the corresponding proof where
-          -- AreInverses is defined. This is sadly a bit anti-modular. The
-          -- reason for my troubles is probably related to the type of objects
-          -- being hSet's rather than sets.
-          p : ∀ {f} g → isProp (AreInverses {A = A} {B} f g)
-          p {f} g xx yy i = ve-re , re-ve
-            where
-            ve-re : g ∘ f ≡ idFun _
-            ve-re = arrowsAreSets {A = hA} {B = hA} _ _ (fst xx) (fst yy) i
-            re-ve : f ∘ g ≡ idFun _
-            re-ve = arrowsAreSets {A = hB} {B = hB} _ _ (snd xx) (snd yy) i
-          1eq : x.inverse ≡ y.inverse
-          1eq = begin
-            x.inverse                   ≡⟨⟩
-            x.inverse ∘ idFun _         ≡⟨ cong (λ φ → x.inverse ∘ φ) (sym (snd y.areInverses)) ⟩
-            x.inverse ∘ (f ∘ y.inverse) ≡⟨⟩
-            (x.inverse ∘ f) ∘ y.inverse ≡⟨ cong (λ φ → φ ∘ y.inverse) (fst x.areInverses) ⟩
-            idFun _ ∘ y.inverse         ≡⟨⟩
-            y.inverse                   ∎
-          2eq : (λ i → AreInverses f (1eq i)) [ x.areInverses ≡ y.areInverses ]
-          2eq = lemPropF p 1eq
-          res : x ≡ y
-          res i = 1eq i , 2eq i
-    module _ {ℓa ℓb : Level} {A : Set ℓa} {P : A → Set ℓb} where
-      lem2 : ((x : A) → isProp (P x)) → (p q : Σ A P)
-        → (p ≡ q) ≃ (fst p ≡ fst q)
-      lem2 pA p q = fromIsomorphism _ _ iso
-        where
-        f : ∀ {p q} → p ≡ q → fst p ≡ fst q
-        f e i = fst (e i)
-        g : ∀ {p q} → fst p ≡ fst q → p ≡ q
-        g {p} {q} = lemSig pA p q
-        ve-re : (e : p ≡ q) → (g ∘ f) e ≡ e
-        ve-re = pathJ (\ q (e : p ≡ q) → (g ∘ f) e ≡ e)
-                  (\ i j → p .fst , propSet (pA (p .fst)) (p .snd) (p .snd) (λ i → (g {p} {p} ∘ f) (λ i₁ → p) i .snd) (λ i → p .snd) i j ) q
-        re-ve : (e : fst p ≡ fst q) → (f {p} {q} ∘ g {p} {q}) e ≡ e
-        re-ve e = refl
-        inv : AreInverses (f {p} {q}) (g {p} {q})
-        inv = funExt ve-re , funExt re-ve
-        iso : (p ≡ q) ≅ (fst p ≡ fst q)
-        iso = f , g , inv
-
-    module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where
-      lem4 : isSet A → isSet B → (f : A → B)
-        → isEquiv A B f ≃ isIso f
-      lem4 sA sB f =
-        let
-          obv : isEquiv A B f → isIso f
-          obv = toIso A B
-          inv : isIso f → isEquiv A B f
-          inv = fromIso A B
-          re-ve : (x : isEquiv A B f) → (inv ∘ obv) x ≡ x
-          re-ve = inverse-from-to-iso A B
-          ve-re : (x : isIso f)       → (obv ∘ inv) x ≡ x
-          ve-re = inverse-to-from-iso A B sA sB
-          iso : isEquiv A B f ≅ isIso f
-          iso = obv , inv , funExt re-ve , funExt ve-re
-        in fromIsomorphism _ _ iso
-
+    open IsPreCategory isPreCat
     module _ {hA hB : Object} where
       open Σ hA renaming (fst to A ; snd to sA)
       open Σ hB renaming (fst to B ; snd to sB)
 
-      -- lem3 and the equivalence from lem4
-      step0 : Σ (A → B) (isEquiv A B) ≃ Σ (A → B) isIso
-      step0 = equivSig (lem4 sA sB)
-
-      -- lem2 with propIsSet
-      step2 : (hA ≡ hB) ≃ (A ≡ B)
-      step2 = lem2 (λ A → isSetIsProp) hA hB
-
       univ≃ : (hA ≡ hB) ≃ (hA ≊ hB)
-      univ≃ = step2 ⊙ univalence ⊙ step0
+      univ≃
+        = equivSigProp (λ A → isSetIsProp)
+        ⊙ univalence
+        ⊙ equivSig {P = isEquiv A B} {Q = TypeIsomorphism} (equiv≃iso sA sB)
 
     univalent : Univalent
     univalent = univalenceFrom≃ univ≃
diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 26a3b02..9394089 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -119,7 +119,7 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
     --
     -- [HoTT §9.1.4]
     idToIso : (A B : Object) → A ≡ B → A ≊ B
-    idToIso A B eq = transp (\ i → A ≊ eq i) (idIso A)
+    idToIso A B eq = subst eq (idIso A)
 
     Univalent : Set (ℓa ⊔ ℓb)
     Univalent = {A B : Object} → isEquiv (A ≡ B) (A ≊ B) (idToIso A B)
@@ -348,7 +348,7 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
           coe refl f ≡⟨ id-coe ⟩
           f ≡⟨ sym rightIdentity ⟩
           f <<< identity ≡⟨ cong (f <<<_) (sym subst-neutral) ⟩
-          f <<< _ ∎) a' p
+          f <<< _ ≡⟨ {!!} ⟩ _ ∎) a' p
 
       module _ {b' : Object} (p : b ≡ b') where
         private
@@ -431,28 +431,17 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
 
       coe-dom : {f : Arrow A X} → coe p-dom f ≡ f <<< ι~
       coe-dom {f} = begin
-        coe p-dom f
-          ≡⟨ 9-1-9 p refl f ⟩
-        fst (idToIso _ _ refl) <<< f <<< fst (snd (idToIso _ _ p))
-          ≡⟨ cong (λ φ → φ <<< f <<< fst (snd (idToIso _ _ p))) subst-neutral ⟩
-        identity <<< f <<< fst (snd (idToIso _ _ p))
-          ≡⟨ cong (λ φ → identity <<< f <<< φ) (cong (λ x → (fst (snd x))) lem) ⟩
-        identity <<< f <<< ι~
-          ≡⟨ cong (_<<< ι~) leftIdentity ⟩
+        coe p-dom f ≡⟨ 9-1-9-left f p ⟩
+        f <<< fst (snd (idToIso _ _ (isoToId iso))) ≡⟨⟩
+        f <<< fst (snd (idToIso _ _ p)) ≡⟨ cong (f <<<_) (cong (fst ∘ snd) lem) ⟩
         f <<< ι~ ∎
 
       coe-cod : {f : Arrow X A} → coe p-cod f ≡ ι <<< f
       coe-cod {f} = begin
         coe p-cod f
-          ≡⟨ 9-1-9 refl p f ⟩
-        fst (idToIso _ _ p) <<< f <<< fst (snd (idToIso _ _ refl))
-          ≡⟨ cong (λ φ → fst (idToIso _ _ p) <<< f <<< φ) subst-neutral ⟩
-        fst (idToIso _ _ p) <<< f <<< identity
-          ≡⟨ cong (λ φ → φ <<< f <<< identity) (cong fst lem) ⟩
-        ι <<< f <<< identity
-          ≡⟨ sym isAssociative ⟩
-        ι <<< (f <<< identity)
-          ≡⟨ cong (ι <<<_) rightIdentity ⟩
+          ≡⟨ 9-1-9-right f p ⟩
+        fst (idToIso _ _ p) <<< f
+          ≡⟨ cong (λ φ → φ <<< f) (cong fst lem) ⟩
         ι <<< f ∎
 
       module _ {f : Arrow A X} {g : Arrow B X} (q : PathP (λ i → p-dom i) f g) where
diff --git a/src/Cat/Category/Product.agda b/src/Cat/Category/Product.agda
index be77ec8..757c5cc 100644
--- a/src/Cat/Category/Product.agda
+++ b/src/Cat/Category/Product.agda
@@ -7,7 +7,6 @@ open import Cat.Equivalence
 open import Cat.Category
 
 module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
-
   open Category ℂ
 
   module _ (A B : Object) where
@@ -18,8 +17,6 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
         fst  : ℂ [ object , A ]
         snd  : ℂ [ object , B ]
 
-    -- FIXME Not sure this is actually a proposition - so this name is
-    -- misleading.
     record IsProduct (raw : RawProduct) : Set (ℓa ⊔ ℓb) where
       open RawProduct raw public
       field
diff --git a/src/Cat/Equivalence.agda b/src/Cat/Equivalence.agda
index a6a8582..6c96f1b 100644
--- a/src/Cat/Equivalence.agda
+++ b/src/Cat/Equivalence.agda
@@ -7,7 +7,10 @@ open import Cubical.PathPrelude hiding (inverse)
 open import Cubical.PathPrelude using (isEquiv ; isContr ; fiber) public
 open import Cubical.GradLemma hiding (isoToPath)
 
-open import Cat.Prelude using (lemPropF ; setPi ; lemSig ; propSet ; Preorder ; equalityIsEquivalence ; propSig ; id-coe)
+open import Cat.Prelude using
+  ( lemPropF ; setPi ; lemSig ; propSet
+  ; Preorder ; equalityIsEquivalence ; propSig ; id-coe
+  ; Setoid )
 
 import Cubical.Univalence as U
 
@@ -327,6 +330,48 @@ preorder≅ ℓ = record
         k = pathJ D (trans id-coe id-coe) B (sym p)
       in k
 
+setoid≅ : (ℓ : Level) → Setoid _ _
+setoid≅ ℓ = record
+  { Carrier = Set ℓ
+  ; _≈_ = _≅_
+  ; isEquivalence = record
+    { refl = idFun _ , idFun _ , (funExt λ _ → refl) , (funExt λ _ → refl)
+    ; sym = symmetryIso
+    ; trans = composeIso
+    }
+  }
+
+setoid≃ : (ℓ : Level) → Setoid _ _
+setoid≃ ℓ = record
+  { Carrier = Set ℓ
+  ; _≈_ = _≃_
+  ; isEquivalence = record
+    { refl = idEquiv
+    ; sym = Equivalence.symmetry
+    ; trans = λ x x₁ → Equivalence.compose x x₁
+    }
+  }
+
+-- If the second component of a pair is propositional, then equality of such
+-- pairs is equivalent to equality of their first components.
+module _ {ℓa ℓb : Level} {A : Set ℓa} {P : A → Set ℓb} where
+  equivSigProp : ((x : A) → isProp (P x)) → {p q : Σ A P}
+    → (p ≡ q) ≃ (fst p ≡ fst q)
+  equivSigProp pA {p} {q} = fromIsomorphism _ _ iso
+    where
+    f : ∀ {p q} → p ≡ q → fst p ≡ fst q
+    f = cong fst
+    g : ∀ {p q} → fst p ≡ fst q → p ≡ q
+    g = lemSig pA _ _
+    ve-re : (e : p ≡ q) → (g ∘ f) e ≡ e
+    ve-re = pathJ (\ q (e : p ≡ q) → (g ∘ f) e ≡ e)
+              (\ i j → p .fst , propSet (pA (p .fst)) (p .snd) (p .snd) (λ i → (g {p} {p} ∘ f) (λ i₁ → p) i .snd) (λ i → p .snd) i j ) q
+    re-ve : (e : fst p ≡ fst q) → (f {p} {q} ∘ g {p} {q}) e ≡ e
+    re-ve e = refl
+    inv : AreInverses (f {p} {q}) (g {p} {q})
+    inv = funExt ve-re , funExt re-ve
+    iso : (p ≡ q) ≅ (fst p ≡ fst q)
+    iso = f , g , inv
 
 module _ {ℓ : Level} {A B : Set ℓ} where
   isoToPath : (A ≅ B) → (A ≡ B)
@@ -347,6 +392,24 @@ module _ {ℓ : Level} {A B : Set ℓ} where
     aux : (A U.≃ B) ≃ (A ≃ B)
     aux = fromIsomorphism _ _ (doEta , deEta , funExt (λ{ (U.con _ _) → refl}) , refl)
 
+  -- Equivalence is equivalent to isomorphism when the equivalence (resp.
+  -- isomorphism) acts on sets.
+  module _ (sA : isSet A) (sB : isSet B) where
+    equiv≃iso : (f : A → B) → isEquiv A B f ≃ Isomorphism f
+    equiv≃iso f =
+      let
+        obv : isEquiv A B f → Isomorphism f
+        obv = toIso A B
+        inv : Isomorphism f → isEquiv A B f
+        inv = fromIso A B
+        re-ve : (x : isEquiv A B f) → (inv ∘ obv) x ≡ x
+        re-ve = inverse-from-to-iso A B
+        ve-re : (x : Isomorphism f) → (obv ∘ inv) x ≡ x
+        ve-re = inverse-to-from-iso A B sA sB
+        iso : isEquiv A B f ≅ Isomorphism f
+        iso = obv , inv , funExt re-ve , funExt ve-re
+      in fromIsomorphism _ _ iso
+
 -- A few results that I have not generalized to work with both the eta and no-eta variable of ≃
 module _ {ℓa ℓb : Level} {A : Set ℓa} {P : A → Set ℓb} where
   -- Equality on sigma's whose second component is a proposition is equivalent
@@ -438,6 +501,8 @@ module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where
     in fromIsomorphism _ _ iso
 
 module _ {ℓa ℓb : Level} {A : Set ℓa} {P : A → Set ℓb} where
+  -- Equivalence of pairs whose first components are identitical can be obtained
+  -- from an equivalence of their seecond components.
   equivSig : {ℓc : Level} {Q : A → Set ℓc}
     → ((a : A) → P a ≃ Q a) → Σ A P ≃ Σ A Q
   equivSig {Q = Q} eA = res
diff --git a/src/Cat/Prelude.agda b/src/Cat/Prelude.agda
index bedad50..0c0bec0 100644
--- a/src/Cat/Prelude.agda
+++ b/src/Cat/Prelude.agda
@@ -76,7 +76,9 @@ module _ {ℓa ℓb : Level} {A : Set ℓa} {B : A → Set ℓb} {a b : Σ A B}
   snd (Σ≡ i) = snd≡ i
 
 import Relation.Binary
-open Relation.Binary public using (Preorder ; Transitive ; IsEquivalence ; Rel)
+open Relation.Binary public using
+  ( Preorder ; Transitive ; IsEquivalence ; Rel
+  ; Setoid )
 
 equalityIsEquivalence : {ℓ : Level} {A : Set ℓ} → IsEquivalence {A = A} _≡_
 IsEquivalence.refl  equalityIsEquivalence = refl