diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda
index a5d986e..da421e9 100644
--- a/src/Cat/Categories/Cat.agda
+++ b/src/Cat/Categories/Cat.agda
@@ -3,7 +3,7 @@
 
 module Cat.Categories.Cat where
 
-open import Cat.Prelude renaming (proj₁ to fst ; proj₂ to snd)
+open import Cat.Prelude renaming (fst to fst ; snd to snd)
 
 open import Cat.Category
 open import Cat.Category.Functor
@@ -83,16 +83,16 @@ module CatProduct {ℓ ℓ' : Level} (ℂ 𝔻 : Category ℓ ℓ') where
   object : Category ℓ ℓ'
   Category.raw object = rawProduct
 
-  proj₁ : Functor object ℂ
-  proj₁ = record
+  fstF : Functor object ℂ
+  fstF = record
     { raw = record
       { omap = fst ; fmap = fst }
     ; isFunctor = record
       { isIdentity = refl ; isDistributive = refl }
     }
 
-  proj₂ : Functor object 𝔻
-  proj₂ = record
+  sndF : Functor object 𝔻
+  sndF = record
     { raw = record
       { omap = snd ; fmap = snd }
     ; isFunctor = record
@@ -116,19 +116,19 @@ module CatProduct {ℓ ℓ' : Level} (ℂ 𝔻 : Category ℓ ℓ') where
           open module x₁ = Functor x₁
           open module x₂ = Functor x₂
 
-      isUniqL : F[ proj₁ ∘ x ] ≡ x₁
+      isUniqL : F[ fstF ∘ x ] ≡ x₁
       isUniqL = Functor≡ refl
 
-      isUniqR : F[ proj₂ ∘ x ] ≡ x₂
+      isUniqR : F[ sndF ∘ x ] ≡ x₂
       isUniqR = Functor≡ refl
 
-      isUniq : F[ proj₁ ∘ x ] ≡ x₁ × F[ proj₂ ∘ x ] ≡ x₂
+      isUniq : F[ fstF ∘ x ] ≡ x₁ × F[ sndF ∘ x ] ≡ x₂
       isUniq = isUniqL , isUniqR
 
-    isProduct : ∃![ x ] (F[ proj₁ ∘ x ] ≡ x₁ × F[ proj₂ ∘ x ] ≡ x₂)
+    isProduct : ∃![ x ] (F[ fstF ∘ x ] ≡ x₁ × F[ sndF ∘ x ] ≡ x₂)
     isProduct = x , isUniq , uq
       where
-      module _ {y : Functor X object} (eq : F[ proj₁ ∘ y ] ≡ x₁ × F[ proj₂ ∘ y ] ≡ x₂) where
+      module _ {y : Functor X object} (eq : F[ fstF ∘ y ] ≡ x₁ × F[ sndF ∘ y ] ≡ x₂) where
         omapEq : Functor.omap x ≡ Functor.omap y
         omapEq = {!!}
         -- fmapEq : (λ i → {!{A B : ?} → Arrow A B → 𝔻 [ ? A , ? B ]!}) [ Functor.fmap x ≡ Functor.fmap y ]
@@ -148,8 +148,8 @@ module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where
 
       rawProduct : RawProduct Catℓ ℂ 𝔻
       RawProduct.object rawProduct = P.object
-      RawProduct.proj₁  rawProduct = P.proj₁
-      RawProduct.proj₂  rawProduct = P.proj₂
+      RawProduct.fst  rawProduct = P.fstF
+      RawProduct.snd  rawProduct = P.sndF
 
       isProduct : IsProduct Catℓ _ _ rawProduct
       IsProduct.ump isProduct = P.isProduct
@@ -182,8 +182,8 @@ module CatExponential {ℓ : Level} (ℂ 𝔻 : Category ℓ ℓ) where
   object = Fun
 
   module _ {dom cod : Functor ℂ 𝔻 × ℂ.Object} where
-    open Σ dom renaming (proj₁ to F ; proj₂ to A)
-    open Σ cod renaming (proj₁ to G ; proj₂ to B)
+    open Σ dom renaming (fst to F ; snd to A)
+    open Σ cod renaming (fst to G ; snd to B)
     private
       module F = Functor F
       module G = Functor G
@@ -200,7 +200,7 @@ module CatExponential {ℓ : Level} (ℂ 𝔻 : Category ℓ ℓ) where
   open CatProduct renaming (object to _⊗_) using ()
 
   module _ {c : Functor ℂ 𝔻 × ℂ.Object} where
-    open Σ c renaming (proj₁ to F ; proj₂ to C)
+    open Σ c renaming (fst to F ; snd to C)
 
     ident : fmap {c} {c} (identityNT F , ℂ.identity {A = snd c}) ≡ 𝔻.identity
     ident = begin
@@ -214,9 +214,9 @@ module CatExponential {ℓ : Level} (ℂ 𝔻 : Category ℓ ℓ) where
         module F = Functor F
 
   module _ {F×A G×B H×C : Functor ℂ 𝔻 × ℂ.Object} where
-    open Σ F×A renaming (proj₁ to F ; proj₂ to A)
-    open Σ G×B renaming (proj₁ to G ; proj₂ to B)
-    open Σ H×C renaming (proj₁ to H ; proj₂ to C)
+    open Σ F×A renaming (fst to F ; snd to A)
+    open Σ G×B renaming (fst to G ; snd to B)
+    open Σ H×C renaming (fst to H ; snd to C)
     private
       module F = Functor F
       module G = Functor G
@@ -225,14 +225,14 @@ module CatExponential {ℓ : Level} (ℂ 𝔻 : Category ℓ ℓ) where
     module _
       {θ×f : NaturalTransformation F G × ℂ [ A , B ]}
       {η×g : NaturalTransformation G H × ℂ [ B , C ]} where
-      open Σ θ×f renaming (proj₁ to θNT ; proj₂ to f)
-      open Σ θNT renaming (proj₁ to θ   ; proj₂ to θNat)
-      open Σ η×g renaming (proj₁ to ηNT ; proj₂ to g)
-      open Σ ηNT renaming (proj₁ to η   ; proj₂ to ηNat)
+      open Σ θ×f renaming (fst to θNT ; snd to f)
+      open Σ θNT renaming (fst to θ   ; snd to θNat)
+      open Σ η×g renaming (fst to ηNT ; snd to g)
+      open Σ ηNT renaming (fst to η   ; snd to ηNat)
       private
         ηθNT : NaturalTransformation F H
         ηθNT = NT[_∘_] {F} {G} {H} ηNT θNT
-      open Σ ηθNT renaming (proj₁ to ηθ   ; proj₂ to ηθNat)
+      open Σ ηθNT renaming (fst to ηθ   ; snd to ηθNat)
 
       isDistributive :
           𝔻 [ 𝔻 [ η C ∘ θ C ] ∘ F.fmap ( ℂ [ g ∘ f ] ) ]
diff --git a/src/Cat/Categories/CwF.agda b/src/Cat/Categories/CwF.agda
index 45dbf2b..1a491ec 100644
--- a/src/Cat/Categories/CwF.agda
+++ b/src/Cat/Categories/CwF.agda
@@ -25,21 +25,21 @@ module _ {ℓa ℓb : Level} where
     private
       module T = Functor T
     Type : (Γ : ℂ.Object) → Set ℓa
-    Type Γ = proj₁ (proj₁ (T.omap Γ))
+    Type Γ = fst (fst (T.omap Γ))
 
     module _ {Γ : ℂ.Object} {A : Type Γ} where
 
       -- module _ {A B : Object ℂ} {γ : ℂ [ A , B ]} where
-      --   k : Σ (proj₁ (omap T B) → proj₁ (omap T A))
+      --   k : Σ (fst (omap T B) → fst (omap T A))
       --     (λ f →
-      --     {x : proj₁ (omap T B)} →
-      --     proj₂ (omap T B) x → proj₂ (omap T A) (f x))
+      --     {x : fst (omap T B)} →
+      --     snd (omap T B) x → snd (omap T A) (f x))
       --   k = T.fmap γ
