diff --git a/src/Cat/Categories/Free.agda b/src/Cat/Categories/Free.agda
index 58b777d..8fe148a 100644
--- a/src/Cat/Categories/Free.agda
+++ b/src/Cat/Categories/Free.agda
@@ -67,7 +67,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
     IsPreCategory.arrowsAreSets isPreCategory = arrowsAreSets
 
     module _ {A B : ℂ.Object} where
-      eqv : isEquiv (A ≡ B) (A ≅ B) (Univalence.idToIso isIdentity A B)
+      eqv : isEquiv (A ≡ B) (A ≊ B) (Univalence.idToIso isIdentity A B)
       eqv = {!!}
 
     univalent : Univalent
diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda
index 07e2263..eb861e7 100644
--- a/src/Cat/Categories/Fun.agda
+++ b/src/Cat/Categories/Fun.agda
@@ -2,6 +2,7 @@
 module Cat.Categories.Fun where
 
 open import Cat.Prelude
+open import Cat.Equivalence
 
 open import Cat.Category
 open import Cat.Category.Functor
@@ -33,13 +34,140 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C
 
     open IsPreCategory isPreCategory hiding (identity)
 
+    module _ {F G : Functor ℂ 𝔻} (p : F ≡ G) where
+      private
+        module F = Functor F
+        module G = Functor G
+        p-omap : F.omap ≡ G.omap
+        p-omap = cong Functor.omap p
+        pp : {C : ℂ.Object} → 𝔻 [ Functor.omap F C , Functor.omap F C ] ≡ 𝔻 [ Functor.omap F C , Functor.omap G C ]
+        pp {C} = cong (λ f → 𝔻 [ Functor.omap F C , f C ]) p-omap
+        module _ {C : ℂ.Object} where
+          p* : F.omap C ≡ G.omap C
+          p* = cong (_$ C) p-omap
+          iso : F.omap C 𝔻.≊ G.omap C
+          iso = 𝔻.idToIso _ _ p*
+          open Σ iso renaming (fst to f→g) public
+          open Σ (snd iso) renaming (fst to g→f ; snd to inv) public
+          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 ∎
+
+    module _ {A B : Functor ℂ 𝔻} where
+      module A = Functor A
+      module B = Functor B
+      module _ (iso : A ≊ B) where
+        omapEq : A.omap ≡ B.omap
+        omapEq = funExt eq
+          where
+          module _ (C : ℂ.Object) where
+            f : 𝔻.Arrow (A.omap C) (B.omap C)
+            f = fst (fst iso) C
+            g : 𝔻.Arrow (B.omap C) (A.omap C)
+            g = fst (fst (snd iso)) C
+            inv : 𝔻.IsInverseOf f g
+            inv
+              = ( begin
+               g 𝔻.<<< f ≡⟨ cong (λ x → fst x $ C) (fst (snd (snd iso))) ⟩
+                𝔻.identity ∎
+                )
+              , ( begin
+                f 𝔻.<<< g ≡⟨ cong (λ x → fst x $ C) (snd (snd (snd iso))) ⟩
+                𝔻.identity ∎
+                )
+            isoC : A.omap C 𝔻.≊ B.omap C
+            isoC = f , g , inv
+            eq : A.omap C ≡ B.omap C
+            eq = 𝔻.isoToId isoC
+
+
+        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
+
+        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 }
+
+      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
+
+      univ : (A ≡ B) ≃ (A ≊ B)
+      univ = fromIsomorphism _ _ iso
+
     -- There used to be some work-in-progress on this theorem, please go back to
     -- this point in time to see it:
     --
     -- commit 6b7d66b7fc936fe3674b2fd9fa790bd0e3fec12f
     -- Author: Frederik Hanghøj Iversen <fhi.1990@gmail.com>
     -- Date:   Fri Apr 13 15:26:46 2018 +0200
