From 0246c1b5abf190ec08f6d0fb935dff4be6327e88 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Thu, 22 Mar 2018 12:25:12 +0100
Subject: [PATCH] Readability

---
 src/Cat/Equivalence.agda | 18 +++++++-----------
 1 file changed, 7 insertions(+), 11 deletions(-)

diff --git a/src/Cat/Equivalence.agda b/src/Cat/Equivalence.agda
index fdbfc00..f60deae 100644
--- a/src/Cat/Equivalence.agda
+++ b/src/Cat/Equivalence.agda
@@ -166,17 +166,13 @@ module _ {ℓa ℓb : Level} (A : Set ℓa) (B : Set ℓb) where
       toIso y             ≡⟨ py ⟩
       x ∎
       where
-      helper : (x : Isomorphism _) → Σ _ λ y → toIso y ≡ x
-      helper (f~ , inv) = y , py
-        where
-        module inv = AreInverses inv
-        y  : isEquiv _ _ f
-        y  = {!!}
-        py : toIso y ≡ (f~ , inv)
-        py = {!!}
-      y : isEquiv _ _ _
-      y  = fst (helper x)
-      py = snd (helper x)
+      open Σ x renaming (fst to f~ ; snd to inv)
+      module inv = AreInverses inv
+      y  : isEquiv _ _ f
+      y  = {!!}
+      open Σ (toIso y) renaming (fst to f~' ; snd to inv')
+      py : toIso y ≡ (f~ , inv)
+      py = {!!}
 
 module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where
   open Cubical.PathPrelude using (_≃_)