diff --git a/hott/algebra/e_closure.hlean b/hott/algebra/e_closure.hlean
index 5a01c4ba7..46b5c3cb7 100644
--- a/hott/algebra/e_closure.hlean
+++ b/hott/algebra/e_closure.hlean
@@ -23,18 +23,18 @@ namespace e_closure
   postfix `⁻¹ʳ`:(max+10) := e_closure.symm
   notation `[`:max a `]`:0 := e_closure.of_rel a
   notation `<`:max p `>`:0 := e_closure.of_path _ p
-  abbreviation rfl {A : Type} {R : A → A → Type} {a : A} := of_path R (idpath a)
+  abbreviation rfl [constructor] {A : Type} {R : A → A → Type} {a : A} := of_path R (idpath a)
 end e_closure
 open e_closure
 namespace relation
 
 section
   parameters {A : Type}
-             (R : A → A → Type)
+             {R : A → A → Type}
   local abbreviation T := e_closure R
 
   variables ⦃a a' a'' : A⦄ {s : R a a'} {r : T a a} {B C : Type}
-  parameter {R}
+
   protected definition e_closure.elim [unfold 8] {f : A → B}
     (e : Π⦃a a' : A⦄, R a a' → f a = f a') (t : T a a') : f a = f a' :=
   begin
diff --git a/hott/algebra/homotopy_group.hlean b/hott/algebra/homotopy_group.hlean
index d92c3ae9a..04b24bc04 100644
--- a/hott/algebra/homotopy_group.hlean
+++ b/hott/algebra/homotopy_group.hlean
@@ -47,7 +47,7 @@ namespace eq
 
   definition phomotopy_group_pequiv [constructor] (n : ℕ) {A B : Type*} (H : A ≃* B)
     : π*[n] A ≃* π*[n] B :=
-  ptrunc_pequiv_ptrunc 0 (iterated_loop_space_pequiv n H)
+  ptrunc_pequiv_ptrunc 0 (loopn_pequiv_loopn n H)
 
   definition phomotopy_group_pequiv_loop_ptrunc [constructor] (k : ℕ) (A : Type*) :
     π*[k] A ≃* Ω[k] (ptrunc k A) :=
diff --git a/hott/book.md b/hott/book.md
index c1ba41cb3..fd14d08aa 100644
--- a/hott/book.md
+++ b/hott/book.md
@@ -20,9 +20,9 @@ The rows indicate the chapters, the columns the sections.
 | Ch 3  | + | + | + | + | ½ | + | + | + | + | .  | +  |    |    |    |    |
 | Ch 4  | - | + | + | + | . | + | + | + | + |    |    |    |    |    |    |
 | Ch 5  | - | . | ½ | - | - | . | . | ½ |   |    |    |    |    |    |    |
-| Ch 6  | . | + | + | + | + | ½ | ½ | + | ¾ | ¼  | ¾  | +  | .  |    |    |
+| Ch 6  | . | + | + | + | + | + | + | + | ¾ | ¼  | ¾  | +  | .  |    |    |
 | Ch 7  | + | + | + | - | ¾ | - | - |   |   |    |    |    |    |    |    |
-| Ch 8  | + | + | + | - | ¾ | ¼ | - | - | - | -  |    |    |    |    |    |
+| Ch 8  | + | + | + | - | ¾ | ¼ | - | - | ½ | -  |    |    |    |    |    |
 | Ch 9  | ¾ | + | + | ½ | ¾ | ½ | - | - | - |    |    |    |    |    |    |
 | Ch 10 | - | - | - | - | - |   |   |   |   |    |    |    |    |    |    |
 | Ch 11 | - | - | - | - | - | - |   |   |   |    |    |    |    |    |    |
@@ -99,25 +99,29 @@ Chapter 4: Equivalences
 Chapter 5: Induction
 ---------
 
+Lean has support for inductive families, but not for induction-induction or induction-recursion.
+
 - 5.1 (Introduction to inductive types): not formalized
 - 5.2 (Uniqueness of inductive types): no formalizable content
 - 5.3 (W-types): [types.W](types/W.hlean) defines W-types.
 - 5.4 (Inductive types are initial algebras): not formalized
 - 5.5 (Homotopy-inductive types): not formalized
 - 5.6 (The general syntax of inductive definitions): no formalizable content
-- 5.7 (Generalizations of inductive types): no formalizable content. Lean has inductive families and mutual induction, but no induction-induction or induction-recursion
+- 5.7 (Generalizations of inductive types): no formalizable content.
 - 5.8 (Identity types and identity systems): 5.8.1-5.8.4 not formalized, 5.8.5 in [init.ua](init/ua.hlean) and 5.8.6 in [init.funext](init/funext.hlean)
 
 Chapter 6: Higher inductive types
 ---------
 