-    postulate univalent : Univalent
+    univalent : Univalent
+    univalent = univalenceFrom≃ univ
 
     isCategory : IsCategory raw
     IsCategory.isPreCategory isCategory = isPreCategory
diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda
index 31d6926..ccf3e05 100644
--- a/src/Cat/Categories/Sets.agda
+++ b/src/Cat/Categories/Sets.agda
@@ -8,7 +8,7 @@ open import Cat.Category
 open import Cat.Category.Functor
 open import Cat.Category.Product
 open import Cat.Wishlist
-open import Cat.Equivalence renaming (_≅_ to _≈_)
+open import Cat.Equivalence
 
 _⊙_ : {ℓa ℓb ℓc : Level} {A : Set ℓa} {B : Set ℓb} {C : Set ℓc} → (A ≃ B) → (B ≃ C) → A ≃ C
 eqA ⊙ eqB = Equivalence.compose eqA eqB
@@ -93,7 +93,7 @@ module _ (ℓ : Level) where
         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 : (p ≡ q) ≅ (fst p ≡ fst q)
         iso = f , g , inv
 
     module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where
@@ -109,7 +109,7 @@ module _ (ℓ : Level) where
           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 : isEquiv A B f ≅ isIso f
           iso = obv , inv , funExt re-ve , funExt ve-re
         in fromIsomorphism _ _ iso
 
@@ -125,7 +125,7 @@ module _ (ℓ : Level) where
       step2 : (hA ≡ hB) ≃ (A ≡ B)
       step2 = lem2 (λ A → isSetIsProp) hA hB
 
-      univ≃ : (hA ≡ hB) ≃ (hA ≅ hB)
+      univ≃ : (hA ≡ hB) ≃ (hA ≊ hB)
       univ≃ = step2 ⊙ univalence ⊙ step0
 
     univalent : Univalent
diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 3cc5068..26a3b02 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -32,7 +32,6 @@ open import Cat.Prelude
 import Cat.Equivalence
 open Cat.Equivalence public using () renaming (Isomorphism to TypeIsomorphism)
 open Cat.Equivalence
-  renaming (_≅_ to _≈_)
   hiding (preorder≅ ; Isomorphism)
 
 ------------------
@@ -52,6 +51,8 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
     identity : {A : Object} → Arrow A A
     _<<<_    : {A B C : Object} → Arrow B C → Arrow A B → Arrow A C
 
+  -- infixr 8 _<<<_
+  -- infixl 8 _>>>_
   infixl 10 _<<<_ _>>>_
 
   -- | Operations on data
@@ -86,8 +87,8 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
   Isomorphism : ∀ {A B} → (f : Arrow A B) → Set ℓb
   Isomorphism {A} {B} f = Σ[ g ∈ Arrow B A ] IsInverseOf f g
 
-  _≅_ : (A B : Object) → Set ℓb
-  _≅_ A B = Σ[ f ∈ Arrow A B ] (Isomorphism f)
+  _≊_ : (A B : Object) → Set ℓb
+  _≊_ A B = Σ[ f ∈ Arrow A B ] (Isomorphism f)
 
   module _ {A B : Object} where
     Epimorphism : {X : Object } → (f : Arrow A B) → Set ℓb
@@ -111,29 +112,30 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
   -- | Univalence is indexed by a raw category as well as an identity proof.
   module Univalence (isIdentity : IsIdentity identity) where
     -- | The identity isomorphism
-    idIso : (A : Object) → A ≅ A
+    idIso : (A : Object) → A ≊ A
     idIso A = identity , identity , isIdentity
 
     -- | Extract an isomorphism from an equality
     --
     -- [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 : Object) → A ≡ B → A ≊ B
+    idToIso A B eq = transp (\ i → A ≊ eq i) (idIso A)
 
     Univalent : Set (ℓa ⊔ ℓb)
