From 2c81c93d69af662cb069c1b59359beda896b1e63 Mon Sep 17 00:00:00 2001
From: seulbaek <seulkeebaek@gmail.com>
Date: Tue, 19 Jan 2016 13:20:18 -0800
Subject: [PATCH] feat(hott/types/equiv): add is_trunc_equiv to equiv.hlean

---
 hott/types/equiv.hlean | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/hott/types/equiv.hlean b/hott/types/equiv.hlean
index c9ca55f39..60d48e3ae 100644
--- a/hott/types/equiv.hlean
+++ b/hott/types/equiv.hlean
@@ -182,4 +182,21 @@ namespace equiv
         apply is_hprop.elimo}
   end
 
+  definition is_contr_equiv (A B : Type) [HA : is_contr A] [HB : is_contr B] : is_contr (A ≃ B) :=
+  begin 
+    apply @is_contr_of_inhabited_hprop, apply is_hprop.mk, 
+    intro x y, cases x with fx Hx, cases y with fy Hy, generalize Hy, 
+    apply (eq_of_homotopy (λ a, !eq_of_is_contr)) ▸ (λ Hy, !is_hprop.elim ▸ rfl), 
+    apply equiv_of_is_contr_of_is_contr 
+  end
+  
+  definition is_trunc_succ_equiv (n : trunc_index) (A B : Type)
+  [HA : is_trunc n.+1 A] [HB : is_trunc n.+1 B] : is_trunc n.+1 (A ≃ B) :=
+  @is_trunc_equiv_closed _ _ n.+1 (equiv.symm !equiv.sigma_char)
+  (@is_trunc_sigma _ _ _ _ (λ f, !is_trunc_succ_of_is_hprop))
+  
+  definition is_trunc_equiv (n : trunc_index) (A B : Type) 
+  [HA : is_trunc n A] [HB : is_trunc n B] : is_trunc n (A ≃ B) :=
+  by cases n; apply !is_contr_equiv; apply !is_trunc_succ_equiv 
+
 end equiv