feat(hott): start with proof to characterize (is_trunc n A) using iterated loop spaces

hott/hit/type_quotient.hlean

@@ -10,7 +10,7 @@ Type quotients (quotient without truncation)
   The hit type_quotient is primitive, declared in init.hit.
   The constructors are
     class_of : A → A / R (A implicit, R explicit)
-    eq_of_rel : Π{a a' : A}, R a a' → a = a' (R explicit)
+    eq_of_rel : Π{a a' : A}, R a a' → class_of a = class_of a' (R explicit)
 -/
 
 open eq equiv sigma.ops

hott/init/pathover.hlean

@@ -153,7 +153,7 @@ namespace eq
     {b : B' (f a)} {b₂ : B' (f a₂)} (q : b =[p] b₂) : b =[ap f p] b₂ :=
   by cases q; exact idpo
 
-  definition of_pathover_ap (B' : A' → Type) (f : A → A') {p : a = a₂}
+  definition pathover_of_pathover_ap (B' : A' → Type) (f : A → A') {p : a = a₂}
     {b : B' (f a)} {b₂ : B' (f a₂)} (q : b =[ap f p] b₂) : b =[p] b₂ :=
   by cases p; apply (idp_rec_on q); apply idpo
 
@@ -162,7 +162,7 @@ namespace eq
   begin
     fapply equiv.MK,
     { apply pathover_ap},
-    { apply of_pathover_ap},
+    { apply pathover_of_pathover_ap},
     { intro q, cases p, esimp, apply (idp_rec_on q), apply idp},
     { intro q, cases q, exact idp},
   end

hott/init/trunc.hlean

@@ -53,6 +53,11 @@ namespace is_trunc
   definition trunc_index.of_nat [coercion] [reducible] (n : nat) : trunc_index :=
   nat.rec_on n (-1.+1) (λ n k, k.+1)
 
+  definition sub_two [reducible] (n : nat) : trunc_index :=
+  nat.rec_on n -2 (λ n k, k.+1)
+
+  postfix `.-2`:(max+1) := sub_two
+
   /- truncated types -/
 
   /-

hott/types/trunc.hlean

@@ -10,7 +10,8 @@ Properties of is_trunc and trunctype
 
 import types.pi types.eq types.equiv .function
 
-open eq sigma sigma.ops pi function equiv is_trunc.trunctype is_equiv prod is_trunc.trunc_index
+open eq sigma sigma.ops pi function equiv is_trunc.trunctype
+     is_equiv prod is_trunc.trunc_index pointed nat
 
 namespace is_trunc
   variables {A B : Type} {n : trunc_index}
@@ -138,6 +139,28 @@ namespace is_trunc
     (K : Π(a : A), is_trunc n (a = a)) : is_trunc (n.+1) A :=
   @is_trunc_succ_intro _ _ (λa b, is_trunc_of_imp_is_trunc_of_leq H (λp, eq.rec_on p !K))
 
+  definition is_trunc_succ_of_is_trunc_loop (Hn : -1 ≤ n) (Hp : Π(a : A), is_trunc n (a = a))
+    : is_trunc (n.+1) A :=
+  begin
+    apply is_trunc_succ_intro, intros a a',
+    apply is_trunc_of_imp_is_trunc_of_leq Hn, intro p,
+    cases p, apply Hp
+  end
+
+  definition is_trunc_succ_iff_is_trunc_loop (A : Type) (Hn : -1 ≤ n) :
+    (Π(a : A), is_trunc n (a = a)) ↔ is_trunc (n.+1) A :=
+  iff.intro (is_trunc_succ_of_is_trunc_loop Hn) _
+
+  definition is_trunc_iff_is_contr_loop' {n : ℕ}
+    : (Π(a : A), is_contr (Ω[ n ](Pointed.mk a))) ↔ is_trunc (n.-2.+1) A :=
+  begin
+    induction n with n H,
+    { esimp [sub_two,Pointed.Iterated_loop_space], apply iff.intro,
+        intro H, apply is_hprop_of_imp_is_contr, exact H,
+        intro H a, exact is_contr_of_inhabited_hprop a},
+    { exact sorry},
+  end
+
 end is_trunc open is_trunc
 
 namespace trunc