-    Univalent = {A B : Object} → isEquiv (A ≡ B) (A ≅ B) (idToIso A B)
+    Univalent = {A B : Object} → isEquiv (A ≡ B) (A ≊ B) (idToIso A B)
 
     univalenceFromIsomorphism : {A B : Object}
-      → TypeIsomorphism (idToIso A B) → isEquiv (A ≡ B) (A ≅ B) (idToIso A B)
+      → TypeIsomorphism (idToIso A B) → isEquiv (A ≡ B) (A ≊ B) (idToIso A B)
     univalenceFromIsomorphism = fromIso _ _
 
     -- A perhaps more readable version of univalence:
-    Univalent≃ = {A B : Object} → (A ≡ B) ≃ (A ≅ B)
+    Univalent≃ = {A B : Object} → (A ≡ B) ≃ (A ≊ B)
+    Univalent≅ = {A B : Object} → (A ≡ B) ≅ (A ≊ B)
 
     private
       -- | Equivalent formulation of univalence.
       Univalent[Contr] : Set _
-      Univalent[Contr] = ∀ A → isContr (Σ[ X ∈ Object ] A ≅ X)
+      Univalent[Contr] = ∀ A → isContr (Σ[ X ∈ Object ] A ≊ X)
 
       -- From: Thierry Coquand <Thierry.Coquand@cse.gu.se>
       -- Date: Wed, Mar 21, 2018 at 3:12 PM
@@ -145,15 +147,18 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
     univalenceFrom≃ = from[Contr] ∘ step
       where
       module _ (f : Univalent≃) (A : Object) where
-        lem : Σ Object (A ≡_) ≃ Σ Object (A ≅_)
+        lem : Σ Object (A ≡_) ≃ Σ Object (A ≊_)
         lem = equivSig λ _ → f
 
         aux : isContr (Σ Object (A ≡_))
         aux = (A , refl) , (λ y → contrSingl (snd y))
 
-        step : isContr (Σ Object (A ≅_))
+        step : isContr (Σ Object (A ≊_))
         step = equivPreservesNType {n = ⟨-2⟩} lem aux
 
+    univalenceFrom≅ : Univalent≅ → Univalent
+    univalenceFrom≅ x = univalenceFrom≃ $ fromIsomorphism _ _ x
+
     propUnivalent : isProp Univalent
     propUnivalent a b i = propPi (λ iso → propIsContr) a b i
 
@@ -263,8 +268,8 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
 
     module _ where
       private
-        trans≅ : Transitive _≅_
-        trans≅ (f , f~ , f-inv) (g , g~ , g-inv)
+        trans≊ : Transitive _≊_
+        trans≊ (f , f~ , f-inv) (g , g~ , g-inv)
           = g <<< f
           , f~ <<< g~
           , ( begin
@@ -283,11 +288,11 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
               g <<< g~                ≡⟨ snd g-inv ⟩
               identity                ∎
             )
-        isPreorder : IsPreorder _≅_
-        isPreorder = record { isEquivalence = equalityIsEquivalence ; reflexive = idToIso _ _ ; trans = trans≅ }
+        isPreorder : IsPreorder _≊_
+        isPreorder = record { isEquivalence = equalityIsEquivalence ; reflexive = idToIso _ _ ; trans = trans≊ }
 
-      preorder≅ : Preorder _ _ _
-      preorder≅ = record { Carrier = Object ; _≈_ = _≡_ ; _∼_ = _≅_ ; isPreorder = isPreorder }
+      preorder≊ : Preorder _ _ _
+      preorder≊ = record { Carrier = Object ; _≈_ = _≡_ ; _∼_ = _≊_ ; isPreorder = isPreorder }
 
   record PreCategory : Set (lsuc (ℓa ⊔ ℓb)) where
     field
@@ -319,7 +324,7 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
         iso : TypeIsomorphism (idToIso A B)
         iso = toIso _ _ univalent
 