+We have two primitive HITs in Lean, the computation rules are manually added to the Lean-HoTT kernel. The primitive HITs are the n-truncation and the quotient (not to be confused with the set-quotient). See [init.hit](init/hit.hlean).
+
 - 6.1 (Introduction): no formalizable content
 - 6.2 (Induction principles and dependent paths): dependent paths in [init.pathover](init/pathover.hlean), circle in [homotopy.circle](homotopy/circle.hlean)
 - 6.3 (The interval): [homotopy.interval](homotopy/interval.hlean)
 - 6.4 (Circles and spheres): [homotopy.sphere](homotopy/sphere.hlean) and [homotopy.circle](homotopy/circle.hlean)
 - 6.5 (Suspensions): [homotopy.suspension](homotopy/susp.hlean) (we define the circle to be the suspension of bool, but Lemma 6.5.1 is similar to proving the ordinary induction principle for the circle in [homotopy.circle](homotopy/circle.hlean)) and a bit in [homotopy.sphere](homotopy/sphere.hlean) and [types.pointed](types/pointed.hlean)
-- 6.6 (Cell complexes): we define the torus using the quotient, see [hit.two_quotient](hit/two_quotient.hlean) and [homotopy.torus](homotopy/torus.hlean) (no dependent eliminator defined yet)
-- 6.7 (Hubs and spokes): [hit.two_quotient](hit/two_quotient.hlean) and [homotopy.torus](homotopy/torus.hlean) (no dependent eliminator defined yet)
+- 6.6 (Cell complexes): We define the torus using a two quotient, which in turn is defined in terms of the quotient, see [homotopy.torus](homotopy/torus.hlean).
+- 6.7 (Hubs and spokes): We define the two quotient using only the quotient in [hit.two_quotient](hit/two_quotient.hlean). This is slightly different than what is done in section 6.7, because the HIT in section 6.7 is not a quotient.
 - 6.8 (Pushouts): [hit.pushout](hit/pushout.hlean). Some of the "standard homotopy-theoretic constructions" have separate files, although not all of them have been defined explicitly yet
 - 6.9 (Truncations): [hit.trunc](hit/trunc.hlean) (except Lemma 6.9.3)
 - 6.10 (Quotients): [hit.set_quotient](hit/set_quotient.hlean) (up to 6.10.3). We define integers differently, to make them compute, in the folder [types.int](types/int/int.md). 6.10.13 is in [types.int.hott](types/int/hott.hlean)
@@ -149,7 +153,7 @@ Every file is in the folder [homotopy](homotopy/homotopy.md)
 - 8.6 (The Freudenthal suspension theorem): [connectedness](homotopy/connectedness.hlean) (Lemma 8.6.1), [wedge](homotopy/wedge.hlean) (Wedge connectivity, Lemma 8.6.2), the rest is not formalized
 - 8.7 (The van Kampen theorem): not formalized
 - 8.8 (Whitehead’s theorem and Whitehead’s principle): not formalized
-- 8.9 (A general statement of the encode-decode method): not formalized
+- 8.9 (A general statement of the encode-decode method): One variation of the encode-decode method is in [types.eq](types/eq.hlean).
 - 8.10 (Additional Results): not formalized
 
 Chapter 9: Category theory
diff --git a/hott/hit/two_quotient.hlean b/hott/hit/two_quotient.hlean
index 25111b9b6..e96e346da 100644
--- a/hott/hit/two_quotient.hlean
+++ b/hott/hit/two_quotient.hlean
@@ -332,7 +332,7 @@ namespace simple_two_quotient
 end
 end simple_two_quotient
 
-attribute simple_two_quotient.j [constructor]
+attribute simple_two_quotient.j simple_two_quotient.incl0 [constructor]
 attribute simple_two_quotient.rec simple_two_quotient.elim [unfold 8] [recursor 8]
 --attribute simple_two_quotient.elim_type [unfold 9] -- TODO
 attribute simple_two_quotient.rec_on simple_two_quotient.elim_on [unfold 5]
diff --git a/hott/homotopy/circle.hlean b/hott/homotopy/circle.hlean
index fb2f936bc..8c810a98a 100644
--- a/hott/homotopy/circle.hlean
+++ b/hott/homotopy/circle.hlean
@@ -164,7 +164,7 @@ namespace circle
 
   theorem elim_type_loop (Pbase : Type) (Ploop : Pbase ≃ Pbase) :
     transport (circle.elim_type Pbase Ploop) loop = Ploop :=
-  by rewrite [tr_eq_cast_ap_fn,↑circle.elim_type,circle.elim_loop];apply cast_ua_fn
+  by rewrite [tr_eq_cast_ap_fn,↑circle.elim_type,elim_loop];apply cast_ua_fn
 
   theorem elim_type_loop_inv (Pbase : Type) (Ploop : Pbase ≃ Pbase) :
     transport (circle.elim_type Pbase Ploop) loop⁻¹ = to_inv Ploop :=
