diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index e795e3c..24ba6aa 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -152,7 +152,7 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
     univalenceFrom≅ x = univalenceFrom≃ $ fromIsomorphism _ _ x
 
     propUnivalent : isProp Univalent
-    propUnivalent a b i = propPi (λ iso → propIsContr) a b i
+    propUnivalent a b i .equiv-proof = propPi (λ iso → propIsContr) (a .equiv-proof) (b .equiv-proof) i
 
 module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
   record IsPreCategory : Set (lsuc (ℓa ⊔ ℓb)) where
diff --git a/src/Cat/Equivalence.agda b/src/Cat/Equivalence.agda
index 6e55cbf..62ce642 100644
--- a/src/Cat/Equivalence.agda
+++ b/src/Cat/Equivalence.agda
@@ -184,7 +184,7 @@ module _ {ℓa ℓb : Level} (A : Set ℓa) (B : Set ℓb) where
   private
     module _ {obverse : A → B} (e : isEquiv A B obverse) where
       inverse : B → A
-      inverse b = fst (fst (e b))
+      inverse b = fst (fst (e .equiv-proof b))
 
       reverse : B → A
       reverse = inverse
@@ -198,7 +198,7 @@ module _ {ℓa ℓb : Level} (A : Set ℓa) (B : Set ℓb) where
           b ∎
           where
           μ : (b : B) → b ≡ obverse (inverse b)
-          μ b = snd (fst (e b))
+          μ b = snd (fst (e .equiv-proof b))
         verso-recto : ∀ a → (inverse ∘ obverse) a ≡ a
         verso-recto a = begin
           (inverse ∘ obverse) a ≡⟨ sym h ⟩
@@ -206,7 +206,7 @@ module _ {ℓa ℓb : Level} (A : Set ℓa) (B : Set ℓb) where
           a ∎
           where
           c : isContr (fiber obverse (obverse a))
-          c = e (obverse a)
+          c = e .equiv-proof (obverse a)
           fbr : fiber obverse (obverse a)
           fbr = fst c
           a' : A