diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda
index 97afcd4..31d6926 100644
--- a/src/Cat/Categories/Sets.agda
+++ b/src/Cat/Categories/Sets.agda
@@ -129,7 +129,7 @@ module _ (ℓ : Level) where
       univ≃ = step2 ⊙ univalence ⊙ step0
 
     univalent : Univalent
-    univalent = from[Andrea] (λ _ _ → univ≃)
+    univalent = univalenceFrom≃ univ≃
 
     SetsIsCategory : IsCategory SetsRaw
     IsCategory.isPreCategory SetsIsCategory = isPreCat
diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index aa77c28..3cc5068 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -130,25 +130,23 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
     -- A perhaps more readable version of univalence:
     Univalent≃ = {A B : Object} → (A ≡ B) ≃ (A ≅ B)
 
-    -- | Equivalent formulation of univalence.
-    Univalent[Contr] : Set _
-    Univalent[Contr] = ∀ A → isContr (Σ[ X ∈ Object ] A ≅ X)
+    private
+      -- | Equivalent formulation of univalence.
+      Univalent[Contr] : Set _
+      Univalent[Contr] = ∀ A → isContr (Σ[ X ∈ Object ] A ≅ X)
 
-    Univalent[Andrea] : Set _
-    Univalent[Andrea] = ∀ A B → (A ≡ B) ≃ (A ≅ B)
+      -- From: Thierry Coquand <Thierry.Coquand@cse.gu.se>
+      -- Date: Wed, Mar 21, 2018 at 3:12 PM
+      --
+      -- This is not so straight-forward so you can assume it
+      postulate from[Contr] : Univalent[Contr] → Univalent
 
-    -- From: Thierry Coquand <Thierry.Coquand@cse.gu.se>
-    -- Date: Wed, Mar 21, 2018 at 3:12 PM
-    --
-    -- This is not so straight-forward so you can assume it
-    postulate from[Contr] : Univalent[Contr] → Univalent
-
-    from[Andrea] : Univalent[Andrea] → Univalent
-    from[Andrea] = from[Contr] ∘ step
+    univalenceFrom≃ : Univalent≃ → Univalent
+    univalenceFrom≃ = from[Contr] ∘ step
       where
-      module _ (f : Univalent[Andrea]) (A : Object) where
+      module _ (f : Univalent≃) (A : Object) where
         lem : Σ Object (A ≡_) ≃ Σ Object (A ≅_)
-        lem = equivSig (f A)
+        lem = equivSig λ _ → f
 
         aux : isContr (Σ Object (A ≡_))
         aux = (A , refl) , (λ y → contrSingl (snd y))
diff --git a/src/Cat/Category/Product.agda b/src/Cat/Category/Product.agda
index e08d7c9..0a2ed8b 100644
--- a/src/Cat/Category/Product.agda
+++ b/src/Cat/Category/Product.agda
@@ -171,7 +171,7 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
 
     open IsPreCategory isPreCat
 
-    module _ (𝕏 𝕐 : Object) where
+    module _ {𝕏 𝕐 : Object} where
       open Σ 𝕏 renaming (fst to X ; snd to x)
       open Σ x renaming (fst to xa ; snd to xb)
       open Σ 𝕐 renaming (fst to Y ; snd to y)
@@ -286,7 +286,7 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
       equiv1 = _ , fromIso _ _ (snd iso)
 
     univalent : Univalent
-    univalent = from[Andrea] equiv1
+    univalent = univalenceFrom≃ equiv1
 
     isCat : IsCategory raw
     IsCategory.isPreCategory isCat = isPreCat