-      --   k₁ : proj₁ (omap T B) → proj₁ (omap T A)
-      --   k₁ = proj₁ k
-      --   k₂ : ({x : proj₁ (omap T B)} →
-      --     proj₂ (omap T B) x → proj₂ (omap T A) (k₁ x))
-      --   k₂ = proj₂ k
+      --   k₁ : fst (omap T B) → fst (omap T A)
+      --   k₁ = fst k
+      --   k₂ : ({x : fst (omap T B)} →
+      --     snd (omap T B) x → snd (omap T A) (k₁ x))
+      --   k₂ = snd k
 
       record ContextComprehension : Set (ℓa ⊔ ℓb) where
         field
diff --git a/src/Cat/Categories/Fam.agda b/src/Cat/Categories/Fam.agda
index ff4fafc..897d6e0 100644
--- a/src/Cat/Categories/Fam.agda
+++ b/src/Cat/Categories/Fam.agda
@@ -8,12 +8,12 @@ open import Cat.Category
 
 module _ (ℓa ℓb : Level) where
   private
-    Object = Σ[ hA ∈ hSet ℓa ] (proj₁ hA → hSet ℓb)
+    Object = Σ[ hA ∈ hSet ℓa ] (fst hA → hSet ℓb)
     Arr : Object → Object → Set (ℓa ⊔ ℓb)
