From e16a4b81895782087dd627bcc6b49e8f34ee0ac3 Mon Sep 17 00:00:00 2001
From: Andrea Vezzosi <sanzhiyan@gmail.com>
Date: Fri, 15 Jun 2018 10:02:46 +0200
Subject: [PATCH] isEquiv is now a record

---
 src/Cat/Category.agda    | 2 +-
 src/Cat/Equivalence.agda | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

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