@@ -182,6 +182,40 @@ attribute circle.rec_on circle.elim_on [unfold 2]
 attribute circle.elim_type_on [unfold 1]
 
 namespace circle
+  open sigma
+  /- universal property of the circle -/
+  definition circle_pi_equiv [constructor] (P : S¹ → Type)
+    : (Π(x : S¹), P x) ≃ Σ(p : P base), p =[loop] p :=
+  begin
+    fapply equiv.MK,
+    { intro f, exact ⟨f base, apdo f loop⟩},
+    { intro v x, induction v with p q, induction x,
+      { exact p},
+      { exact q}},
+    { intro v, induction v with p q, fapply sigma_eq,
+      { reflexivity},
+      { esimp, apply pathover_idp_of_eq, apply rec_loop}},
+    { intro f, apply eq_of_homotopy, intro x, induction x,
+      { reflexivity},
+      { apply eq_pathover_dep, apply hdeg_squareover, esimp, apply rec_loop}}
+  end
+
+  definition circle_arrow_equiv [constructor] (P : Type)
+    : (S¹ → P) ≃ Σ(p : P), p = p :=
+  begin
+    fapply equiv.MK,
+    { intro f, exact ⟨f base, ap f loop⟩},
+    { intro v x, induction v with p q, induction x,
+      { exact p},
+      { exact q}},
+    { intro v, induction v with p q, fapply sigma_eq,
+      { reflexivity},
+      { esimp, apply pathover_idp_of_eq, apply elim_loop}},
+    { intro f, apply eq_of_homotopy, intro x, induction x,
+      { reflexivity},
+      { apply eq_pathover, apply hdeg_square, esimp, apply elim_loop}}
+  end
+
   definition pointed_circle [instance] [constructor] : pointed S¹ :=
   pointed.mk base
 
diff --git a/hott/homotopy/connectedness.hlean b/hott/homotopy/connectedness.hlean
index 802d5475c..ae3e65797 100644
--- a/hott/homotopy/connectedness.hlean
+++ b/hott/homotopy/connectedness.hlean
@@ -265,4 +265,17 @@ namespace is_conn
     [H : is_conn_fun n f] : trunc n A ≃ trunc n B :=
   equiv.mk (trunc_functor n f) (is_equiv_trunc_functor_of_is_conn_fun n f)
 
+  definition is_conn_fun_trunc_functor {n k : ℕ₋₂} {A B : Type} (f : A → B) (H : k ≤ n)
+    [H2 : is_conn_fun k f] : is_conn_fun k (trunc_functor n f) :=
+  begin
+    apply is_conn_fun.intro,
+    intro P, have Πb, is_trunc n (P b), from (λb, is_trunc_of_le _ H),
+    fconstructor,
+    { intro f' b,
+      induction b with b,
+      refine is_conn_fun.elim k H2 _ _ b, intro a, exact f' (tr a)},
+    { intro f', apply eq_of_homotopy, intro a,
+      induction a with a, esimp, rewrite [is_conn_fun.elim_β]}
+  end
+
 end is_conn
diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean
index cd5174045..79573781b 100644
--- a/hott/init/equiv.hlean
+++ b/hott/init/equiv.hlean
@@ -68,10 +68,10 @@ namespace is_equiv
   parameters {A B : Type} (f : A → B) (g : B → A)
             (ret : Πb, f (g b) = b) (sec : Πa, g (f a) = a)
 
-  private definition adjointify_left_inv' (a : A) : g (f a) = a :=
+  definition adjointify_left_inv' (a : A) : g (f a) = a :=
   ap g (ap f (inverse (sec a))) ⬝ ap g (ret (f a)) ⬝ sec a
 
-  private theorem adjointify_adj' (a : A) : ret (f a) = ap f (adjointify_left_inv' a) :=
+  theorem adjointify_adj' (a : A) : ret (f a) = ap f (adjointify_left_inv' a) :=
   let fgretrfa := ap f (ap g (ret (f a))) in
   let fgfinvsect := ap f (ap g (ap f (sec a)⁻¹)) in
   let fgfa := f (g (f a)) in
diff --git a/hott/init/hit.hlean b/hott/init/hit.hlean
index d96137396..ea3c27526 100644
--- a/hott/init/hit.hlean
+++ b/hott/init/hit.hlean
@@ -28,18 +28,18 @@ open is_trunc eq
   uses of these hits, see the folder ../hit/
 -/
 
-constant trunc.{u} (n : trunc_index) (A : Type.{u}) : Type.{u}
+constant trunc.{u} (n : ℕ₋₂) (A : Type.{u}) : Type.{u}
 
 namespace trunc