-    Arr ((A , _) , B) ((A' , _) , B') = Σ[ f ∈ (A → A') ] ({x : A} → proj₁ (B x) → proj₁ (B' (f x)))
+    Arr ((A , _) , B) ((A' , _) , B') = Σ[ f ∈ (A → A') ] ({x : A} → fst (B x) → fst (B' (f x)))
     identity : {A : Object} → Arr A A
-    proj₁ identity = λ x → x
-    proj₂ identity = λ b → b
+    fst identity = λ x → x
+    snd identity = λ b → b
     _∘_ : {a b c : Object} → Arr b c → Arr a b → Arr a c
     (g , g') ∘ (f , f') = g Function.∘ f , g' Function.∘ f'
 
@@ -47,11 +47,11 @@ module _ (ℓa ℓb : Level) where
               {sA = setPi λ _ → hB}
               {sB = λ f →
                 let
-                  helpr : isSet ((a : A) → proj₁ (famA a) → proj₁ (famB (f a)))
-                  helpr = setPi λ a → setPi λ _ → proj₂ (famB (f a))
+                  helpr : isSet ((a : A) → fst (famA a) → fst (famB (f a)))
+                  helpr = setPi λ a → setPi λ _ → snd (famB (f a))
                   -- It's almost like above, but where the first argument is
                   -- implicit.
-                  res : isSet ({a : A} → proj₁ (famA a) → proj₁ (famB (f a)))
+                  res : isSet ({a : A} → fst (famA a) → fst (famB (f a)))
                   res = {!!}
                 in res
               }
diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda
index 1cd2e0a..63e6f1b 100644
--- a/src/Cat/Categories/Fun.agda
+++ b/src/Cat/Categories/Fun.agda
@@ -29,16 +29,16 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C
       center : Σ[ G ∈ Object ] (F ≅ G)
       center = F , id-to-iso F F refl
 
-      open Σ center renaming (proj₂ to isoF)
+      open Σ center renaming (snd to isoF)
 
       module _ (cG : Σ[ G ∈ Object ] (F ≅ G)) where
-        open Σ cG renaming (proj₁ to G ; proj₂ to isoG)
+        open Σ cG renaming (fst to G ; snd to isoG)
         module G = Functor G
-        open Σ isoG   renaming (proj₁ to θNT ; proj₂ to invθNT)
-        open Σ invθNT renaming (proj₁ to ηNT ; proj₂ to areInv)
-        open Σ θNT    renaming (proj₁ to θ   ; proj₂ to θN)
-        open Σ ηNT    renaming (proj₁ to η   ; proj₂ to ηN)
-        open Σ areInv renaming (proj₁ to ve-re ; proj₂ to re-ve)
+        open Σ isoG   renaming (fst to θNT ; snd to invθNT)
+        open Σ invθNT renaming (fst to ηNT ; snd to areInv)
+        open Σ θNT    renaming (fst to θ   ; snd to θN)
+        open Σ ηNT    renaming (fst to η   ; snd to ηN)
+        open Σ areInv renaming (fst to ve-re ; snd to re-ve)
 
         -- f ~ Transformation G G
         -- f : (X : ℂ.Object) → 𝔻 [ G.omap X , G.omap X ]
diff --git a/src/Cat/Categories/Rel.agda b/src/Cat/Categories/Rel.agda
index 73d4bff..e4e9edc 100644
--- a/src/Cat/Categories/Rel.agda
+++ b/src/Cat/Categories/Rel.agda
@@ -1,7 +1,7 @@
 {-# OPTIONS --cubical --allow-unsolved-metas #-}
 module Cat.Categories.Rel where
 
-open import Cat.Prelude renaming (proj₁ to fst ; proj₂ to snd)
+open import Cat.Prelude renaming (fst to fst ; snd to snd)
 open import Function
 
 open import Cat.Category
diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda
index ab094c9..683192b 100644
--- a/src/Cat/Categories/Sets.agda
+++ b/src/Cat/Categories/Sets.agda
@@ -2,8 +2,7 @@
 {-# OPTIONS --allow-unsolved-metas --cubical --caching #-}
 module Cat.Categories.Sets where
 
-open import Cat.Prelude hiding (_≃_)
-import Data.Product
+open import Cat.Prelude as P hiding (_≃_)
 
 open import Function using (_∘_ ; _∘′_)
 
@@ -38,8 +37,8 @@ module _ (ℓ : Level) where
     open RawCategory SetsRaw hiding (_∘_)
 
     isIdentity : IsIdentity Function.id
-    proj₁ isIdentity = funExt λ _ → refl
-    proj₂ isIdentity = funExt λ _ → refl
+    fst isIdentity = funExt λ _ → refl
+    snd isIdentity = funExt λ _ → refl
 
     open Univalence (λ {A} {B} {f} → isIdentity {A} {B} {f})
 
@@ -48,14 +47,14 @@ module _ (ℓ : Level) where
 
     isIso = Eqv.Isomorphism
     module _ {hA hB : hSet ℓ} where
-      open Σ hA renaming (proj₁ to A ; proj₂ to sA)
-      open Σ hB renaming (proj₁ to B ; proj₂ to sB)
+      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 (proj₁ to inverse ; proj₂ to areInverses)
-          module y = Σ y renaming (proj₁ to inverse ; proj₂ to areInverses)
+          module x = Σ x renaming (fst to inverse ; snd to areInverses)
+          module y = Σ y renaming (fst to inverse ; snd to areInverses)
           module xA = AreInverses x.areInverses
           module yA = AreInverses y.areInverses
           -- I had a lot of difficulty using the corresponding proof where
@@ -88,24 +87,24 @@ module _ (ℓ : Level) where
           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) ≃ (proj₁ p ≡ proj₁ q)
+        → (p ≡ q) ≃ (fst p ≡ fst q)
       lem2 pA p q = fromIsomorphism iso
         where
-        f : ∀ {p q} → p ≡ q → proj₁ p ≡ proj₁ q
-        f e i = proj₁ (e i)
-        g : ∀ {p q} → proj₁ p ≡ proj₁ q → p ≡ q
+        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 .proj₁ , propSet (pA (p .proj₁)) (p .proj₂) (p .proj₂) (λ i → (g {p} {p} ∘ f) (λ i₁ → p) i .proj₂) (λ i → p .proj₂) i j ) q
-        re-ve : (e : proj₁ p ≡ proj₁ q) → (f {p} {q} ∘ g {p} {q}) 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 = record
           { verso-recto = funExt ve-re
           ; recto-verso = funExt re-ve
           }
-        iso : (p ≡ q) Eqv.≅ (proj₁ p ≡ proj₁ q)
+        iso : (p ≡ q) Eqv.≅ (fst p ≡ fst q)
         iso = f , g , inv
 
       lem3 : ∀ {ℓc} {Q : A → Set (ℓc ⊔ ℓb)}
@@ -119,37 +118,37 @@ module _ (ℓ : Level) where
           where
           k : Eqv.Isomorphism _
           k = Equiv≃.toIso _ _ (_≃_.isEqv (eA a))
-          open Σ k renaming (proj₁ to g')
+          open Σ k renaming (fst to g')
         ve-re : (x : Σ A P) → (g ∘ f) x ≡ x
-        ve-re x i = proj₁ x , eq i
+        ve-re x i = fst x , eq i
           where
-          eq : proj₂ ((g ∘ f) x) ≡ proj₂ x
+          eq : snd ((g ∘ f) x) ≡ snd x
           eq = begin
-            proj₂ ((g ∘ f) x) ≡⟨⟩
-            proj₂ (g (f (a , pA))) ≡⟨⟩
+            snd ((g ∘ f) x) ≡⟨⟩
+            snd (g (f (a , pA))) ≡⟨⟩
             g' (_≃_.eqv (eA a) pA) ≡⟨ lem ⟩
             pA ∎
             where
-            open Σ x renaming (proj₁ to a ; proj₂ to pA)
+            open Σ x renaming (fst to a ; snd to pA)
             k : Eqv.Isomorphism _
             k = Equiv≃.toIso _ _ (_≃_.isEqv (eA a))
-            open Σ k renaming (proj₁ to g' ; proj₂ to inv)
+            open Σ k renaming (fst to g' ; snd to inv)
             module A = AreInverses inv
             -- anti-funExt
             lem : (g' ∘ (_≃_.eqv (eA a))) pA ≡ pA
             lem i = A.verso-recto i pA
         re-ve : (x : Σ A Q) → (f ∘ g) x ≡ x
-        re-ve x i = proj₁ x , eq i
+        re-ve x i = fst x , eq i
           where
-          open Σ x renaming (proj₁ to a ; proj₂ to qA)
+          open Σ x renaming (fst to a ; snd to qA)
           eq = begin
-            proj₂ ((f ∘ g) x)                 ≡⟨⟩
+            snd ((f ∘ g) x)                 ≡⟨⟩
             _≃_.eqv (eA a) (g' qA)            ≡⟨ (λ i → A.recto-verso i qA) ⟩
             qA                                ∎
             where
             k : Eqv.Isomorphism _
             k = Equiv≃.toIso _ _ (_≃_.isEqv (eA a))
-            open Σ k renaming (proj₁ to g' ; proj₂ to inv)
+            open Σ k renaming (fst to g' ; snd to inv)
             module A = AreInverses inv
         inv : AreInverses f g
         inv = record
@@ -183,8 +182,8 @@ module _ (ℓ : Level) where
         in fromIsomorphism iso
 
     module _ {hA hB : Object} where
-      open Σ hA renaming (proj₁ to A ; proj₂ to sA)
-      open Σ hB renaming (proj₁ to B ; proj₂ to sB)
+      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) isIso ≃ Σ (A → B) (isEquiv A B)
@@ -236,7 +235,7 @@ module _ (ℓ : Level) where
       univ≃ = trivial? ⊙ step0 ⊙ step1 ⊙ step2
 
     module _ (hA : Object) where
-      open Σ hA renaming (proj₁ to A)
+      open Σ hA renaming (fst to A)
 
       eq1 : (Σ[ hB ∈ Object ] hA ≅ hB) ≡ (Σ[ hB ∈ Object ] hA ≡ hB)
       eq1 = ua (lem3 (\ hB → univ≃))
@@ -245,7 +244,7 @@ module _ (ℓ : Level) where
       univalent[Contr] = subst {P = isContr} (sym eq1) tres
         where
         module _ (y : Σ[ hB ∈ Object ] hA ≡ hB) where
-          open Σ y renaming (proj₁ to hB ; proj₂ to hA≡hB)
+          open Σ y renaming (fst to hB ; snd to hA≡hB)
           qres : (hA , refl) ≡ (hB , hA≡hB)
           qres = contrSingl hA≡hB
 
@@ -273,8 +272,8 @@ module _ {ℓ : Level} where
     open import Cubical.Sigma
 
     module _ (hA hB : Object) where
-      open Σ hA renaming (proj₁ to A ; proj₂ to sA)
-      open Σ hB renaming (proj₁ to B ; proj₂ to sB)
+      open Σ hA renaming (fst to A ; snd to sA)
+      open Σ hB renaming (fst to B ; snd to sB)
 
       private
         productObject : Object
@@ -285,30 +284,30 @@ module _ {ℓ : Level} where
           _&&&_ x = f x , g x
 
         module _ (hX : Object) where
-          open Σ hX renaming (proj₁ to X)
+          open Σ hX renaming (fst to X)
           module _ (f : X → A ) (g : X → B) where
-            ump : proj₁ Function.∘′ (f &&& g) ≡ f × proj₂ Function.∘′ (f &&& g) ≡ g
-            proj₁ ump = refl
-            proj₂ ump = refl
+            ump : fst Function.∘′ (f &&& g) ≡ f × snd Function.∘′ (f &&& g) ≡ g
+            fst ump = refl
+            snd ump = refl
 
         rawProduct : RawProduct 𝓢 hA hB
         RawProduct.object rawProduct = productObject
-        RawProduct.proj₁  rawProduct = Data.Product.proj₁
-        RawProduct.proj₂  rawProduct = Data.Product.proj₂
+        RawProduct.fst    rawProduct = fst
+        RawProduct.snd    rawProduct = snd
 
         isProduct : IsProduct 𝓢 _ _ rawProduct
         IsProduct.ump isProduct {X = hX} f g
           = f &&& g , ump hX f g , λ eq → funExt (umpUniq eq)
           where
-          open Σ hX renaming (proj₁ to X) using ()
-          module _ {y : X → A × B} (eq : proj₁ Function.∘′ y ≡ f × proj₂ Function.∘′ y ≡ g) (x : X) where
-            p1 : proj₁ ((f &&& g) x) ≡ proj₁ (y x)
+          open Σ hX renaming (fst to X) using ()
+          module _ {y : X → A × B} (eq : fst Function.∘′ y ≡ f × snd Function.∘′ y ≡ g) (x : X) where
+            p1 : fst ((f &&& g) x) ≡ fst (y x)
             p1 = begin
-              proj₁ ((f &&& g) x) ≡⟨⟩
-              f x ≡⟨ (λ i → sym (proj₁ eq) i x) ⟩
-              proj₁ (y x) ∎
-            p2 : proj₂ ((f &&& g) x) ≡ proj₂ (y x)
-            p2 = λ i → sym (proj₂ eq) i x
+              fst ((f &&& g) x) ≡⟨⟩
+              f x ≡⟨ (λ i → sym (fst eq) i x) ⟩
+              fst (y x) ∎
+            p2 : snd ((f &&& g) x) ≡ snd (y x)
+            p2 = λ i → sym (snd eq) i x
             umpUniq : (f &&& g) x ≡ y x
             umpUniq i = p1 i , p2 i
 
diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 5c497b9..a847eb9 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -29,12 +29,8 @@
 module Cat.Category where
 
 open import Cat.Prelude
-  renaming
-  ( proj₁ to fst
-  ; proj₂ to snd
-  )
 
-import      Function
+import Function
 
 ------------------
 -- * Categories --
@@ -136,10 +132,10 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
           -- It may be that we need something weaker than this, in that there
           -- may be some other lemmas available to us.
           -- For instance, `need0` should be available to us when we prove `need1`.
-          (need0 : (s : Σ Object (A ≅_)) → (open Σ s renaming (proj₁ to Y) using ()) → A ≡ Y)
+          (need0 : (s : Σ Object (A ≅_)) → (open Σ s renaming (fst to Y) using ()) → A ≡ Y)
           (need2 : (iso : A ≅ A)
-            → (open Σ iso   renaming (proj₁ to f  ; proj₂ to iso-f))
-            → (open Σ iso-f renaming (proj₁ to f~ ; proj₂ to areInv))
+            → (open Σ iso   renaming (fst to f  ; snd to iso-f))
+            → (open Σ iso-f renaming (fst to f~ ; snd to areInv))
             → (identity , identity) ≡ (f , f~)
           ) where
 
@@ -147,7 +143,7 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
         c = A , idIso A
 
         module _ (y : Σ Object (A ≅_)) where
-          open Σ y renaming (proj₁ to Y ; proj₂ to isoY)
+          open Σ y renaming (fst to Y ; snd to isoY)
           q : A ≡ Y
           q = need0 y
 
@@ -163,8 +159,8 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
             d  : D A refl
             d A≅Y i = a0 i , a1 i , a2 i
               where
-              open Σ A≅Y   renaming (proj₁ to f  ; proj₂ to iso-f)
-              open Σ iso-f renaming (proj₁ to f~ ; proj₂ to areInv)
+              open Σ A≅Y   renaming (fst to f  ; snd to iso-f)
+              open Σ iso-f renaming (fst to f~ ; snd to areInv)
               aaa : (identity , identity) ≡ (f , f~)
               aaa = need2 A≅Y
               a0 : identity ≡ f
@@ -309,8 +305,8 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
     propIsTerminal T x y i {X} = res X i
       where
       module _ (X : Object) where
-        open Σ (x {X}) renaming (proj₁ to fx ; proj₂ to cx)
-        open Σ (y {X}) renaming (proj₁ to fy ; proj₂ to cy)
+        open Σ (x {X}) renaming (fst to fx ; snd to cx)
+        open Σ (y {X}) renaming (fst to fy ; snd to cy)
         fp : fx ≡ fy
         fp = cx fy
         prop : (x : Arrow X T) → isProp (∀ f → x ≡ f)
@@ -328,10 +324,10 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
     propTerminal : isProp Terminal
     propTerminal Xt Yt = res
       where
-      open Σ Xt renaming (proj₁ to X ; proj₂ to Xit)
-      open Σ Yt renaming (proj₁ to Y ; proj₂ to Yit)
-      open Σ (Xit {Y}) renaming (proj₁ to Y→X) using ()
-      open Σ (Yit {X}) renaming (proj₁ to X→Y) using ()
+      open Σ Xt renaming (fst to X ; snd to Xit)
+      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
@@ -361,8 +357,8 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
     propIsInitial I x y i {X} = res X i
       where
       module _ (X : Object) where
-        open Σ (x {X}) renaming (proj₁ to fx ; proj₂ to cx)
-        open Σ (y {X}) renaming (proj₁ to fy ; proj₂ to cy)
+        open Σ (x {X}) renaming (fst to fx ; snd to cx)
+        open Σ (y {X}) renaming (fst to fy ; snd to cy)
         fp : fx ≡ fy
         fp = cx fy
         prop : (x : Arrow I X) → isProp (∀ f → x ≡ f)
@@ -375,10 +371,10 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
     propInitial : isProp Initial
     propInitial Xi Yi = res
       where
-      open Σ Xi renaming (proj₁ to X ; proj₂ to Xii)
-      open Σ Yi renaming (proj₁ to Y ; proj₂ to Yii)
-      open Σ (Xii {Y}) renaming (proj₁ to Y→X) using ()
-      open Σ (Yii {X}) renaming (proj₁ to X→Y) using ()
+      open Σ Xi renaming (fst to X ; snd to Xii)
+      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
@@ -508,7 +504,7 @@ module Opposite {ℓa ℓb : Level} where
         open import Cat.Equivalence as Equivalence hiding (_≅_)
         k : Equivalence.Isomorphism (ℂ.id-to-iso A B)
         k = Equiv≃.toIso _ _ ℂ.univalent
-        open Σ k renaming (proj₁ to f ; proj₂ to inv)
+        open Σ k renaming (fst to f ; snd to inv)
         open AreInverses inv
 
         _⊙_ = Function._∘_
@@ -531,12 +527,12 @@ module Opposite {ℓa ℓb : Level} where
           where
           l = id-to-iso A B p
           r = flopDem (ℂ.id-to-iso A B p)
-          open Σ l renaming (proj₁ to l-obv ; proj₂ to l-areInv)
-          open Σ l-areInv renaming (proj₁ to l-invs ; proj₂ to l-iso)
-          open Σ l-iso renaming (proj₁ to l-l ; proj₂ to l-r)
-          open Σ r renaming (proj₁ to r-obv ; proj₂ to r-areInv)
-          open Σ r-areInv renaming (proj₁ to r-invs ; proj₂ to r-iso)
-          open Σ r-iso renaming (proj₁ to r-l ; proj₂ to r-r)
+          open Σ l renaming (fst to l-obv ; snd to l-areInv)
+          open Σ l-areInv renaming (fst to l-invs ; snd to l-iso)
+          open Σ l-iso renaming (fst to l-l ; snd to l-r)
+          open Σ r renaming (fst to r-obv ; snd to r-areInv)
+          open Σ r-areInv renaming (fst to r-invs ; snd to r-iso)
+          open Σ r-iso renaming (fst to r-l ; snd to r-r)
           l-obv≡r-obv : l-obv ≡ r-obv
           l-obv≡r-obv = refl
           l-invs≡r-invs : l-invs ≡ r-invs
diff --git a/src/Cat/Category/Exponential.agda b/src/Cat/Category/Exponential.agda
index 4b4f017..46aa1c0 100644
--- a/src/Cat/Category/Exponential.agda
+++ b/src/Cat/Category/Exponential.agda
@@ -30,7 +30,7 @@ module _ {ℓ ℓ'} (ℂ : Category ℓ ℓ') {{hasProducts : HasProducts ℂ}}
         {{isExponential}} : IsExponential obj eval
 
       transpose : (A : Object) → ℂ [ A × B , C ] → ℂ [ A , obj ]
-      transpose A f = proj₁ (isExponential A f)
+      transpose A f = fst (isExponential A f)
 
 record HasExponentials {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') {{_ : HasProducts ℂ}} : Set (ℓ ⊔ ℓ') where
   open Category ℂ
diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda
index 6383ab0..5b3c657 100644
--- a/src/Cat/Category/Monad.agda
+++ b/src/Cat/Category/Monad.agda
@@ -52,7 +52,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
       private
         module MI = M.IsMonad m
       forthIsMonad : K.IsMonad (forthRaw raw)
-      K.IsMonad.isIdentity     forthIsMonad = proj₂ MI.isInverse
+      K.IsMonad.isIdentity     forthIsMonad = snd MI.isInverse
       K.IsMonad.isNatural      forthIsMonad = MI.isNatural
       K.IsMonad.isDistributive forthIsMonad = MI.isDistributive
 
@@ -83,11 +83,11 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
         where
         inv-l = begin
           joinT X ∘ pureT (R.omap X) ≡⟨⟩
-          join ∘ pure                 ≡⟨ proj₁ isInverse ⟩
+          join ∘ pure                 ≡⟨ fst isInverse ⟩
           identity                    ∎
         inv-r = begin
           joinT X ∘ R.fmap (pureT X) ≡⟨⟩
-          join ∘ fmap pure            ≡⟨ proj₂ isInverse ⟩
+          join ∘ fmap pure            ≡⟨ snd isInverse ⟩
           identity                    ∎
 
     back : K.Monad → M.Monad
@@ -160,7 +160,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
              Rfmap (f >>> pureT B) >>> joinT B     ≡⟨⟩
           Rfmap (f >>> pureT B) >>> joinT B        ≡⟨ cong (λ φ → φ >>> joinT B) R.isDistributive ⟩
           Rfmap f >>> Rfmap (pureT B) >>> joinT B  ≡⟨ ℂ.isAssociative ⟩
-          joinT B ∘ Rfmap (pureT B) ∘ Rfmap f      ≡⟨ cong (λ φ → φ ∘ Rfmap f) (proj₂ isInverse) ⟩
+          joinT B ∘ Rfmap (pureT B) ∘ Rfmap f      ≡⟨ cong (λ φ → φ ∘ Rfmap f) (snd isInverse) ⟩
           identity ∘ Rfmap f                       ≡⟨ ℂ.leftIdentity ⟩
           Rfmap f                                  ∎
           )
diff --git a/src/Cat/Category/Monad/Kleisli.agda b/src/Cat/Category/Monad/Kleisli.agda
index dc40f1c..1faf079 100644
--- a/src/Cat/Category/Monad/Kleisli.agda
+++ b/src/Cat/Category/Monad/Kleisli.agda
@@ -165,12 +165,12 @@ record IsMonad (raw : RawMonad) : Set ℓ where
       R.fmap f  ∘ join        ∎
 
   pureNT : NaturalTransformation R⁰ R
-  proj₁ pureNT = pureT
-  proj₂ pureNT = pureN
+  fst pureNT = pureT
+  snd pureNT = pureN
 
   joinNT : NaturalTransformation R² R
-  proj₁ joinNT = joinT
-  proj₂ joinNT = joinN
+  fst joinNT = joinT
+  snd joinNT = joinN
 
   isNaturalForeign : IsNaturalForeign
   isNaturalForeign = begin
diff --git a/src/Cat/Category/Monad/Monoidal.agda b/src/Cat/Category/Monad/Monoidal.agda
index 56319c2..707ea07 100644
--- a/src/Cat/Category/Monad/Monoidal.agda
+++ b/src/Cat/Category/Monad/Monoidal.agda
@@ -29,14 +29,14 @@ record RawMonad : Set ℓ where
   -- Note that `pureT` and `joinT` differs from their definition in the
   -- kleisli formulation only by having an explicit parameter.
   pureT : Transformation Functors.identity R
-  pureT = proj₁ pureNT
+  pureT = fst pureNT
   pureN : Natural Functors.identity R pureT
-  pureN = proj₂ pureNT
+  pureN = snd pureNT
 
   joinT : Transformation F[ R ∘ R ] R
-  joinT = proj₁ joinNT
+  joinT = fst joinNT
   joinN : Natural F[ R ∘ R ] R joinT
-  joinN = proj₂ joinNT
+  joinN = snd joinNT
 
   Romap = Functor.omap R
   Rfmap = Functor.fmap R
@@ -71,7 +71,7 @@ record IsMonad (raw : RawMonad) : Set ℓ where
     joinT Y ∘ R.fmap f ∘ pureT X     ≡⟨ sym ℂ.isAssociative ⟩
     joinT Y ∘ (R.fmap f ∘ pureT X)   ≡⟨ cong (λ φ → joinT Y ∘ φ) (sym (pureN f)) ⟩
     joinT Y ∘ (pureT (R.omap Y) ∘ f) ≡⟨ ℂ.isAssociative ⟩
-    joinT Y ∘ pureT (R.omap Y) ∘ f   ≡⟨ cong (λ φ → φ ∘ f) (proj₁ isInverse) ⟩
+    joinT Y ∘ pureT (R.omap Y) ∘ f   ≡⟨ cong (λ φ → φ ∘ f) (fst isInverse) ⟩
     identity ∘ f                     ≡⟨ ℂ.leftIdentity ⟩
     f                                ∎
 
@@ -129,8 +129,8 @@ private
       where
       xX = x {X}
       yX = y {X}
-      e1 = Category.arrowsAreSets ℂ _ _ (proj₁ xX) (proj₁ yX)
-      e2 = Category.arrowsAreSets ℂ _ _ (proj₂ xX) (proj₂ yX)
+      e1 = Category.arrowsAreSets ℂ _ _ (fst xX) (fst yX)
+      e2 = Category.arrowsAreSets ℂ _ _ (snd xX) (snd yX)
 
   open IsMonad
   propIsMonad : (raw : _) → isProp (IsMonad raw)
diff --git a/src/Cat/Category/Monad/Voevodsky.agda b/src/Cat/Category/Monad/Voevodsky.agda
index 6563cb8..3c6bad6 100644
--- a/src/Cat/Category/Monad/Voevodsky.agda
+++ b/src/Cat/Category/Monad/Voevodsky.agda
@@ -124,7 +124,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 (Monoidal≅Kleisli ℂ .proj₂ .proj₂)
+      module E = AreInverses (Monoidal≅Kleisli ℂ .snd .snd)
 
       Monoidal→Kleisli : M.Monad → K.Monad
       Monoidal→Kleisli = E.obverse
diff --git a/src/Cat/Category/NaturalTransformation.agda b/src/Cat/Category/NaturalTransformation.agda
index 0b4d784..01eff6d 100644
--- a/src/Cat/Category/NaturalTransformation.agda
+++ b/src/Cat/Category/NaturalTransformation.agda
@@ -58,7 +58,7 @@ module _ (F G : Functor ℂ 𝔻) where
   propIsNatural θ x y i {A} {B} f = 𝔻.arrowsAreSets _ _ (x f) (y f) i
 
   NaturalTransformation≡ : {α β : NaturalTransformation}
-    → (eq₁ : α .proj₁ ≡ β .proj₁)
+    → (eq₁ : α .fst ≡ β .fst)
     → α ≡ β
   NaturalTransformation≡ eq = lemSig propIsNatural _ _ eq
 
@@ -88,8 +88,8 @@ module _ {F G H : Functor ℂ 𝔻} where
   T[ θ ∘ η ] C = 𝔻 [ θ C ∘ η C ]
 
   NT[_∘_] : NaturalTransformation G H → NaturalTransformation F G → NaturalTransformation F H
-  proj₁ NT[ (θ , _) ∘ (η , _) ] = T[ θ ∘ η ]
-  proj₂ NT[ (θ , θNat) ∘ (η , ηNat) ] {A} {B} f = begin
+  fst NT[ (θ , _) ∘ (η , _) ] = T[ θ ∘ η ]
+  snd NT[ (θ , θNat) ∘ (η , ηNat) ] {A} {B} f = begin
     𝔻 [ T[ θ ∘ η ] B ∘ F.fmap f ]     ≡⟨⟩
     𝔻 [ 𝔻 [ θ B ∘ η B ] ∘ F.fmap f ] ≡⟨ sym 𝔻.isAssociative ⟩
     𝔻 [ θ B ∘ 𝔻 [ η B ∘ F.fmap f ] ] ≡⟨ cong (λ φ → 𝔻 [ θ B ∘ φ ]) (ηNat f) ⟩
diff --git a/src/Cat/Category/Product.agda b/src/Cat/Category/Product.agda
index 44fb0ef..ac5ac14 100644
--- a/src/Cat/Category/Product.agda
+++ b/src/Cat/Category/Product.agda
@@ -2,8 +2,8 @@
 module Cat.Category.Product where
 
 open import Cubical.NType.Properties
-open import Cat.Prelude hiding (_×_ ; proj₁ ; proj₂)
-import Data.Product as P
+open import Cat.Prelude as P hiding (_×_ ; fst ; snd)
+-- module P = Cat.Prelude
 
 open import Cat.Category
 
@@ -16,8 +16,8 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
       no-eta-equality
       field
         object : Object
-        proj₁  : ℂ [ object , A ]
-        proj₂  : ℂ [ object , B ]
+        fst  : ℂ [ object , A ]
+        snd  : ℂ [ object , B ]
 
     -- FIXME Not sure this is actually a proposition - so this name is
     -- misleading.
@@ -25,12 +25,12 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
       open RawProduct raw public
       field
         ump : ∀ {X : Object} (f : ℂ [ X , A ]) (g : ℂ [ X , B ])
-          → ∃![ f×g ] (ℂ [ proj₁ ∘ f×g ] ≡ f P.× ℂ [ proj₂ ∘ f×g ] ≡ g)
+          → ∃![ f×g ] (ℂ [ fst ∘ f×g ] ≡ f P.× ℂ [ snd ∘ f×g ] ≡ g)
 
       -- | Arrow product
       _P[_×_] : ∀ {X} → (π₁ : ℂ [ X , A ]) (π₂ : ℂ [ X , B ])
         → ℂ [ X , object ]
-      _P[_×_] π₁ π₂ = P.proj₁ (ump π₁ π₂)
+      _P[_×_] π₁ π₂ = P.fst (ump π₁ π₂)
 
     record Product : Set (ℓa ⊔ ℓb) where
       field
@@ -51,8 +51,8 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
     -- The product mentioned in awodey in Def 6.1 is not the regular product of
     -- arrows. It's a "parallel" product
     module _ {A A' B B' : Object} where
-      open Product
-      open Product (product A B) hiding (_P[_×_]) renaming (proj₁ to fst ; proj₂ to snd)
+      open Product using (_P[_×_])
+      open Product (product A B) hiding (_P[_×_]) renaming (fst to fst ; snd to snd)
       _|×|_ : ℂ [ A , A' ] → ℂ [ B , B' ] → ℂ [ A × B , A' × B' ]
       f |×| g = product A' B'
         P[ ℂ [ f ∘ fst ]
@@ -70,7 +70,7 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} {A B : Category.Object 
 
         module _ {X : Object} (f : ℂ [ X , A ]) (g : ℂ [ X , B ]) where
           module _ (f×g : Arrow X y.object) where
-            help : isProp (∀{y} → (ℂ [ y.proj₁ ∘ y ] ≡ f) P.× (ℂ [ y.proj₂ ∘ y ] ≡ g) → f×g ≡ y)
+            help : isProp (∀{y} → (ℂ [ y.fst ∘ y ] ≡ f) P.× (ℂ [ y.snd ∘ y ] ≡ g) → f×g ≡ y)
             help = propPiImpl (λ _ → propPi (λ _ → arrowsAreSets _ _))
 
           res = ∃-unique (x.ump f g) (y.ump f g)
@@ -93,7 +93,7 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} {A B : Category.Object 
 module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
   (let module ℂ = Category ℂ) {A B : ℂ.Object} where
 
-  open import Data.Product
+  open P
 
   module _ where
     raw : RawCategory _ _
@@ -130,12 +130,12 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
 
     isAssocitaive : IsAssociative
     isAssocitaive {A'@(A , a0 , a1)} {B , _} {C , c0 , c1} {D'@(D , d0 , d1)} {ff@(f , f0 , f1)} {gg@(g , g0 , g1)} {hh@(h , h0 , h1)} i
-      = s0 i , lemPropF propEqs s0 {proj₂ l} {proj₂ r} i
+      = s0 i , lemPropF propEqs s0 {P.snd l} {P.snd r} i
       where
       l = hh ∘ (gg ∘ ff)
       r = hh ∘ gg ∘ ff
       -- s0 : h ℂ.∘ (g ℂ.∘ f) ≡ h ℂ.∘ g ℂ.∘ f
-      s0 : proj₁ l ≡ proj₁ r
+      s0 : fst l ≡ fst r
       s0 = ℂ.isAssociative {f = f} {g} {h}
 
 
@@ -143,15 +143,15 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
     isIdentity {AA@(A , a0 , a1)} {BB@(B , b0 , b1)} {f , f0 , f1} = leftIdentity , rightIdentity
       where
       leftIdentity : identity ∘ (f , f0 , f1) ≡ (f , f0 , f1)
-      leftIdentity i = l i , lemPropF propEqs l {proj₂ L} {proj₂ R} i
+      leftIdentity i = l i , lemPropF propEqs l {snd L} {snd R} i
         where
         L = identity ∘ (f , f0 , f1)
         R : Arrow AA BB
         R = f , f0 , f1
-        l : proj₁ L ≡ proj₁ R
+        l : fst L ≡ fst R
         l = ℂ.leftIdentity
       rightIdentity : (f , f0 , f1) ∘ identity ≡ (f , f0 , f1)
-      rightIdentity i = l i , lemPropF propEqs l {proj₂ L} {proj₂ R} i
+      rightIdentity i = l i , lemPropF propEqs l {snd L} {snd R} i
         where
         L = (f , f0 , f1) ∘ identity
         R : Arrow AA BB
@@ -165,29 +165,50 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
 
     open Univalence isIdentity
 
-    module _ (A : Object) where
-      c : Σ Object (A ≅_)
-      c = A , {!!}
-      univalent[Contr] : isContr (Σ Object (A ≅_))
-      univalent[Contr] = {!!} , {!!}
+    -- module _ (X : Object) where
+    --   center : Σ Object (X ≅_)
+    --   center = X , idIso X
+
+    --   module _ (y : Σ Object (X ≅_)) where
+    --     open Σ y renaming (fst to Y ; snd to X≅Y)
+
+    --     contractible : (X , idIso X) ≡ (Y , X≅Y)
+    --     contractible = {!!}
+
+    --   univalent[Contr] : isContr (Σ Object (X ≅_))
+    --   univalent[Contr] = center , contractible
+    --   module _ (y : Σ Object (X ≡_)) where
+    --     open Σ y renaming (fst to Y ; snd to p)
+    --     a0 : X ≡ Y
+    --     a0 = {!!}
+    --     a1 : PathP (λ i → X ≡ a0 i) refl p
+    --     a1 = {!!}
+    --       where
+    --       P : (Z : Object) → X ≡ Z → Set _
+    --       P Z p = PathP (λ i → X ≡ Z)
+
+    --     alt' : (X , refl) ≡ y
+    --     alt' i = a0 i , a1 i
+    --   alt : isContr (Σ Object (X ≡_))
+    --   alt = (X , refl) , alt'
 
     univalent' : Univalent[Contr]
     univalent' = univalence-lemma p q
       where
       module _ {𝕏 : Object} where
-        open Σ 𝕏    renaming (proj₁ to X ; proj₂ to x0x1)
-        open Σ x0x1 renaming (proj₁ to x0 ; proj₂ to x1)
+        open Σ 𝕏    renaming (fst to X ; snd to x0x1)
+        open Σ x0x1 renaming (fst to x0 ; snd to x1)
         -- x0 : X → A in ℂ
         -- x1 : X → B in ℂ
         module _ (𝕐-isoY : Σ Object (𝕏 ≅_)) where
-          open Σ 𝕐-isoY  renaming (proj₁ to 𝕐  ; proj₂ to isoY)
-          open Σ 𝕐       renaming (proj₁ to Y  ; proj₂ to y0y1)
-          open Σ y0y1    renaming (proj₁ to y0 ; proj₂ to y1)
-          open Σ isoY    renaming (proj₁ to 𝓯  ; proj₂ to iso-𝓯)
-          open Σ iso-𝓯   renaming (proj₁ to 𝓯~ ; proj₂ to inv-𝓯)
-          open Σ 𝓯       renaming (proj₁ to f  ; proj₂ to inv-f)
-          open Σ 𝓯~      renaming (proj₁ to f~ ; proj₂ to inv-f~)
-          open Σ inv-𝓯   renaming (proj₁ to left ; proj₂ to right)
+          open Σ 𝕐-isoY  renaming (fst to 𝕐  ; snd to isoY)
+          open Σ 𝕐       renaming (fst to Y  ; snd to y0y1)
+          open Σ y0y1    renaming (fst to y0 ; snd to y1)
+          open Σ isoY    renaming (fst to 𝓯  ; snd to iso-𝓯)
+          open Σ iso-𝓯   renaming (fst to 𝓯~ ; snd to inv-𝓯)
+          open Σ 𝓯       renaming (fst to f  ; snd to inv-f)
+          open Σ 𝓯~      renaming (fst to f~ ; snd to inv-f~)
+          open Σ inv-𝓯   renaming (fst to left ; snd to right)
           -- y0 : Y → A in ℂ
           -- y1 : Y → B in ℂ
           -- f  : X → Y in ℂ
@@ -199,24 +220,24 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
             = f
             , f~
             , ( begin
-                ℂ [ f~ ∘ f ] ≡⟨ (λ i → proj₁ (left i)) ⟩
+                ℂ [ f~ ∘ f ] ≡⟨ (λ i → fst (left i)) ⟩
                 ℂ.identity ∎
               )
             , ( begin
-                ℂ [ f ∘ f~ ] ≡⟨ (λ i → proj₁ (right i)) ⟩
+                ℂ [ f ∘ f~ ] ≡⟨ (λ i → fst (right i)) ⟩
                 ℂ.identity ∎
               )
           p0 : X ≡ Y
           p0 = ℂ.iso-to-id isoℂ
           -- I note `left2` and right2` here as a reminder.
           left2 : PathP
-            (λ i → ℂ [ x0 ∘ proj₁ (left i) ] ≡ x0 × ℂ [ x1 ∘ proj₁ (left i) ] ≡ x1)
-            (proj₂ (𝓯~ ∘ 𝓯)) (proj₂ identity)
-          left2 i = proj₂ (left i)
+            (λ i → ℂ [ x0 ∘ fst (left i) ] ≡ x0 × ℂ [ x1 ∘ fst (left i) ] ≡ x1)
+            (snd (𝓯~ ∘ 𝓯)) (snd identity)
+          left2 i = snd (left i)
           right2 : PathP
-            (λ i → ℂ [ y0 ∘ proj₁ (right i) ] ≡ y0 × ℂ [ y1 ∘ proj₁ (right i) ] ≡ y1)
-            (proj₂ (𝓯 ∘ 𝓯~)) (proj₂ identity)
-          right2 i = proj₂ (right i)
+            (λ i → ℂ [ y0 ∘ fst (right i) ] ≡ y0 × ℂ [ y1 ∘ fst (right i) ] ≡ y1)
+            (snd (𝓯 ∘ 𝓯~)) (snd identity)
+          right2 i = snd (right i)
           -- My idea:
           --
           -- x0, x1 and y0 and y1 are product arrows as in the diagram
@@ -245,23 +266,23 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
           p : (X , x0x1) ≡ (Y , y0y1)
           p i = p0 i , {!!}
         module _ (iso : 𝕏 ≅ 𝕏) where
-          open Σ iso renaming (proj₁ to 𝓯 ; proj₂ to inv-𝓯)
-          open Σ inv-𝓯 renaming (proj₁ to 𝓯~) using ()
-          open Σ 𝓯  renaming (proj₁ to f  ; proj₂ to inv-f)
-          open Σ 𝓯~ renaming (proj₁ to f~ ; proj₂ to inv-f~)
+          open Σ iso renaming (fst to 𝓯 ; snd to inv-𝓯)
+          open Σ inv-𝓯 renaming (fst to 𝓯~) using ()
+          open Σ 𝓯  renaming (fst to f  ; snd to inv-f)
+          open Σ 𝓯~ renaming (fst to f~ ; snd to inv-f~)
           q0' : ℂ.identity ≡ f
           q0' i = {!!}
           prop : ∀ x → isProp (ℂ [ x0 ∘ x ] ≡ x0 × ℂ [ x1 ∘ x ] ≡ x1)
           prop x = propSig
             (      ℂ.arrowsAreSets (ℂ [ x0 ∘ x ]) x0)
             (λ _ → ℂ.arrowsAreSets (ℂ [ x1 ∘ x ]) x1)
-          q0'' : PathP (λ i → ℂ [ x0 ∘ q0' i ] ≡ x0 × ℂ [ x1 ∘ q0' i ] ≡ x1) (proj₂ identity) inv-f
+          q0'' : PathP (λ i → ℂ [ x0 ∘ q0' i ] ≡ x0 × ℂ [ x1 ∘ q0' i ] ≡ x1) (snd identity) inv-f
           q0'' = lemPropF prop q0'
           q0 : identity ≡ 𝓯
           q0 i = q0' i , q0'' i
           q1' : ℂ.identity ≡ f~
           q1' = {!!}
-          q1'' : PathP (λ i → (ℂ [ x0 ∘ q1' i ]) ≡ x0 × (ℂ [ x1 ∘ q1' i ]) ≡ x1) (proj₂ identity) inv-f~
+          q1'' : PathP (λ i → (ℂ [ x0 ∘ q1' i ]) ≡ x0 × (ℂ [ x1 ∘ q1' i ]) ≡ x1) (snd identity) inv-f~
           q1'' = lemPropF prop q1'
           q1 : identity ≡ 𝓯~
           q1 i = q1' i , {!!}
@@ -275,11 +296,11 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
       open import Cubical.Univalence
       module _ (c : (X , x) ≅ (Y , y)) where
       -- module _ (c : _ ≅ _) where
-        open Σ c renaming (proj₁ to f_c ; proj₂ to inv_c)
-        open Σ inv_c renaming (proj₁ to g_c ; proj₂ to ainv_c)
-        open Σ ainv_c renaming (proj₁ to left ; proj₂ to right)
+        open Σ c renaming (fst to f_c ; snd to inv_c)
+        open Σ inv_c renaming (fst to g_c ; snd to ainv_c)
+        open Σ ainv_c renaming (fst to left ; snd to right)
         c0 : X ℂ.≅ Y
-        c0 = proj₁ f_c , proj₁ g_c , (λ i → proj₁ (left i)) , (λ i → proj₁ (right i))
+        c0 = fst f_c , fst g_c , (λ i → fst (left i)) , (λ i → fst (right i))
         f0 : X ≡ Y
         f0 = ℂ.iso-to-id c0
         module _ {A : ℂ.Object} (α : ℂ.Arrow X A) where
@@ -296,7 +317,7 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
       prp : isSet (ℂ.Object × ℂ.Arrow Y A × ℂ.Arrow Y B)
       prp = setSig {sA = {!!}} {(λ _ → setSig {sA = ℂ.arrowsAreSets} {λ _ → ℂ.arrowsAreSets})}
       ve-re : (p : (X , x) ≡ (Y , y)) → f (id-to-iso _ _ p) ≡ p
-      -- ve-re p i j = {!ℂ.arrowsAreSets!} , ℂ.arrowsAreSets _ _ (let k = proj₁ (proj₂ (p i)) in {!!}) {!!} {!!} {!!} , {!!}
+      -- ve-re p i j = {!ℂ.arrowsAreSets!} , ℂ.arrowsAreSets _ _ (let k = fst (snd (p i)) in {!!}) {!!} {!!} {!!} , {!!}
       ve-re p = let k = prp {!!} {!!} {!!} {!p!} in {!!}
       re-ve : (iso : (X , x) ≅ (Y , y)) → id-to-iso _ _ (f iso) ≡ iso
       re-ve = {!!}
@@ -332,17 +353,17 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
       rawP : RawProduct ℂ A B
       rawP = record
         { object = X
-        ; proj₁ = x0
-        ; proj₂ = x1
+        ; fst = x0
+        ; snd = x1
         }
-      -- open RawProduct rawP renaming (proj₁ to x0 ; proj₂ to x1)
+      -- open RawProduct rawP renaming (fst to x0 ; snd to x1)
       module _ {Y : ℂ.Object} (p0 : ℂ [ Y , A ]) (p1 : ℂ [ Y , B ]) where
         uy : isContr (Arrow (Y , p0 , p1) (X , x0 , x1))
         uy = uniq {Y , p0 , p1}
-        open Σ uy renaming (proj₁ to Y→X ; proj₂ to contractible)
-        open Σ Y→X renaming (proj₁ to p0×p1 ; proj₂ to cond)
+        open Σ uy renaming (fst to Y→X ; snd to contractible)
+        open Σ Y→X renaming (fst to p0×p1 ; snd to cond)
         ump : ∃![ f×g ] (ℂ [ x0 ∘ f×g ] ≡ p0 P.× ℂ [ x1 ∘ f×g ] ≡ p1)
-        ump = p0×p1 , cond , λ {y} x → let k = contractible (y , x) in λ i → proj₁ (k i)
+        ump = p0×p1 , cond , λ {y} x → let k = contractible (y , x) in λ i → fst (k i)
       isP : IsProduct ℂ A B rawP
       isP = record { ump = ump }
       p : Product ℂ A B
@@ -356,31 +377,31 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
       module p = Product p
       module isp = IsProduct p.isProduct
       o : Object
-      o = p.object , p.proj₁ , p.proj₂
+      o = p.object , p.fst , p.snd
       module _ {Xx : Object} where
-        open Σ Xx renaming (proj₁ to X ; proj₂ to x)
+        open Σ Xx renaming (fst to X ; snd to x)
         ℂXo : ℂ [ X , isp.object ]
-        ℂXo = isp._P[_×_] (proj₁ x) (proj₂ x)
-        ump = p.ump (proj₁ x) (proj₂ x)
-        Xoo = proj₁ (proj₂ ump)
+        ℂXo = isp._P[_×_] (fst x) (snd x)
+        ump = p.ump (fst x) (snd x)
+        Xoo = fst (snd ump)
         Xo : Arrow Xx o
         Xo = ℂXo , Xoo
         contractible : ∀ y → Xo ≡ y
         contractible (y , yy) = res
           where
           k : ℂXo ≡ y
-          k = proj₂ (proj₂ ump) (yy)
+          k = snd (snd ump) (yy)
           prp : ∀ a → isProp
-            ( (ℂ [ p.proj₁ ∘ a ] ≡ proj₁ x)
-            × (ℂ [ p.proj₂ ∘ a ] ≡ proj₂ x)
+            ( (ℂ [ p.fst ∘ a ] ≡ fst x)
+            × (ℂ [ p.snd ∘ a ] ≡ snd x)
             )
           prp ab ac ad i
-            = ℂ.arrowsAreSets _ _ (proj₁ ac) (proj₁ ad) i
-            , ℂ.arrowsAreSets _ _ (proj₂ ac) (proj₂ ad) i
+            = ℂ.arrowsAreSets _ _ (fst ac) (fst ad) i
+            , ℂ.arrowsAreSets _ _ (snd ac) (snd ad) i
           h :
             ( λ i
-              → ℂ [ p.proj₁ ∘ k i ] ≡ proj₁ x
-              × ℂ [ p.proj₂ ∘ k i ] ≡ proj₂ x
+              → ℂ [ p.fst ∘ k i ] ≡ fst x
+              × ℂ [ p.snd ∘ k i ] ≡ snd x
             ) [ Xoo ≡ yy ]
           h = lemPropF prp k
           res : (ℂXo , Xoo) ≡ (y , yy)
@@ -396,8 +417,8 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
       -- RawProduct does not have eta-equality.
       e : Product.raw (f (g p)) ≡ Product.raw p
       RawProduct.object (e i) = p.object
-      RawProduct.proj₁ (e i) = p.proj₁
-      RawProduct.proj₂ (e i) = p.proj₂
+      RawProduct.fst (e i) = p.fst
+      RawProduct.snd (e i) = p.snd
     inv : AreInverses f g
     inv = record
       { verso-recto = funExt ve-re
diff --git a/src/Cat/Prelude.agda b/src/Cat/Prelude.agda
index 370b300..7a239d5 100644
--- a/src/Cat/Prelude.agda
+++ b/src/Cat/Prelude.agda
@@ -3,10 +3,11 @@ module Cat.Prelude where
 
 open import Agda.Primitive public
 -- FIXME Use:
--- open import Agda.Builtin.Sigma public
+open import Agda.Builtin.Sigma public
 -- Rather than
 open import Data.Product public
   renaming (∃! to ∃!≈)
+  using (_×_ ; Σ-syntax ; swap)
 
 -- TODO Import Data.Function under appropriate names.
 
@@ -46,7 +47,7 @@ module _ (ℓ : Level) where
 -- * Utilities --
 -----------------
 
--- | Unique existensials.
+-- | Unique existentials.
 ∃! : ∀ {a b} {A : Set a}
   → (A → Set b) → Set (a ⊔ b)
 ∃! = ∃!≈ _≡_
@@ -57,15 +58,15 @@ module _ (ℓ : Level) where
 syntax ∃!-syntax (λ x → B) = ∃![ x ] B
 
 module _ {ℓa ℓb} {A : Set ℓa} {P : A → Set ℓb} (f g : ∃! P) where
-  open Σ (proj₂ f) renaming (proj₂ to u)
+  open Σ (snd f) renaming (snd to u)
 
-  ∃-unique : proj₁ f ≡ proj₁ g
-  ∃-unique = u (proj₁ (proj₂ g))
+  ∃-unique : fst f ≡ fst g
+  ∃-unique = u (fst (snd g))
 
 module _ {ℓa ℓb : Level} {A : Set ℓa} {B : A → Set ℓb} {a b : Σ A B}
-  (proj₁≡ : (λ _ → A)            [ proj₁ a ≡ proj₁ b ])
-  (proj₂≡ : (λ i → B (proj₁≡ i)) [ proj₂ a ≡ proj₂ b ]) where
+  (fst≡ : (λ _ → A)            [ fst a ≡ fst b ])
+  (snd≡ : (λ i → B (fst≡ i)) [ snd a ≡ snd b ]) where
 
   Σ≡ : a ≡ b
-  proj₁ (Σ≡ i) = proj₁≡ i
-  proj₂ (Σ≡ i) = proj₂≡ i
+  fst (Σ≡ i) = fst≡ i
+  snd (Σ≡ i) = snd≡ i