From 69689e7b2a8a29a39f6c6cb7b5a3c7e337dae3e8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Fri, 6 Apr 2018 18:27:24 +0200
Subject: [PATCH] Use a single version of \simeq

---
 src/Cat/Categories/Fam.agda   |   3 -
 src/Cat/Categories/Fun.agda   |   1 -
 src/Cat/Categories/Sets.agda  |  79 ++++++++----------------
 src/Cat/Category.agda         |  35 +++++------
 src/Cat/Category/Functor.agda |   1 -
 src/Cat/Category/Product.agda |   6 +-
 src/Cat/Equivalence.agda      | 113 ++++++++++++++--------------------
 src/Cat/Prelude.agda          |   2 +-
 8 files changed, 91 insertions(+), 149 deletions(-)

diff --git a/src/Cat/Categories/Fam.agda b/src/Cat/Categories/Fam.agda
index e90838c..dd5c757 100644
--- a/src/Cat/Categories/Fam.agda
+++ b/src/Cat/Categories/Fam.agda
@@ -33,9 +33,6 @@ module _ (ℓa ℓb : Level) where
     isIdentity : IsIdentity λ { {A} → identity {A} }
     isIdentity = (Σ≡ refl refl) , Σ≡ refl refl
 
-    open import Cubical.NType.Properties
-    open import Cubical.Sigma
-
     isPreCategory : IsPreCategory RawFam
     IsPreCategory.isAssociative isPreCategory
       {A} {B} {C} {D} {f} {g} {h} = isAssociative {A} {B} {C} {D} {f} {g} {h}
diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda
index be37dcb..48ee817 100644
--- a/src/Cat/Categories/Fun.agda
+++ b/src/Cat/Categories/Fun.agda
@@ -78,7 +78,6 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C
           F[ F  ∘ G~ ] ≡⟨ prop1 ⟩
           idFunctor ∎
 
-        open import Cubical.Univalence
         p0 : F ≡ G
         p0 = begin
           F                              ≡⟨ sym Functors.rightIdentity ⟩
diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda
index a323481..7870fc0 100644
--- a/src/Cat/Categories/Sets.agda
+++ b/src/Cat/Categories/Sets.agda
@@ -2,21 +2,15 @@
 {-# OPTIONS --allow-unsolved-metas --cubical --caching #-}
 module Cat.Categories.Sets where
 
-open import Cat.Prelude as P hiding (_≃_)
+open import Cat.Prelude as P
 
 open import Function using (_∘_ ; _∘′_)
 
-open import Cubical.Univalence using (univalence ; con ; _≃_ ; idtoeqv ; ua)
-
 open import Cat.Category
 open import Cat.Category.Functor
 open import Cat.Category.Product
 open import Cat.Wishlist
-open import Cat.Equivalence as Eqv using (AreInverses ; module Equiv≃ ; module NoEta)
-
-open NoEta
-
-module Equivalence = Equivalence′
+open import Cat.Equivalence renaming (_≅_ to _≈_)
 
 _⊙_ : {ℓ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
@@ -52,7 +46,7 @@ module _ (ℓ : Level) where
 
     open IsPreCategory isPreCat hiding (_∘_)
 
-    isIso = Eqv.Isomorphism
+    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)
@@ -95,7 +89,7 @@ module _ (ℓ : Level) where
     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
+      lem2 pA p q = fromIsomorphism _ _ iso
         where
         f : ∀ {p q} → p ≡ q → fst p ≡ fst q
         f e i = fst (e i)
@@ -111,7 +105,7 @@ module _ (ℓ : Level) where
           { verso-recto = funExt ve-re
           ; recto-verso = funExt re-ve
           }
-        iso : (p ≡ q) Eqv.≅ (fst p ≡ fst q)
+        iso : (p ≡ q) ≈ (fst p ≡ fst q)
         iso = f , g , inv
 
       lem3 : ∀ {ℓc} {Q : A → Set (ℓc ⊔ ℓb)}
@@ -119,12 +113,12 @@ module _ (ℓ : Level) where
       lem3 {Q = Q} eA = res
         where
         f : Σ A P → Σ A Q
-        f (a , pA) = a , _≃_.eqv (eA a) pA
+        f (a , pA) = a , fst (eA a) pA
         g : Σ A Q → Σ A P
         g (a , qA) = a , g' qA
           where
-          k : Eqv.Isomorphism _
-          k = Equiv≃.toIso _ _ (_≃_.isEqv (eA a))
+          k : TypeIsomorphism _
+          k = toIso _ _ (snd (eA a))
           open Σ k renaming (fst to g')
         ve-re : (x : Σ A P) → (g ∘ f) x ≡ x
         ve-re x i = fst x , eq i
@@ -133,16 +127,16 @@ module _ (ℓ : Level) where
           eq = begin
             snd ((g ∘ f) x) ≡⟨⟩
             snd (g (f (a , pA))) ≡⟨⟩
-            g' (_≃_.eqv (eA a) pA) ≡⟨ lem ⟩
+            g' (fst (eA a) pA) ≡⟨ lem ⟩
             pA ∎
             where
             open Σ x renaming (fst to a ; snd to pA)
-            k : Eqv.Isomorphism _
-            k = Equiv≃.toIso _ _ (_≃_.isEqv (eA a))
+            k : TypeIsomorphism _
+            k = toIso _ _ (snd (eA a))
             open Σ k renaming (fst to g' ; snd to inv)
             module A = AreInverses inv
             -- anti-funExt
-            lem : (g' ∘ (_≃_.eqv (eA a))) pA ≡ pA
+            lem : (g' ∘ (fst (eA a))) pA ≡ pA
             lem i = A.verso-recto i pA
         re-ve : (x : Σ A Q) → (f ∘ g) x ≡ x
         re-ve x i = fst x , eq i
@@ -150,11 +144,11 @@ module _ (ℓ : Level) where
           open Σ x renaming (fst to a ; snd to qA)
           eq = begin
             snd ((f ∘ g) x)                 ≡⟨⟩
-            _≃_.eqv (eA a) (g' qA)            ≡⟨ (λ i → A.recto-verso i qA) ⟩
+            fst (eA a) (g' qA)            ≡⟨ (λ i → A.recto-verso i qA) ⟩
             qA                                ∎
             where
-            k : Eqv.Isomorphism _
-            k = Equiv≃.toIso _ _ (_≃_.isEqv (eA a))
+            k : TypeIsomorphism _
+            k = toIso _ _ (snd (eA a))
             open Σ k renaming (fst to g' ; snd to inv)
             module A = AreInverses inv
         inv : AreInverses f g
@@ -162,10 +156,10 @@ module _ (ℓ : Level) where
           { verso-recto = funExt ve-re
           ; recto-verso = funExt re-ve
           }
-        iso : Σ A P Eqv.≅ Σ A Q
+        iso : Σ A P ≈ Σ A Q
         iso = f , g , inv
         res : Σ A P ≃ Σ A Q
-        res = fromIsomorphism iso
+        res = fromIsomorphism _ _ iso
 
     module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where
       lem4 : isSet A → isSet B → (f : A → B)
@@ -173,20 +167,20 @@ module _ (ℓ : Level) where
       lem4 sA sB f =
         let
           obv : isEquiv A B f → isIso f
-          obv = Equiv≃.toIso A B
+          obv = toIso A B
           inv : isIso f → isEquiv A B f
-          inv = Equiv≃.fromIso A B
+          inv = fromIso A B
           re-ve : (x : isEquiv A B f) → (inv ∘ obv) x ≡ x
-          re-ve = Equiv≃.inverse-from-to-iso A B
+          re-ve = inverse-from-to-iso A B
           ve-re : (x : isIso f)       → (obv ∘ inv) x ≡ x
-          ve-re = Equiv≃.inverse-to-from-iso A B sA sB
-          iso : isEquiv A B f Eqv.≅ isIso f
+          ve-re = inverse-to-from-iso A B sA sB
+          iso : isEquiv A B f ≈ isIso f
           iso = obv , inv ,
             record
               { verso-recto = funExt re-ve
               ; recto-verso = funExt ve-re
               }
-        in fromIsomorphism iso
+        in fromIsomorphism _ _ iso
 
     module _ {hA hB : Object} where
       open Σ hA renaming (fst to A ; snd to sA)
@@ -198,33 +192,15 @@ module _ (ℓ : Level) where
 
       -- univalence
       step1 : Σ (A → B) (isEquiv A B) ≃ (A ≡ B)
-      step1 = hh ⊙ h
-        where
-          h : (A ≃ B) ≃ (A ≡ B)
-          h = sym≃ (univalence {A = A} {B})
-          obv : Σ (A → B) (isEquiv A B) → A ≃ B
-          obv = Eqv.deEta
-          inv : A ≃ B → Σ (A → B) (isEquiv A B)
-          inv = Eqv.doEta
-          re-ve : (x : _) → (inv ∘ obv) x ≡ x
-          re-ve x = refl
-          -- Because _≃_ does not have eta equality!
-          ve-re : (x : _) → (obv ∘ inv) x ≡ x
-          ve-re (con eqv isEqv) i = con eqv isEqv
-          areInv : AreInverses obv inv
-          areInv = record { verso-recto = funExt re-ve ; recto-verso = funExt ve-re }
-          eqv : Σ (A → B) (isEquiv A B) Eqv.≅ (A ≃ B)
-          eqv = obv , inv , areInv
-          hh : Σ (A → B) (isEquiv A B) ≃ (A ≃ B)
-          hh = fromIsomorphism eqv
+      step1 = sym≃ univalence
 
       -- lem2 with propIsSet
       step2 : (A ≡ B) ≃ (hA ≡ hB)
       step2 = sym≃ (lem2 (λ A → isSetIsProp) hA hB)
 
       -- Go from an isomorphism on sets to an isomorphism on homotopic sets
-      trivial? : (hA ≅ hB) ≃ (A Eqv.≅ B)
-      trivial? = sym≃ (fromIsomorphism res)
+      trivial? : (hA ≅ hB) ≃ (A ≈ B)
+      trivial? = sym≃ (fromIsomorphism _ _ res)
         where
         fwd : Σ (A → B) isIso → hA ≅ hB
         fwd (f , g , inv) = f , g , inv.toPair
@@ -232,7 +208,7 @@ module _ (ℓ : Level) where
           module inv = AreInverses inv
         bwd : hA ≅ hB → Σ (A → B) isIso
         bwd (f , g , x , y) = f , g , record { verso-recto = x ; recto-verso = y }
-        res : Σ (A → B) isIso Eqv.≅ (hA ≅ hB)
+        res : Σ (A → B) isIso ≈ (hA ≅ hB)
         res = fwd , bwd , record { verso-recto = refl ; recto-verso = refl }
 
       conclusion : (hA ≅ hB) ≃ (hA ≡ hB)
@@ -274,7 +250,6 @@ module _ {ℓ : Level} where
   private
     𝓢 = 𝓢𝓮𝓽 ℓ
     open Category 𝓢
-    open import Cubical.Sigma
 
     module _ (hA hB : Object) where
       open Σ hA renaming (fst to A ; snd to sA)
diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 7c316e9..254f024 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -29,6 +29,7 @@
 module Cat.Category where
 
 open import Cat.Prelude
+open import Cat.Equivalence as Equivalence renaming (_≅_ to _≈_ ; Isomorphism to TypeIsomorphism) hiding (preorder≅)
 
 import Function
 
@@ -122,8 +123,6 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
 
     import Cat.Equivalence as E
     open E public using () renaming (Isomorphism to TypeIsomorphism)
-    open E using (module Equiv≃)
-    open Equiv≃ using (fromIso)
 
     univalenceFromIsomorphism : {A B : Object}
       → TypeIsomorphism (idToIso A B) → isEquiv (A ≡ B) (A ≅ B) (idToIso A B)
@@ -299,10 +298,8 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
     univalent≃ = _ , univalent
 
     module _ {A B : Object} where
-      open import Cat.Equivalence using (module Equiv≃)
-
       iso-to-id : (A ≅ B) → (A ≡ B)
-      iso-to-id = fst (Equiv≃.toIso _ _ univalent)
+      iso-to-id = fst (toIso _ _ univalent)
 
     -- | All projections are propositions.
     module Propositionality where
@@ -321,7 +318,6 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
         open Σ Yt renaming (fst to Y ; snd to Yit)
         open Σ (Xit {Y}) renaming (fst to Y→X) using ()
         open Σ (Yit {X}) renaming (fst to X→Y) using ()
-        open import Cat.Equivalence hiding (_≅_)
         -- Need to show `left` and `right`, what we know is that the arrows are
         -- unique. Well, I know that if I compose these two arrows they must give
         -- the identity, since also the identity is the unique such arrow (by X
@@ -336,10 +332,10 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
         right = Yprop _ _
         iso : X ≅ Y
         iso = X→Y , Y→X , left , right
-        fromIso : X ≅ Y → X ≡ Y
-        fromIso = fst (Equiv≃.toIso (X ≡ Y) (X ≅ Y) univalent)
+        fromIso' : X ≅ Y → X ≡ Y
+        fromIso' = fst (toIso (X ≡ Y) (X ≅ Y) univalent)
         p0 : X ≡ Y
-        p0 = fromIso iso
+        p0 = fromIso' iso
         p1 : (λ i → IsTerminal (p0 i)) [ Xit ≡ Yit ]
         p1 = lemPropF propIsTerminal p0
         res : Xt ≡ Yt
@@ -354,7 +350,6 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
         open Σ Yi renaming (fst to Y ; snd to Yii)
         open Σ (Xii {Y}) renaming (fst to Y→X) using ()
         open Σ (Yii {X}) renaming (fst to X→Y) using ()
-        open import Cat.Equivalence hiding (_≅_)
         -- Need to show `left` and `right`, what we know is that the arrows are
         -- unique. Well, I know that if I compose these two arrows they must give
         -- the identity, since also the identity is the unique such arrow (by X
@@ -369,10 +364,10 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
         right = Xprop _ _
         iso : X ≅ Y
         iso = Y→X , X→Y , right , left
-        fromIso : X ≅ Y → X ≡ Y
-        fromIso = fst (Equiv≃.toIso (X ≡ Y) (X ≅ Y) univalent)
+        fromIso' : X ≅ Y → X ≡ Y
+        fromIso' = fst (toIso (X ≡ Y) (X ≅ Y) univalent)
         p0 : X ≡ Y
-        p0 = fromIso iso
+        p0 = fromIso' iso
         p1 : (λ i → IsInitial (p0 i)) [ Xii ≡ Yii ]
         p1 = lemPropF propIsInitial p0
         res : Xi ≡ Yi
@@ -436,9 +431,12 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
   propIsCategory : isProp (IsCategory ℂ)
   propIsCategory = done
 
+
 -- | Univalent categories
 --
 -- Just bundles up the data with witnesses inhabiting the propositions.
+
+-- Question: Should I remove the type `Category`?
 record Category (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
   field
     raw            : RawCategory ℓa ℓb
@@ -459,10 +457,8 @@ module _ {ℓa ℓb : Level} {ℂ 𝔻 : Category ℓa ℓb} where
       isCategoryEq = lemPropF propIsCategory rawEq
 
     Category≡ : ℂ ≡ 𝔻
-    Category≡ i = record
-      { raw        = rawEq i
-      ; isCategory = isCategoryEq i
-      }
+    Category.raw (Category≡ i) = rawEq i
+    Category.isCategory (Category≡ i) = isCategoryEq i
 
 -- | Syntax for arrows- and composition in a given category.
 module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
@@ -501,9 +497,8 @@ module Opposite {ℓa ℓb : Level} where
       open IsPreCategory isPreCategory
 
       module _ {A B : ℂ.Object} where
-        open import Cat.Equivalence as Equivalence hiding (_≅_)
         k : Equivalence.Isomorphism (ℂ.idToIso A B)
-        k = Equiv≃.toIso _ _ ℂ.univalent
+        k = toIso _ _ ℂ.univalent
         open Σ k renaming (fst to f ; snd to inv)
         open AreInverses inv
 
@@ -568,7 +563,7 @@ module Opposite {ℓa ℓb : Level} where
         h = ff , invv
         univalent : isEquiv (A ≡ B) (A ≅ B)
           (Univalence.idToIso (swap ℂ.isIdentity) A B)
-        univalent = Equiv≃.fromIso _ _ h
+        univalent = fromIso _ _ h
 
       isCategory : IsCategory opRaw
       IsCategory.isPreCategory isCategory = isPreCategory
diff --git a/src/Cat/Category/Functor.agda b/src/Cat/Category/Functor.agda
index c4a7346..08dcafa 100644
--- a/src/Cat/Category/Functor.agda
+++ b/src/Cat/Category/Functor.agda
@@ -5,7 +5,6 @@ open import Cat.Prelude
 open import Function
 
 open import Cubical
-open import Cubical.NType.Properties using (lemPropF)
 
 open import Cat.Category
 
diff --git a/src/Cat/Category/Product.agda b/src/Cat/Category/Product.agda
index 9def8a2..536467b 100644
--- a/src/Cat/Category/Product.agda
+++ b/src/Cat/Category/Product.agda
@@ -1,8 +1,8 @@
 {-# OPTIONS --allow-unsolved-metas --cubical #-}
 module Cat.Category.Product where
 
-open import Cubical.NType.Properties
 open import Cat.Prelude as P hiding (_×_ ; fst ; snd)
+open import Cat.Equivalence hiding (_≅_)
 -- module P = Cat.Prelude
 
 open import Cat.Category
@@ -285,10 +285,8 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
 
   open Category cat
 
-  open import Cat.Equivalence
-
   lemma : Terminal ≃ Product ℂ A B
-  lemma = Equiv≃.fromIsomorphism Terminal (Product ℂ A B) (f , g , inv)
+  lemma = fromIsomorphism Terminal (Product ℂ A B) (f , g , inv)
     where
     f : Terminal → Product ℂ A B
     f ((X , x0 , x1) , uniq) = p
diff --git a/src/Cat/Equivalence.agda b/src/Cat/Equivalence.agda
index a7386b1..43a25e4 100644
--- a/src/Cat/Equivalence.agda
+++ b/src/Cat/Equivalence.agda
@@ -3,11 +3,26 @@ module Cat.Equivalence where
 
 open import Cubical.Primitives
 open import Cubical.FromStdLib renaming (ℓ-max to _⊔_)
+-- FIXME: Don't hide ≃
 open import Cubical.PathPrelude hiding (inverse ; _≃_)
 open import Cubical.PathPrelude using (isEquiv ; isContr ; fiber) public
 open import Cubical.GradLemma
 
-open import Cat.Prelude using (lemPropF ; setPi ; lemSig ; propSet ; Preorder ; equalityIsEquivalence)
+open import Cat.Prelude using (lemPropF ; setPi ; lemSig ; propSet ; Preorder ; equalityIsEquivalence ; _≃_)
+
+import Cubical.Univalence as U
+
+module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where
+  open Cubical.PathPrelude
+  deEta : A ≃ B → A U.≃ B
+  deEta (a , b) = U.con a b
+  doEta : A U.≃ B → A ≃ B
+  doEta (U.con eqv isEqv) = eqv , isEqv
+
+module _ {ℓ : Level} {A B : Set ℓ} where
+  open Cubical.PathPrelude
+  ua : A ≃ B → A ≡ B
+  ua (f , isEqv) = U.ua (U.con f isEqv)
 
 module _ {ℓa ℓb : Level} where
   private
@@ -242,8 +257,7 @@ module _ {ℓa ℓb : Level} (A : Set ℓa) (B : Set ℓb) where
       where
       import Cubical.NType.Properties as P
 
-  module Equiv≃ where
-    open Equiv ≃isEquiv public
+  open Equiv ≃isEquiv public
 
 module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where
   open Cubical.PathPrelude using (_≃_)
@@ -273,20 +287,19 @@ module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where
         }
 
     composeIsEquiv : isEquiv A B f → isEquiv B C g → isEquiv A C (g ∘ f)
-    composeIsEquiv a b = Equiv≃.fromIso A C (composeIsomorphism a' b')
+    composeIsEquiv a b = fromIso A C (composeIsomorphism a' b')
       where
-      a' = Equiv≃.toIso A B a
-      b' = Equiv≃.toIso B C b
+      a' = toIso A B a
+      b' = toIso B C b
 
   composeIso : {ℓc : Level} {C : Set ℓc} → (A ≅ B) → (B ≅ C) → A ≅ C
   composeIso {C = C} (f , iso-f) (g , iso-g) = g ∘ f , composeIsomorphism iso-f iso-g
 
   -- Gives the quasi inverse from an equivalence.
   module Equivalence (e : A ≃ B) where
-    open Equiv≃ A B public
     private
       iso : Isomorphism (fst e)
-      iso = snd (toIsomorphism e)
+      iso = snd (toIsomorphism _ _ e)
 
     open AreInverses (snd iso) public
 
@@ -303,9 +316,7 @@ module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where
         }
 
     symmetry : B ≃ A
-    symmetry = B≃A.fromIsomorphism symmetryIso
-      where
-      module B≃A = Equiv≃ B A
+    symmetry = fromIsomorphism _ _ symmetryIso
 
 preorder≅ : (ℓ : Level) → Preorder _ _ _
 preorder≅ ℓ = record
@@ -323,54 +334,24 @@ preorder≅ ℓ = record
     ; trans = composeIso
     }
   }
-
-module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where
-  open import Cubical.PathPrelude renaming (_≃_ to _≃η_)
-  open import Cubical.Univalence using (_≃_)
-
-  doEta : A ≃ B → A ≃η B
-  doEta (_≃_.con eqv isEqv) = eqv , isEqv
-
-  deEta : A ≃η B → A ≃ B
-  deEta (eqv , isEqv) = _≃_.con eqv isEqv
-
-module NoEta {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where
-  open import Cubical.PathPrelude renaming (_≃_ to _≃η_)
-  open import Cubical.Univalence using (_≃_)
-
-  module Equivalence′ (e : A ≃ B) where
-    open Equivalence (doEta e) hiding
-      ( toIsomorphism ; fromIsomorphism ; _~_
-      ; compose ; symmetryIso ; symmetry ) public
-
-    compose : {ℓc : Level} {C : Set ℓc} → (B ≃ C) → A ≃ C
-    compose ee = deEta (Equivalence.compose (doEta e) (doEta ee))
-
-    symmetry : B ≃ A
-    symmetry = deEta (Equivalence.symmetry (doEta e))
-
-  -- fromIso      : {f : A → B} → Isomorphism f → isEquiv f
-  -- fromIso = ?
-
-  -- toIso        : {f : A → B} → isEquiv f → Isomorphism f
-  -- toIso = ?
-
-  fromIsomorphism : A ≅ B → A ≃ B
-  fromIsomorphism (f , iso) = _≃_.con f (Equiv≃.fromIso _ _ iso)
-
-  toIsomorphism : A ≃ B → A ≅ B
-  toIsomorphism (_≃_.con f eqv) = f , Equiv≃.toIso _ _ eqv
+module _ {ℓ : Level} {A B : Set ℓ} where
+  univalence : (A ≡ B) ≃ (A ≃ B)
+  univalence = Equivalence.compose u' aux
+    where
+    u : (A ≡ B) U.≃ (A U.≃ B)
+    u = U.univalence
+    u' : (A ≡ B) ≃ (A U.≃ B)
+    u' = doEta u
+    aux : (A U.≃ B) ≃ (A ≃ B)
+    aux = fromIsomorphism _ _ (doEta , deEta , record { verso-recto = funExt (λ{ (U.con _ _) → refl}) ; recto-verso = refl })
 
 -- 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
-  open NoEta
-  open import Cubical.Univalence using (_≃_)
-
   -- Equality on sigma's whose second component is a proposition is equivalent
   -- to equality on their first components.
   equivPropSig : ((x : A) → isProp (P x)) → (p q : Σ A P)
     → (p ≡ q) ≃ (fst p ≡ fst q)
-  equivPropSig pA p q = fromIsomorphism iso
+  equivPropSig pA p q = fromIsomorphism _ _ iso
     where
     f : ∀ {p q} → p ≡ q → fst p ≡ fst q
     f e i = fst (e i)
@@ -396,12 +377,12 @@ module _ {ℓa ℓb : Level} {A : Set ℓa} {P : A → Set ℓb} where
   equivSigSnd {Q = Q} eA = res
     where
     f : Σ A P → Σ A Q
-    f (a , pA) = a , _≃_.eqv (eA a) pA
+    f (a , pA) = a , fst (eA a) pA
     g : Σ A Q → Σ A P
     g (a , qA) = a , g' qA
       where
       k : Isomorphism _
-      k = Equiv≃.toIso _ _ (_≃_.isEqv (eA a))
+      k = toIso _ _ (snd (eA a))
       open Σ k renaming (fst to g')
     ve-re : (x : Σ A P) → (g ∘ f) x ≡ x
     ve-re x i = fst x , eq i
@@ -410,16 +391,16 @@ module _ {ℓa ℓb : Level} {A : Set ℓa} {P : A → Set ℓb} where
       eq = begin
         snd ((g ∘ f) x) ≡⟨⟩
         snd (g (f (a , pA))) ≡⟨⟩
-        g' (_≃_.eqv (eA a) pA) ≡⟨ lem ⟩
+        g' (fst (eA a) pA) ≡⟨ lem ⟩
         pA ∎
         where
         open Σ x renaming (fst to a ; snd to pA)
         k : Isomorphism _
-        k = Equiv≃.toIso _ _ (_≃_.isEqv (eA a))
+        k = toIso _ _ (snd (eA a))
         open Σ k renaming (fst to g' ; snd to inv)
         module A = AreInverses inv
         -- anti-funExt
-        lem : (g' ∘ (_≃_.eqv (eA a))) pA ≡ pA
+        lem : (g' ∘ (fst (eA a))) pA ≡ pA
         lem i = A.verso-recto i pA
     re-ve : (x : Σ A Q) → (f ∘ g) x ≡ x
     re-ve x i = fst x , eq i
@@ -427,11 +408,11 @@ module _ {ℓa ℓb : Level} {A : Set ℓa} {P : A → Set ℓb} where
       open Σ x renaming (fst to a ; snd to qA)
       eq = begin
         snd ((f ∘ g) x)                 ≡⟨⟩
-        _≃_.eqv (eA a) (g' qA)            ≡⟨ (λ i → A.recto-verso i qA) ⟩
+        fst (eA a) (g' qA)            ≡⟨ (λ i → A.recto-verso i qA) ⟩
         qA                                ∎
         where
         k : Isomorphism _
-        k = Equiv≃.toIso _ _ (_≃_.isEqv (eA a))
+        k = toIso _ _ (snd (eA a))
         open Σ k renaming (fst to g' ; snd to inv)
         module A = AreInverses inv
     inv : AreInverses f g
@@ -442,11 +423,9 @@ module _ {ℓa ℓb : Level} {A : Set ℓa} {P : A → Set ℓb} where
     iso : Σ A P ≅ Σ A Q
     iso = f , g , inv
     res : Σ A P ≃ Σ A Q
-    res = fromIsomorphism iso
+    res = fromIsomorphism _ _ iso
 
 module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where
-  open NoEta
-  open import Cubical.Univalence using (_≃_)
   -- Equivalence is equivalent to isomorphism when the domain and codomain of
   -- the equivalence is a set.
   equivSetIso : isSet A → isSet B → (f : A → B)
@@ -454,17 +433,17 @@ module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where
   equivSetIso sA sB f =
     let
       obv : isEquiv A B f → Isomorphism f
-      obv = Equiv≃.toIso A B
+      obv = toIso A B
       inv : Isomorphism f → isEquiv A B f
-      inv = Equiv≃.fromIso A B
+      inv = fromIso A B
       re-ve : (x : isEquiv A B f) → (inv ∘ obv) x ≡ x
-      re-ve = Equiv≃.inverse-from-to-iso A B
+      re-ve = inverse-from-to-iso A B
       ve-re : (x : Isomorphism f)       → (obv ∘ inv) x ≡ x
-      ve-re = Equiv≃.inverse-to-from-iso A B sA sB
+      ve-re = inverse-to-from-iso A B sA sB
       iso : isEquiv A B f ≅ Isomorphism f
       iso = obv , inv ,
         record
           { verso-recto = funExt re-ve
           ; recto-verso = funExt ve-re
           }
-    in fromIsomorphism iso
+    in fromIsomorphism _ _ iso
diff --git a/src/Cat/Prelude.agda b/src/Cat/Prelude.agda
index a01dc25..0646bf5 100644
--- a/src/Cat/Prelude.agda
+++ b/src/Cat/Prelude.agda
@@ -24,7 +24,7 @@ open import Cubical.NType.Properties
   using
     ( lemPropF ; lemSig ;  lemSigP ; isSetIsProp
     ; propPi ; propPiImpl ; propHasLevel ; setPi ; propSet
-    ; propSig)
+    ; propSig ; equivPreservesNType)
   public
 
 propIsContr : {ℓ : Level} → {A : Set ℓ} → isProp (isContr A)