-  constant tr {n : trunc_index} {A : Type} (a : A) : trunc n A
-  constant is_trunc_trunc (n : trunc_index) (A : Type) : is_trunc n (trunc n A)
+  constant tr {n : ℕ₋₂} {A : Type} (a : A) : trunc n A
+  constant is_trunc_trunc (n : ℕ₋₂) (A : Type) : is_trunc n (trunc n A)
 
   attribute is_trunc_trunc [instance]
 
-  protected constant rec {n : trunc_index} {A : Type} {P : trunc n A → Type}
+  protected constant rec {n : ℕ₋₂} {A : Type} {P : trunc n A → Type}
     [Pt : Πaa, is_trunc n (P aa)] (H : Πa, P (tr a)) : Πaa, P aa
 
-  protected definition rec_on [reducible] {n : trunc_index} {A : Type}
+  protected definition rec_on [reducible] {n : ℕ₋₂} {A : Type}
     {P : trunc n A → Type} (aa : trunc n A) [Pt : Πaa, is_trunc n (P aa)] (H : Πa, P (tr a))
     : P aa :=
   trunc.rec H aa
@@ -68,7 +68,7 @@ end quotient
 init_hits -- Initialize builtin computational rules for trunc and quotient
 
 namespace trunc
-  definition rec_tr [reducible] {n : trunc_index} {A : Type} {P : trunc n A → Type}
+  definition rec_tr [reducible] {n : ℕ₋₂} {A : Type} {P : trunc n A → Type}
     [Pt : Πaa, is_trunc n (P aa)] (H : Πa, P (tr a)) (a : A) : trunc.rec H (tr a) = H a :=
   idp
 end trunc
diff --git a/hott/init/tactic.hlean b/hott/init/tactic.hlean
index ae6670628..97eb0757d 100644
--- a/hott/init/tactic.hlean
+++ b/hott/init/tactic.hlean
@@ -144,8 +144,8 @@ definition repeat1     (t : tactic) : tactic := and_then t (repeat t)
 definition focus       (t : tactic) : tactic := focus_at t 0
 definition determ      (t : tactic) : tactic := at_most t 1
 definition trivial                  : tactic := or_else (apply eq.refl) assumption
-definition do (n : num) (t : tactic) : tactic :=
-nat.rec id (λn t', and_then t t') (nat.of_num n)
+definition do (n : nat) (t : tactic) : tactic :=
+nat.rec id (λn t', and_then t t') n
 
 end tactic
 tactic_infixl `;`:15 := tactic.and_then
diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean
index e1e01f139..3c53f2794 100644
--- a/hott/init/trunc.hlean
+++ b/hott/init/trunc.hlean
@@ -23,7 +23,8 @@ open trunc_index
 
 /-
    notation for trunc_index is -2, -1, 0, 1, ...
-   from 0 and up this comes from a coercion from num to trunc_index (via ℕ)
+   from 0 and up this comes from the way numerals are parsed in Lean.
+   Any structure with a 0, a 1, and a + have numerals defined in them.
 -/
 
 notation `ℕ₋₂` := trunc_index -- input using \N-2
diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean
index 30026578d..3453f64e8 100644
--- a/hott/types/pointed.hlean
+++ b/hott/types/pointed.hlean
@@ -539,6 +539,13 @@ namespace pointed
     { refine ap1_phomotopy IH ⬝* _, apply ap1_compose}
   end
 
+  definition apn_pid [constructor] {A : Type*} (n : ℕ) : apn n (pid A) ~* pid (Ω[n] A) :=
+  begin
+    induction n with n IH,
+    { reflexivity},
+    { exact ap1_phomotopy IH ⬝* ap1_id}
+  end
+
   theorem apn_con (n : ℕ) (f : A →* B) (p q : Ω[n+1] A)
     : apn (n+1) f (p ⬝ q) = apn (n+1) f p ⬝ apn (n+1) f q :=
   by rewrite [+apn_succ, ap1_con]
diff --git a/hott/types/pointed2.hlean b/hott/types/pointed2.hlean
index 86fa91c68..1f28763ab 100644
--- a/hott/types/pointed2.hlean
+++ b/hott/types/pointed2.hlean
@@ -11,10 +11,6 @@ import .equiv cubical.square
 
 open eq is_equiv equiv pointed is_trunc
 
--- structure pequiv (A B : Type*) :=
---   (to_pmap : A →* B)
---   (is_equiv_to_pmap : is_equiv to_pmap)
-
 structure pequiv (A B : Type*) extends equiv A B, pmap A B
 
 namespace pointed
@@ -36,7 +32,7 @@ namespace pointed
   definition pequiv_of_equiv [constructor] (f : A ≃ B) (H : f pt = pt) : A ≃* B :=
   pequiv.mk f _ H
 
-  protected definition pequiv.MK [constructor] (f : A →* B) (g : B →* A)
+  protected definition pequiv.MK [constructor] (f : A →* B) (g : B → A)
     (gf : Πa, g (f a) = a) (fg : Πb, f (g b) = b) : A ≃* B :=
   pequiv.mk f (adjointify f g fg gf) (respect_pt f)
 
