From 86b4f80aa5e05d3d3117a7714be2c9c0bb0b0749 Mon Sep 17 00:00:00 2001
From: Niels <nnmvdw@gmail.com>
Date: Fri, 4 Aug 2017 20:54:53 +0200
Subject: [PATCH] Added proof that Z' is HSet.

---
 int/Integers.v | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

diff --git a/int/Integers.v b/int/Integers.v
index 1b53378..e06192f 100644
--- a/int/Integers.v
+++ b/int/Integers.v
@@ -650,17 +650,16 @@ Section Isomorphic.
       apply concat_1p.      
   Defined.
 
-  Definition biinv_Z'_to_Int : BiInv Z'_to_Int :=
-    ((Int_to_Z' ; Z'_to_Int_to_Z'), (Int_to_Z' ; Int_to_Z'_to_Int)).
+  Definition biinv_Int_to_Z' : BiInv Int_to_Z' :=
+    ((Z'_to_Int ; Int_to_Z'_to_Int), (Z'_to_Int ; Z'_to_Int_to_Z')).
 
-  Definition equiv_Z'_to_Int : IsEquiv Z'_to_Int :=
-    isequiv_biinv _ biinv_Z'_to_Int.
+  Instance equiv_Int_to_Z' : IsEquiv Int_to_Z' :=
+    isequiv_biinv _ biinv_Int_to_Z'.
 
   Instance Z'_set : IsHSet Z'.
   Proof.
-    intros x y p q.
-    
-  Admitted.    
+    apply (trunc_equiv Int Int_to_Z').
+  Defined
 
   Definition Z_to_Z' : Z -> Z'.
   Proof.