-      isoToId : (A ≅ B) → (A ≡ B)
+      isoToId : (A ≊ B) → (A ≡ B)
       isoToId = fst iso
 
       asTypeIso : TypeIsomorphism (idToIso A B)
@@ -329,14 +334,47 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
       inverse-from-to-iso' : AreInverses (idToIso A B) isoToId
       inverse-from-to-iso' = snd iso
 
-      -- lemma 9.1.9 in hott
+    module _ {a b : Object} (f : Arrow a b) where
+      module _ {a' : Object} (p : a ≡ a') where
+        private
+          p~ : Arrow a' a
+          p~ = fst (snd (idToIso _ _ p))
+
+          D : ∀ a'' → a ≡ a'' → Set _
+          D a'' p' = coe (cong (λ x → Arrow x b) p') f ≡ f <<< (fst (snd (idToIso _ _ p')))
+
+        9-1-9-left  : coe (cong (λ x → Arrow x b) p) f ≡ f <<< p~
+        9-1-9-left  = pathJ D (begin
+          coe refl f ≡⟨ id-coe ⟩
+          f ≡⟨ sym rightIdentity ⟩
+          f <<< identity ≡⟨ cong (f <<<_) (sym subst-neutral) ⟩
+          f <<< _ ∎) a' p
+
+      module _ {b' : Object} (p : b ≡ b') where
+        private
+          p* : Arrow b  b'
+          p* = fst (idToIso _ _ p)
+
+          D : ∀ b'' → b ≡ b'' → Set _
+          D b'' p' = coe (cong (λ x → Arrow a x) p') f ≡ fst (idToIso _ _ p') <<< f
+
+        9-1-9-right : coe (cong (λ x → Arrow a x) p) f ≡ p* <<< f
+        9-1-9-right = pathJ D (begin
+          coe refl f ≡⟨ id-coe ⟩
+          f ≡⟨ sym leftIdentity ⟩
+          identity <<< f ≡⟨ cong (_<<< f) (sym subst-neutral) ⟩
+          _ <<< f ∎) b' p
+
+    -- lemma 9.1.9 in hott
     module _ {a a' b b' : Object}
       (p : a ≡ a') (q : b ≡ b') (f : Arrow a b)
       where
       private
-        q* : Arrow b b'
-        q* = fst (idToIso b b' q)
-        p* : Arrow a a'
+        q* : Arrow b  b'
+        q* = fst (idToIso _ _ q)
+        q~ : Arrow b' b
+        q~ = fst (snd (idToIso _ _ q))
+        p* : Arrow a  a'
         p* = fst (idToIso _ _ p)
         p~ : Arrow a' a
         p~ = fst (snd (idToIso _ _ p))
@@ -376,7 +414,8 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
         where
         lem : p~ <<< p* ≡ identity
         lem = fst (snd (snd (idToIso _ _ p)))
-    module _ {A B X : Object} (iso : A ≅ B) where
+
+    module _ {A B X : Object} (iso : A ≊ B) where
       private
         p : A ≡ B
         p = isoToId iso
@@ -384,7 +423,7 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
         p-dom = cong (λ x → Arrow x X) p
         p-cod : Arrow X A ≡ Arrow X B
         p-cod = cong (λ x → Arrow X x) p
-        lem : ∀ {A B} {x : A ≅ B} → idToIso A B (isoToId x) ≡ x
+        lem : ∀ {A B} {x : A ≊ B} → idToIso A B (isoToId x) ≡ x
         lem {x = x} i = snd inverse-from-to-iso' i x
 
       open Σ iso renaming (fst to ι) using ()
@@ -459,7 +498,7 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
         left = Xprop _ _
         right : X→Y <<< Y→X ≡ identity
         right = Yprop _ _
-        iso : X ≅ Y
+        iso : X ≊ Y
         iso = X→Y , Y→X , left , right
         p0 : X ≡ Y
         p0 = isoToId iso
@@ -489,7 +528,7 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
         left = Yprop _ _
         right : X→Y <<< Y→X ≡ identity
         right = Xprop _ _
-        iso : X ≅ Y
+        iso : X ≊ Y
         iso = Y→X , X→Y , right , left
         res : Xi ≡ Yi
         res = lemSig propIsInitial _ _ (isoToId iso)
@@ -500,11 +539,11 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
       open import Data.Nat using (_≤_ ; z≤n ; s≤s)
       setIso : ∀ x → isSet (Isomorphism x)
       setIso x = ntypeCommulative ((s≤s {n = 1} z≤n)) (propIsomorphism x)
-      step : isSet (A ≅ B)
+      step : isSet (A ≊ B)
       step = setSig {sA = arrowsAreSets} {sB = setIso}
       res : isSet (A ≡ B)
       res = equivPreservesNType
-        {A = A ≅ B} {B = A ≡ B} {n = ⟨0⟩}
+        {A = A ≊ B} {B = A ≡ B} {n = ⟨0⟩}
         (Equivalence.symmetry (univalent≃ {A = A} {B}))
         step
 
@@ -636,10 +675,10 @@ module Opposite {ℓa ℓb : Level} where
           → a × b × c → b × a × c
         genericly (a , b , c) = (b , a , c)
 
-        shuffle : A ≅ B → A ℂ.≅ B
+        shuffle : A ≊ B → A ℂ.≊ B
         shuffle (f , g , inv) = g , f , inv
 
-        shuffle~ : A ℂ.≅ B → A ≅ B
+        shuffle~ : A ℂ.≊ B → A ≊ B
         shuffle~ (f , g , inv) = g , f , inv
 
         -- Shouldn't be necessary to use `arrowsAreSets` here, but we have it,
@@ -656,12 +695,12 @@ module Opposite {ℓa ℓb : Level} where
           open Σ r-areInv renaming (fst to r-invs ; snd to r-iso)
           open Σ r-iso renaming (fst to r-l ; snd to r-r)
 
-        ζ : A ≅ B → A ≡ B
+        ζ : A ≊ B → A ≡ B
         ζ = η ∘ shuffle
 
         -- inv : AreInverses (ℂ.idToIso A B) f
         inv-ζ : AreInverses (idToIso A B) ζ
-        -- recto-verso : ℂ.idToIso A B <<< f ≡ idFun (A ℂ.≅ B)
+        -- recto-verso : ℂ.idToIso A B <<< f ≡ idFun (A ℂ.≊ B)
         inv-ζ = record
           { fst = funExt (λ x → begin
             (ζ ∘ idToIso A B) x                       ≡⟨⟩
diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda
index ac9c9bb..63fbab7 100644
--- a/src/Cat/Category/Monad.agda
+++ b/src/Cat/Category/Monad.agda
@@ -204,11 +204,8 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
 
   open import Cat.Equivalence
 
-  Monoidal≅Kleisli : M.Monad ≅ K.Monad
-  Monoidal≅Kleisli = forth , back , funExt backeq , funExt fortheq
-
-  Monoidal≃Kleisli : M.Monad ≃ K.Monad
-  Monoidal≃Kleisli = forth , eqv
+  Monoidal≊Kleisli : M.Monad ≅ K.Monad
+  Monoidal≊Kleisli = forth , back , funExt backeq , funExt fortheq
 
   Monoidal≡Kleisli : M.Monad ≡ K.Monad
-  Monoidal≡Kleisli = ua (forth , eqv)
+  Monoidal≡Kleisli = isoToPath Monoidal≊Kleisli
diff --git a/src/Cat/Category/Monad/Voevodsky.agda b/src/Cat/Category/Monad/Voevodsky.agda
index 8f4c610..e5ff355 100644
--- a/src/Cat/Category/Monad/Voevodsky.agda
+++ b/src/Cat/Category/Monad/Voevodsky.agda
@@ -123,7 +123,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 = AreInverses {f = (fst (Monoidal≅Kleisli ℂ))} {fst (snd (Monoidal≅Kleisli ℂ))}(Monoidal≅Kleisli ℂ .snd .snd)
+      module E = AreInverses {f = (fst (Monoidal≊Kleisli ℂ))} {fst (snd (Monoidal≊Kleisli ℂ))}(Monoidal≊Kleisli ℂ .snd .snd)
 
       Monoidal→Kleisli : M.Monad → K.Monad
       Monoidal→Kleisli = E.obverse
diff --git a/src/Cat/Category/Product.agda b/src/Cat/Category/Product.agda
index 0a2ed8b..be77ec8 100644
--- a/src/Cat/Category/Product.agda
+++ b/src/Cat/Category/Product.agda
@@ -2,7 +2,7 @@
 module Cat.Category.Product where
 
 open import Cat.Prelude as P hiding (_×_ ; fst ; snd)
-open import Cat.Equivalence hiding (_≅_)
+open import Cat.Equivalence
 
 open import Cat.Category
 
@@ -176,10 +176,10 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
       open Σ x renaming (fst to xa ; snd to xb)
       open Σ 𝕐 renaming (fst to Y ; snd to y)
       open Σ y renaming (fst to ya ; snd to yb)
-      open import Cat.Equivalence using (composeIso) renaming (_≅_ to _≈_)
+      open import Cat.Equivalence using (composeIso) renaming (_≅_ to _≅_)
       step0
         : ((X , xa , xb) ≡ (Y , ya , yb))
-        ≈ (Σ[ p ∈ (X ≡ Y) ] (PathP (λ i → ℂ.Arrow (p i) A) xa ya) × (PathP (λ i → ℂ.Arrow (p i) B) xb yb))
+        ≅ (Σ[ p ∈ (X ≡ Y) ] (PathP (λ i → ℂ.Arrow (p i) A) xa ya) × (PathP (λ i → ℂ.Arrow (p i) B) xb yb))
       step0
         = (λ p → cong fst p , cong-d (fst ∘ snd) p , cong-d (snd ∘ snd) p)
         -- , (λ x  → λ i → fst x i , (fst (snd x) i) , (snd (snd x) i))
@@ -190,7 +190,7 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
       -- Should follow from c being univalent
       iso-id-inv : {p : X ≡ Y} → p ≡ ℂ.isoToId (ℂ.idToIso X Y p)
       iso-id-inv {p} = sym (λ i → fst (ℂ.inverse-from-to-iso' {X} {Y}) i p)
-      id-iso-inv : {iso : X ℂ.≅ Y} → iso ≡ ℂ.idToIso X Y (ℂ.isoToId iso)
+      id-iso-inv : {iso : X ℂ.≊ Y} → iso ≡ ℂ.idToIso X Y (ℂ.isoToId iso)
       id-iso-inv {iso} = sym (λ i → snd (ℂ.inverse-from-to-iso' {X} {Y}) i iso)
 
       lemA : {A B : Object} {f g : Arrow A B} → fst f ≡ fst g → f ≡ g
@@ -207,7 +207,7 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
 
       step1
         : (Σ[ p ∈ (X ≡ Y) ] (PathP (λ i → ℂ.Arrow (p i) A) xa ya) × (PathP (λ i → ℂ.Arrow (p i) B) xb yb))
-        ≈ Σ (X ℂ.≅ Y) (λ iso
+        ≅ Σ (X ℂ.≊ Y) (λ iso
           → let p = ℂ.isoToId iso
           in
           ( PathP (λ i → ℂ.Arrow (p i) A) xa ya)
@@ -216,7 +216,7 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
       step1
         = symIso
             (isoSigFst
-              {A = (X ℂ.≅ Y)}
+              {A = (X ℂ.≊ Y)}
               {B = (X ≡ Y)}
               (ℂ.groupoidObject _ _)
               {Q = \ p → (PathP (λ i → ℂ.Arrow (p i) A) xa ya) × (PathP (λ i → ℂ.Arrow (p i) B) xb yb)}
@@ -225,13 +225,13 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
             )
 
       step2
-        : Σ (X ℂ.≅ Y) (λ iso
+        : Σ (X ℂ.≊ Y) (λ iso
           → let p = ℂ.isoToId iso
           in
           ( PathP (λ i → ℂ.Arrow (p i) A) xa ya)
           × PathP (λ i → ℂ.Arrow (p i) B) xb yb
           )
-        ≈ ((X , xa , xb) ≅ (Y , ya , yb))
+        ≅ ((X , xa , xb) ≊ (Y , ya , yb))
       step2
         = ( λ{ (iso@(f , f~ , inv-f) , p , q)
             → ( f  , sym (ℂ.domain-twist0 iso p) , sym (ℂ.domain-twist0 iso q))
@@ -242,7 +242,7 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
           )
         , (λ{ (f , f~ , inv-f , inv-f~) →
           let
-            iso : X ℂ.≅ Y
+            iso : X ℂ.≊ Y
             iso = fst f , fst f~ , cong fst inv-f , cong fst inv-f~
             p : X ≡ Y
             p = ℂ.isoToId iso
@@ -275,14 +275,14 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
       -- must compose to give idToIso
       iso
         : ((X , xa , xb) ≡ (Y , ya , yb))
-        ≈ ((X , xa , xb) ≅ (Y , ya , yb))
+        ≅ ((X , xa , xb) ≊ (Y , ya , yb))
       iso = step0 ⊙ step1 ⊙ step2
         where
         infixl 5 _⊙_
         _⊙_ = composeIso
       equiv1
         : ((X , xa , xb) ≡ (Y , ya , yb))
-        ≃ ((X , xa , xb) ≅ (Y , ya , yb))
+        ≃ ((X , xa , xb) ≊ (Y , ya , yb))
       equiv1 = _ , fromIso _ _ (snd iso)
 
     univalent : Univalent
diff --git a/src/Cat/Equivalence.agda b/src/Cat/Equivalence.agda
index 2972c2b..a6a8582 100644
--- a/src/Cat/Equivalence.agda
+++ b/src/Cat/Equivalence.agda
@@ -5,7 +5,7 @@ open import Cubical.Primitives
 open import Cubical.FromStdLib renaming (ℓ-max to _⊔_)
 open import Cubical.PathPrelude hiding (inverse)
 open import Cubical.PathPrelude using (isEquiv ; isContr ; fiber) public
-open import Cubical.GradLemma
+open import Cubical.GradLemma hiding (isoToPath)
 
 open import Cat.Prelude using (lemPropF ; setPi ; lemSig ; propSet ; Preorder ; equalityIsEquivalence ; propSig ; id-coe)
 
@@ -329,6 +329,9 @@ preorder≅ ℓ = record
 
 
 module _ {ℓ : Level} {A B : Set ℓ} where
+  isoToPath : (A ≅ B) → (A ≡ B)
+  isoToPath = ua ∘ fromIsomorphism _ _
+
   univalence : (A ≡ B) ≃ (A ≃ B)
   univalence = Equivalence.compose u' aux
     where
diff --git a/src/Cat/Prelude.agda b/src/Cat/Prelude.agda
index 55f031c..bedad50 100644
--- a/src/Cat/Prelude.agda
+++ b/src/Cat/Prelude.agda
@@ -90,6 +90,7 @@ IsPreorder
 IsPreorder _~_ = Relation.Binary.IsPreorder _≡_ _~_
 
 module _ {ℓ : Level} {A : Set ℓ} {a : A} where
+  -- FIXME rename to `coe-neutral`
   id-coe : coe refl a ≡ a
   id-coe = begin
     coe refl a                 ≡⟨⟩