@@ -44,7 +40,34 @@ namespace pointed
   equiv.mk f _
 
   definition to_pinv [constructor] (f : A ≃* B) : B →* A :=
-  pmap.mk f⁻¹ ((ap f⁻¹ (respect_pt f))⁻¹ ⬝ !left_inv)
+  pmap.mk f⁻¹ ((ap f⁻¹ (respect_pt f))⁻¹ ⬝ left_inv f pt)
+
+  /- A version of pequiv.MK with stronger conditions.
+     The advantage of defining a pointed equivalence with this definition is that there is a
+     pointed homotopy between the inverse of the resulting equivalence and the given pointed map g.
+     This is not the case when using `pequiv.MK` (if g is a pointed map),
+     that will only give an ordinary homotopy.
+  -/
+  protected definition pequiv.MK2 [constructor] (f : A →* B) (g : B →* A)
+    (gf : g ∘* f ~* !pid) (fg : f ∘* g ~* !pid) : A ≃* B :=
+  pequiv.MK f g gf fg
+
+  definition to_pmap_pequiv_MK2 [constructor] (f : A →* B) (g : B →* A)
+    (gf : g ∘* f ~* !pid) (fg : f ∘* g ~* !pid) : pequiv.MK2 f g gf fg ~* f :=
+  phomotopy.mk (λb, idp) !idp_con
+
+  definition to_pinv_pequiv_MK2 [constructor] (f : A →* B) (g : B →* A)
+    (gf : g ∘* f ~* !pid) (fg : f ∘* g ~* !pid) : to_pinv (pequiv.MK2 f g gf fg) ~* g :=
+  phomotopy.mk (λb, idp)
+    abstract [irreducible] begin
+      esimp, unfold [adjointify_left_inv'],
+      note H := to_homotopy_pt gf, note H2 := to_homotopy_pt fg,
+      note H3 := eq_top_of_square (natural_square_tr (to_homotopy fg) (respect_pt f)),
+      rewrite [▸* at *, H, H3, H2, ap_id, - +con.assoc, ap_compose' f g, con_inv,
+               - ap_inv, - +ap_con g],
+      apply whisker_right, apply ap02 g,
+      rewrite [ap_con, - + con.assoc, +ap_inv, +inv_con_cancel_right, con.left_inv],
+    end end
 
   definition pua {A B : Type*} (f : A ≃* B) : A = B :=
   pType_eq (equiv_of_pequiv f) !respect_pt
@@ -64,6 +87,13 @@ namespace pointed
   postfix `⁻¹ᵉ*`:(max + 1) := pequiv.symm
   infix ` ⬝e* `:75 := pequiv.trans
 
+  definition pequiv_change_fun [constructor] (f : A ≃* B) (f' : A →* B) (Heq : f ~ f') : A ≃* B :=
+  pequiv_of_pmap f' (is_equiv.homotopy_closed f Heq)
+
+  definition pequiv_change_inv [constructor] (f : A ≃* B) (f' : B →* A) (Heq : to_pinv f ~ f')
+    : A ≃* B :=
+  pequiv.MK f f' (to_left_inv (equiv_change_inv f Heq)) (to_right_inv (equiv_change_inv f Heq))
+
   definition pequiv_rect' (f : A ≃* B) (P : A → B → Type)
     (g : Πb, P (f⁻¹ b) b) (a : A) : P a (f a) :=
   left_inv f a ▸ g (f a)
@@ -83,26 +113,12 @@ namespace pointed
   definition peap {A B : Type*} (F : Type* → Type*) (p : A ≃* B) : F A ≃* F B :=
   pequiv_of_pmap (pcast (ap F (eq_of_pequiv p))) begin cases eq_of_pequiv p, apply is_equiv_id end
 
-  definition loop_space_pequiv [constructor] (p : A ≃* B) : Ω A ≃* Ω B :=
-  pequiv_of_pmap (ap1 p) (is_equiv_ap1 p)
-
-  definition iterated_loop_space_pequiv [constructor] (n : ℕ) (p : A ≃* B) : Ω[n] A ≃* Ω[n] B :=
-  pequiv_of_pmap (apn n p) (is_equiv_apn n p)
-
   definition pequiv_eq {p q : A ≃* B} (H : p = q :> (A →* B)) : p = q :=
   begin
     cases p with f Hf, cases q with g Hg, esimp at *,
     exact apd011 pequiv_of_pmap H !is_prop.elim
   end
 
-  definition loop_space_pequiv_rfl
-    : loop_space_pequiv (@pequiv.refl A) = @pequiv.refl (Ω A) :=
-  begin
-    apply pequiv_eq, fapply pmap_eq: esimp,
-    { intro p, exact !idp_con ⬝ !ap_id},
-    { reflexivity}
-  end
-
   infix ` ⬝e*p `:75 := peconcat_eq
   infix ` ⬝pe* `:75 := eq_peconcat
 
@@ -195,33 +211,50 @@ namespace pointed
 
   /- pointed equivalences between particular pointed types -/
 
-  definition loop_pequiv_loop [constructor] (f : A ≃* B) : Ω A ≃* Ω B :=
-  pequiv.MK (ap1 f) (ap1 f⁻¹ᵉ*)
+  definition loopn_pequiv_loopn [constructor] (n : ℕ) (f : A ≃* B) : Ω[n] A ≃* Ω[n] B :=
+  pequiv.MK2 (apn n f) (apn n f⁻¹ᵉ*)
   abstract begin
-    intro p,
-    refine ((ap1_compose f⁻¹ᵉ* f) p)⁻¹ ⬝ _,
-    refine ap1_phomotopy (pleft_inv f) p ⬝ _,
-    exact ap1_id p
+    induction n with n IH,
+    { apply pleft_inv},
+    { replace nat.succ n with n + 1,
+      rewrite [+apn_succ],
+      refine !ap1_compose⁻¹* ⬝* _,
+      refine ap1_phomotopy IH ⬝* _,
+      apply ap1_id}
   end end
   abstract begin
-    intro p,
-    refine ((ap1_compose f f⁻¹ᵉ*) p)⁻¹ ⬝ _,
-    refine ap1_phomotopy (pright_inv f) p ⬝ _,
-    exact ap1_id p
+    induction n with n IH,
+    { apply pright_inv},
+    { replace nat.succ n with n + 1,
+      rewrite [+apn_succ],
+      refine !ap1_compose⁻¹* ⬝* _,
+      refine ap1_phomotopy IH ⬝* _,
+      apply ap1_id}
   end end
 
-  definition loopn_pequiv_loopn (n : ℕ) (f : A ≃* B) : Ω[n] A ≃* Ω[n] B :=
-  begin
-    induction n with n IH,
-    { exact f},
-    { exact loop_pequiv_loop IH}
-  end
+  definition loop_pequiv_loop [constructor] (f : A ≃* B) : Ω A ≃* Ω B :=
+  loopn_pequiv_loopn 1 f
+
+  definition to_pmap_loopn_pequiv_loopn [constructor] (n : ℕ) (f : A ≃* B)
+    : loopn_pequiv_loopn n f ~* apn n f :=
+  !to_pmap_pequiv_MK2
+
+  definition to_pinv_loopn_pequiv_loopn [constructor] (n : ℕ) (f : A ≃* B)
+    : (loopn_pequiv_loopn n f)⁻¹ᵉ* ~* apn n f⁻¹ᵉ* :=
+  !to_pinv_pequiv_MK2
 
   definition loopn_pequiv_loopn_con (n : ℕ) (f : A ≃* B) (p q : Ω[n+1] A)
     : loopn_pequiv_loopn (n+1) f (p ⬝ q) =
     loopn_pequiv_loopn (n+1) f p ⬝ loopn_pequiv_loopn (n+1) f q :=
   ap1_con (loopn_pequiv_loopn n f) p q
 
+  definition loopn_pequiv_loopn_rfl (n : ℕ) :
+    loopn_pequiv_loopn n (@pequiv.refl A) = @pequiv.refl (Ω[n] A) :=
+  begin
+    apply pequiv_eq, apply eq_of_phomotopy,
+    exact !to_pmap_loopn_pequiv_loopn ⬝* apn_pid n,
+  end
+
   definition pmap_functor [constructor] {A A' B B' : Type*} (f : A' →* A) (g : B →* B') :
     ppmap A B →* ppmap A' B' :=
   pmap.mk (λh, g ∘* h ∘* f)
diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean
index b00fc0645..47c5b2376 100644
--- a/hott/types/sigma.hlean
+++ b/hott/types/sigma.hlean
@@ -393,6 +393,18 @@ namespace sigma
     { intro v, induction v with a p, induction p: reflexivity},
   end
 
+  definition sigma_sigma_eq_right {A : Type} (a : A) (P : Π(b : A), a = b → Type)
+    : (Σ(b : A) (p : a = b), P b p) ≃ P a idp :=
+  calc
+    (Σ(b : A) (p : a = b), P b p) ≃ (Σ(v : Σ(b : A), a = b), P v.1 v.2) : sigma_assoc_equiv
+      ... ≃ P a idp : !sigma_equiv_of_is_contr_left
+
+  definition sigma_sigma_eq_left {A : Type} (a : A) (P : Π(b : A), b = a → Type)
+    : (Σ(b : A) (p : b = a), P b p) ≃ P a idp :=
+  calc
+    (Σ(b : A) (p : b = a), P b p) ≃ (Σ(v : Σ(b : A), b = a), P v.1 v.2) : sigma_assoc_equiv
+      ... ≃ P a idp : !sigma_equiv_of_is_contr_left
+
   /- ** Universal mapping properties -/
   /- *** The positive universal property. -/
 
diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean
index f987e6f00..ec16ff10e 100644
--- a/hott/types/trunc.hlean
+++ b/hott/types/trunc.hlean
@@ -13,6 +13,7 @@ import .pointed2 ..function algebra.order types.nat.order
 open eq sigma sigma.ops pi function equiv trunctype
      is_equiv prod pointed nat is_trunc algebra
 
+  /- basic computation with ℕ₋₂, its operations and its order -/
 namespace trunc_index
 
   definition minus_one_le_succ (n : ℕ₋₂) : -1 ≤ n.+1 :=
@@ -203,26 +204,7 @@ namespace is_trunc
 
   variables {A B : Type} {n : ℕ₋₂}
 
-  /- theorems about trunctype -/
-  protected definition trunctype.sigma_char.{l} [constructor] (n : ℕ₋₂) :
-    (trunctype.{l} n) ≃ (Σ (A : Type.{l}), is_trunc n A) :=
-  begin
-    fapply equiv.MK,
-    { intro A, exact (⟨carrier A, struct A⟩)},
-    { intro S, exact (trunctype.mk S.1 S.2)},
-    { intro S, induction S with S1 S2, reflexivity},
-    { intro A, induction A with A1 A2, reflexivity},
-  end
-
-  definition trunctype_eq_equiv [constructor] (n : ℕ₋₂) (A B : n-Type) :
-    (A = B) ≃ (carrier A = carrier B) :=
-  calc
-    (A = B) ≃ (to_fun (trunctype.sigma_char n) A = to_fun (trunctype.sigma_char n) B)
-              : eq_equiv_fn_eq_of_equiv
-      ... ≃ ((to_fun (trunctype.sigma_char n) A).1 = (to_fun (trunctype.sigma_char n) B).1)
-             : equiv.symm (!equiv_subtype)
-      ... ≃ (carrier A = carrier B) : equiv.refl
-
+  /- closure properties of truncatedness -/
   theorem is_trunc_is_embedding_closed (f : A → B) [Hf : is_embedding f] [HB : is_trunc n B]
     (Hn : -1 ≤ n) : is_trunc n A :=
   begin
@@ -254,13 +236,31 @@ namespace is_trunc
   definition is_embedding_to_fun (A B : Type) : is_embedding (@to_fun A B)  :=
   λf f', !is_equiv_ap_to_fun
 
+  /- theorems about trunctype -/
+  protected definition trunctype.sigma_char.{l} [constructor] (n : ℕ₋₂) :
+    (trunctype.{l} n) ≃ (Σ (A : Type.{l}), is_trunc n A) :=
+  begin
+    fapply equiv.MK,
+    { intro A, exact (⟨carrier A, struct A⟩)},
+    { intro S, exact (trunctype.mk S.1 S.2)},
+    { intro S, induction S with S1 S2, reflexivity},
+    { intro A, induction A with A1 A2, reflexivity},
+  end
+
+  definition trunctype_eq_equiv [constructor] (n : ℕ₋₂) (A B : n-Type) :
+    (A = B) ≃ (carrier A = carrier B) :=
+  calc
+    (A = B) ≃ (to_fun (trunctype.sigma_char n) A = to_fun (trunctype.sigma_char n) B)
+              : eq_equiv_fn_eq_of_equiv
+      ... ≃ ((to_fun (trunctype.sigma_char n) A).1 = (to_fun (trunctype.sigma_char n) B).1)
+             : equiv.symm (!equiv_subtype)
+      ... ≃ (carrier A = carrier B) : equiv.refl
+
   theorem is_trunc_trunctype [instance] (n : ℕ₋₂) : is_trunc n.+1 (n-Type) :=
   begin
     apply is_trunc_succ_intro, intro X Y,
-    fapply is_trunc_equiv_closed,
-    { apply equiv.symm, apply trunctype_eq_equiv},
-    fapply is_trunc_equiv_closed,
-    { apply equiv.symm, apply eq_equiv_equiv},
+    fapply is_trunc_equiv_closed_rev, { apply trunctype_eq_equiv},
+    fapply is_trunc_equiv_closed_rev, { apply eq_equiv_equiv},
     induction n,
     { apply @is_contr_of_inhabited_prop,
       { apply is_trunc_is_embedding_closed,
@@ -272,7 +272,6 @@ namespace is_trunc
       { apply minus_one_le_succ}}
   end
 
-
   /- theorems about decidable equality and axiom K -/
   theorem is_set_of_axiom_K {A : Type} (K : Π{a : A} (p : a = a), p = idp) : is_set A :=
   is_set.mk _ (λa b p q, eq.rec K q p)
@@ -413,6 +412,7 @@ namespace trunc
     : (tr a = tr a' :> trunc n.+1 A) ≃ trunc n (a = a') :=
   !trunc_eq_equiv
 
+  /- encode preserves concatenation -/
   definition trunc_functor2 [unfold 6 7] {n : ℕ₋₂} {A B C : Type} (f : A → B → C)
     (x : trunc n A) (y : trunc n B) : trunc n C :=
   by induction x with a; induction y with b; exact tr (f a b)
@@ -425,8 +425,7 @@ namespace trunc
     (g : trunc.code n aa₁ aa₂) (h : trunc.code n aa₂ aa₃) : trunc.code n aa₁ aa₃ :=
   begin
     induction aa₁ with a₁, induction aa₂ with a₂, induction aa₃ with a₃,
-    esimp at *, induction g with p, induction h with q,
-    exact tr (p ⬝ q)
+    esimp at *, apply trunc_concat g h,
   end
 
   definition encode_con' {n : ℕ₋₂} {aa₁ aa₂ aa₃ : trunc n.+1 A} (p : aa₁ = aa₂) (q : aa₂ = aa₃)
@@ -440,6 +439,22 @@ namespace trunc
     : trunc.encode (p ⬝ q) = trunc_concat (trunc.encode p) (trunc.encode q) :=
   encode_con' p q
 
+  /- the principle of unique choice -/
+  definition unique_choice {P : A → Type} [H : Πa, is_prop (P a)] (f : Πa, ∥ P a ∥) (a : A)
+    : P a :=
+  !trunc_equiv (f a)
+
+  /- transport over a truncated family -/
+  definition trunc_transport {a a' : A} {P : A → Type} (p : a = a') (n : ℕ₋₂) (x : P a)
+    : transport (λa, trunc n (P a)) p (tr x) = tr (p ▸ x) :=
+  by induction p; reflexivity
+
+  /- pathover over a truncated family -/
+  definition trunc_pathover {A : Type} {B : A → Type} {n : ℕ₋₂} {a a' : A} {p : a = a'}
+    {b : B a} {b' : B a'} (q : b =[p] b') : @tr n _ b =[p] @tr n _ b' :=
+  by induction q; constructor
+
+  /- truncations preserve truncatedness -/
   definition is_trunc_trunc_of_is_trunc [instance] [priority 500] (A : Type)
     (n m : ℕ₋₂) [H : is_trunc n A] : is_trunc n (trunc m A) :=
   begin
@@ -456,20 +471,6 @@ namespace trunc
         { exact (IH _ _ _)}}}
   end
 
-  definition unique_choice {P : A → Type} [H : Πa, is_prop (P a)] (f : Πa, ∥ P a ∥) (a : A)
-    : P a :=
-  !trunc_equiv (f a)
-
-  /- transport over a truncated family -/
-  definition trunc_transport {a a' : A} {P : A → Type} (p : a = a') (n : ℕ₋₂) (x : P a)
-    : transport (λa, trunc n (P a)) p (tr x) = tr (p ▸ x) :=
-  by induction p; reflexivity
-
-  /- pathover over a truncated family -/
-  definition trunc_pathover {A : Type} {B : A → Type} {n : ℕ₋₂} {a a' : A} {p : a = a'}
-    {b : B a} {b' : B a'} (q : b =[p] b') : @tr n _ b =[p] @tr n _ b' :=
-  by induction q; constructor
-
   /- equivalences between truncated types (see also hit.trunc) -/
   definition trunc_trunc_equiv_left [constructor] (A : Type) (n m : ℕ₋₂) (H : n ≤ m)
     : trunc n (trunc m A) ≃ trunc n A :=
@@ -515,7 +516,6 @@ namespace trunc
       exact tr (fiber.mk (tr a) (ap tr p))}
   end
 
-
   /- the image of a map is the (-1)-truncated fiber -/
   definition image [constructor] {A B : Type} (f : A → B) (b : B) : Prop := ∥ fiber f b ∥
 
diff --git a/library/init/tactic.lean b/library/init/tactic.lean
index 83047789e..7fe558fd8 100644
--- a/library/init/tactic.lean
+++ b/library/init/tactic.lean
@@ -154,8 +154,9 @@ definition repeat1     (t : tactic) : tactic := and_then t (repeat t)
 definition focus       (t : tactic) : tactic := focus_at t 0
 definition determ      (t : tactic) : tactic := at_most t 1
 definition trivial                  : tactic := or_else (or_else (apply eq.refl) (apply true.intro)) assumption
-definition do (n : num) (t : tactic) : tactic :=
-nat.rec id (λn t', and_then t t') (nat.of_num n)
+definition do (n : nat) (t : tactic) : tactic :=
+nat.rec id (λn t', and_then t t') n
+
 end tactic
 tactic_infixl `;`:15 := tactic.and_then
 tactic_notation T1 `:`:15 T2 := tactic.focus (tactic.and_then T1 (tactic.all_goals T2))