diff --git a/hott/algebra/homotopy_group.hlean b/hott/algebra/homotopy_group.hlean
index 6a156f7757..c386ce9f8c 100644
--- a/hott/algebra/homotopy_group.hlean
+++ b/hott/algebra/homotopy_group.hlean
@@ -6,7 +6,7 @@ Authors: Floris van Doorn
 homotopy groups of a pointed space
 -/
 
-import types.pointed .trunc_group .hott types.trunc
+import .trunc_group .hott types.trunc
 
 open nat eq pointed trunc is_trunc algebra
 
@@ -45,6 +45,10 @@ namespace eq
 
   prefix `π₁`:95 := fundamental_group
 
+  definition phomotopy_group_pequiv [constructor] (n : ℕ) {A B : Type*} (H : A ≃* B)
+    : π*[n] A ≃* π*[n] B :=
+  ptrunc_pequiv 0 (iterated_loop_space_pequiv n H)
+
   open equiv unit
   theorem trivial_homotopy_of_is_set (A : Type*) [H : is_set A] (n : ℕ) : πg[n+1] A = G0 :=
   begin
@@ -54,12 +58,17 @@ namespace eq
     apply is_trunc_succ_succ_of_is_set
   end
 
-  definition homotopy_group_succ_out (A : Type*) (n : ℕ) : πg[ n +1] A = π₁ Ω[n] A := idp
+  definition phomotopy_group_succ_out (A : Type*) (n : ℕ) : π*[n + 1] A = π₁ Ω[n] A := idp
 
-  definition homotopy_group_succ_in (A : Type*) (n : ℕ) : πg[succ n +1] A = πg[n +1] Ω A :=
+  definition phomotopy_group_succ_in (A : Type*) (n : ℕ) : π*[n + 1] A = π*[n] Ω A :=
+  ap (ptrunc 0) (loop_space_succ_eq_in A n)
+
+  definition ghomotopy_group_succ_out (A : Type*) (n : ℕ) : πg[n +1] A = π₁ Ω[n] A := idp
+
+  definition ghomotopy_group_succ_in (A : Type*) (n : ℕ) : πg[succ n +1] A = πg[n +1] Ω A :=
   begin
     fapply Group_eq,
-    { apply equiv_of_eq, exact ap (λ(X : Type*), trunc 0 X) (loop_space_succ_eq_in A (succ n))},
+    { apply equiv_of_eq, exact ap (ptrunc 0) (loop_space_succ_eq_in A (succ n))},
     { exact abstract [irreducible] begin refine trunc.rec _, intro p, refine trunc.rec _, intro q,
       rewrite [▸*,-+tr_eq_cast_ap, +trunc_transport], refine !trunc_transport ⬝ _, apply ap tr,
       apply loop_space_succ_eq_in_concat end end},
@@ -69,18 +78,51 @@ namespace eq
   begin
     revert A, induction m with m IH: intro A,
     { reflexivity},
-    { esimp [iterated_ploop_space, nat.add], refine !homotopy_group_succ_in ⬝ _, refine !IH ⬝ _,
+    { esimp [iterated_ploop_space, nat.add], refine !ghomotopy_group_succ_in ⬝ _, refine !IH ⬝ _,
       exact ap (ghomotopy_group n) !loop_space_succ_eq_in⁻¹}
   end
 
-  theorem trivial_homotopy_of_is_set_loop_space {A : Type*} {n : ℕ} (m : ℕ) (H : is_set (Ω[n] A))
-    : πg[m+n+1] A = G0 :=
+  theorem trivial_homotopy_add_of_is_set_loop_space {A : Type*} {n : ℕ} (m : ℕ)
+    (H : is_set (Ω[n] A)) : πg[m+n+1] A = G0 :=
   !homotopy_group_add ⬝ !trivial_homotopy_of_is_set
 
+  theorem trivial_homotopy_le_of_is_set_loop_space {A : Type*} {n : ℕ} (m : ℕ) (H1 : n ≤ m)
+    (H2 : is_set (Ω[n] A)) : πg[m+1] A = G0 :=
+  obtain (k : ℕ) (p : n + k = m), from le.elim H1,
+  ap (λx, πg[x+1] A) (p⁻¹ ⬝ add.comm n k) ⬝ trivial_homotopy_add_of_is_set_loop_space k H2
+
   definition phomotopy_group_functor [constructor] (n : ℕ) {A B : Type*} (f : A →* B)
     : π*[n] A →* π*[n] B :=
   ptrunc_functor 0 (apn n f)
 
-  notation `π→*[`:95  n:0    `] `:0 f:95 := phomotopy_group_functor n f
+  definition homotopy_group_functor (n : ℕ) {A B : Type*} (f : A →* B) : π[n] A → π[n] B :=
+  phomotopy_group_functor n f
+
+  notation `π→*[`:95 n:0 `] `:0 f:95 := phomotopy_group_functor n f
+  notation `π→[`:95  n:0 `] `:0 f:95 :=  homotopy_group_functor n f
+
+  definition tinverse [constructor] {X : Type*} : π*[1] X →* π*[1] X :=
+  ptrunc_functor 0 pinverse
+
+  definition ptrunc_functor_pinverse [constructor] {X : Type*}
+    : ptrunc_functor 0 (@pinverse X) ~* @tinverse X :=
+  begin
+    fapply phomotopy.mk,
+    { reflexivity},
+    { reflexivity}
+  end
+
+  definition phomotopy_group_functor_mul [constructor] (n : ℕ) {A B : Type*} (g : A →* B)
+    (p q : πg[n+1] A) :
+    (π→[n + 1] g) (p *[πg[n+1] A] q) = (π→[n + 1] g) p *[πg[n+1] B] (π→[n + 1] g) q :=
+  begin
+    unfold [ghomotopy_group, homotopy_group] at *,
+    refine @trunc.rec _ _ _ (λq, !is_trunc_eq) _ p, clear p, intro p,
+    refine @trunc.rec _ _ _ (λq, !is_trunc_eq) _ q, clear q, intro q,
+    apply ap tr, apply apn_con
+  end
+
+
+
 
 end eq
diff --git a/hott/algebra/hott.hlean b/hott/algebra/hott.hlean
index 2fb73a5a2e..1eab2f9611 100644
--- a/hott/algebra/hott.hlean
+++ b/hott/algebra/hott.hlean
@@ -18,7 +18,7 @@ namespace algebra
   definition Trivial_group [constructor] : Group :=
   Group.mk _ trivial_group
 
-  notation `G0` := Trivial_group
+  abbreviation G0 := Trivial_group
 
   open Group has_mul has_inv
   -- we prove under which conditions two groups are equal
@@ -27,8 +27,8 @@ namespace algebra
   -- coercions between them anymore.
   -- So, an application such as (@mul A G g h) in the following definition
   -- is type incorrect if the coercion is not added (explicitly or implicitly).
-  definition group.to_has_mul [coercion] {A : Type} (H : group A) : has_mul A := _
-  local attribute group.to_has_inv [coercion]
+  definition group.to_has_mul {A : Type} (H : group A) : has_mul A := _
+  local attribute group.to_has_mul group.to_has_inv [coercion]
 
   universe variable l
   variables {A B : Type.{l}}
@@ -39,7 +39,7 @@ namespace algebra
       from λg, !mul_inv_cancel_right⁻¹,
     cases G with Gm Gs Gh1 G1 Gh2 Gh3 Gi Gh4,
     cases H with Hm Hs Hh1 H1 Hh2 Hh3 Hi Hh4,
-    rewrite [↑[semigroup.to_has_mul,group.to_has_inv] at (same_mul,foo)],
+    rewrite [↑[semigroup.to_has_mul,group.to_has_inv] at (same_mul',foo)],
     have same_mul : Gm = Hm, from eq_of_homotopy2 same_mul',
     cases same_mul,
     have same_one : G1 = H1, from calc
@@ -58,24 +58,24 @@ namespace algebra
     cases ps, cases ph1, cases ph2, cases ph3, cases ph4, reflexivity
   end
 
-  definition group_pathover {G : group A} {H : group B} {f : A ≃ B}
-    : (Π(g h : A), f (g * h) = f g * f h) → G =[ua f] H :=
+  definition group_pathover {G : group A} {H : group B} {p : A = B}
+    (resp_mul : Π(g h : A), cast p (g * h) = cast p g * cast p h) : G =[p] H :=
   begin
-    revert H,
-    eapply (rec_on_ua_idp' f),
-    intros H resp_mul,
-    esimp [equiv.refl] at resp_mul, esimp,
-    apply pathover_idp_of_eq, apply group_eq,
-    exact resp_mul
+    induction p,
+    apply pathover_idp_of_eq, exact group_eq (resp_mul)
+  end
+
+  definition Group_eq_of_eq {G H : Group} (p : carrier G = carrier H)
+    (resp_mul : Π(g h : G), cast p (g * h) = cast p g * cast p h) : G = H :=
+  begin
+    cases G with Gc G, cases H with Hc H,
+    apply (apo011 mk p),
+    exact group_pathover resp_mul
   end
 
   definition Group_eq {G H : Group} (f : carrier G ≃ carrier H)
     (resp_mul : Π(g h : G), f (g * h) = f g * f h) : G = H :=
-  begin
-    cases G with Gc G, cases H with Hc H,
-    apply (apo011 mk (ua f)),
-    apply group_pathover, exact resp_mul
-  end
+  Group_eq_of_eq (ua f) (λg h, !cast_ua ⬝ resp_mul g h ⬝ ap011 mul !cast_ua⁻¹ !cast_ua⁻¹)
 
   definition trivial_group_of_is_contr (G : Group) [H : is_contr G] : G = G0 :=
   begin
diff --git a/hott/hit/trunc.hlean b/hott/hit/trunc.hlean
index ea7b3d345c..0a123d4b92 100644
--- a/hott/hit/trunc.hlean
+++ b/hott/hit/trunc.hlean
@@ -57,13 +57,20 @@ namespace trunc
   definition trunc_functor [unfold 5] (f : X → Y) : trunc n X → trunc n Y :=
   λxx, trunc.rec_on xx (λx, tr (f x))
 
-  definition trunc_functor_compose (f : X → Y) (g : Y → Z)
+  definition trunc_functor_compose [unfold 7] (f : X → Y) (g : Y → Z)
     : trunc_functor n (g ∘ f) ~ trunc_functor n g ∘ trunc_functor n f :=
   λxx, trunc.rec_on xx (λx, idp)
 
   definition trunc_functor_id : trunc_functor n (@id A) ~ id :=
   λxx, trunc.rec_on xx (λx, idp)
 
+  definition trunc_functor_cast {X Y : Type} (n : ℕ₋₂) (p : X = Y) :
+    trunc_functor n (cast p) ~ cast (ap (trunc n) p) :=
+  begin
+    intro x, induction x with x, esimp,
+    exact fn_tr_eq_tr_fn p (λy, tr) x ⬝ !tr_compose
+  end
+
   definition is_equiv_trunc_functor [constructor] (f : X → Y) [H : is_equiv f]
     : is_equiv (trunc_functor n f) :=
   adjointify _
@@ -98,8 +105,11 @@ namespace trunc
 
   /- Propositional truncation -/
 
+  definition ttrunc [constructor] (n : ℕ₋₂) (X : Type) : n-Type :=
+  trunctype.mk (trunc n X) _
+
   -- should this live in Prop?
-  definition merely [reducible] [constructor] (A : Type) : Prop := trunctype.mk (trunc -1 A) _
+  definition merely [reducible] [constructor] (A : Type) : Prop := ttrunc -1 A
 
   notation `||`:max A `||`:0 := merely A
   notation `∥`:max A `∥`:0   := merely A
diff --git a/hott/homotopy/circle.hlean b/hott/homotopy/circle.hlean
index abbae11085..249d90b5f5 100644
--- a/hott/homotopy/circle.hlean
+++ b/hott/homotopy/circle.hlean
@@ -254,7 +254,7 @@ namespace circle
   open nat
   definition homotopy_group_of_circle (n : ℕ) : πg[n+1 +1] S¹. = G0 :=
   begin
-    refine @trivial_homotopy_of_is_set_loop_space S¹. 1 n _,
+    refine @trivial_homotopy_add_of_is_set_loop_space S¹. 1 n _,
     apply is_trunc_equiv_closed_rev, apply base_eq_base_equiv
   end
 
diff --git a/hott/homotopy/connectedness.hlean b/hott/homotopy/connectedness.hlean
index 459c0b0a97..e14a84bb39 100644
--- a/hott/homotopy/connectedness.hlean
+++ b/hott/homotopy/connectedness.hlean
@@ -171,7 +171,7 @@ namespace homotopy
         (Πa : A, P a) (unit → P (Point A)) (P (Point A))
         (λs x, s (Point A)) (λf, f unit.star)
         (is_conn_map.rec (is_conn_map_from_unit n A (Point A)) P)
-        (to_is_equiv (unit.unit_imp_equiv (P (Point A))))
+        (to_is_equiv (arrow_unit_left (P (Point A))))
 
       protected definition elim : P (Point A) → (Πa : A, P a) :=
       @is_equiv.inv _ _ (λs, s (Point A)) rec
@@ -191,7 +191,7 @@ namespace homotopy
         (fiber (λs x, s (Point A)) (λx, p))
         (fiber (λs, s (Point A)) p)
         k
-        (equiv.symm (fiber.equiv_postcompose (to_fun (unit.unit_imp_equiv (P (Point A))))))
+        (equiv.symm (fiber.equiv_postcompose (to_fun (arrow_unit_left (P (Point A))))))
         (is_conn_map.elim_general (is_conn_map_from_unit n A (Point A)) P (λx, p))
     end
   end is_conn
diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean
index 98edc28d37..fe51981691 100644
--- a/hott/init/equiv.hlean
+++ b/hott/init/equiv.hlean
@@ -328,7 +328,7 @@ namespace equiv
   equiv.mk (transport P p) !is_equiv_tr
 
   definition equiv_of_eq [constructor] {A B : Type} (p : A = B) : A ≃ B :=
-  equiv_ap (λX, X) p
+  equiv.mk (cast p) !is_equiv_tr
 
   definition eq_of_fn_eq_fn (f : A ≃ B) {x y : A} (q : f x = f y) : x = y :=
   (left_inv f x)⁻¹ ⬝ ap f⁻¹ q ⬝ left_inv f y
diff --git a/hott/init/path.hlean b/hott/init/path.hlean
index 9561099cc9..8680026961 100644
--- a/hott/init/path.hlean
+++ b/hott/init/path.hlean
@@ -499,7 +499,7 @@ namespace eq
   by induction r; exact !idp_con⁻¹
 
   definition fn_tr_eq_tr_fn {P Q : A → Type} {x y : A} (p : x = y) (f : Πx, P x → Q x) (z : P x) :
-    f y (p ▸ z) = (p ▸ (f x z)) :=
+    f y (p ▸ z) = p ▸ f x z :=
   by induction p; reflexivity
 
   /- Transporting in particular fibrations -/
diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean
index 4a55ffef94..5b2538ae8d 100644
--- a/hott/types/pointed.hlean
+++ b/hott/types/pointed.hlean
@@ -77,7 +77,7 @@ namespace pointed
   definition ploop_space [reducible] [constructor] (A : Type*) : Type* :=
   pointed.mk' (point A = point A)
 
-  definition iterated_ploop_space [unfold 1] [reducible] : ℕ → Type* → Type*
+  definition iterated_ploop_space [reducible] : ℕ → Type* → Type*
   | iterated_ploop_space  0    X := X
   | iterated_ploop_space (n+1) X := ploop_space (iterated_ploop_space n X)
 
@@ -357,39 +357,18 @@ namespace pointed
   { esimp [iterated_ploop_space], exact ap1 IH}
   end
 
+  prefix `Ω→`:(max+5) := ap1
+  notation `Ω→[`:95 n:0 `] `:0 f:95 := apn n f
+
+  definition apn_zero (f : map₊ A B) : Ω→[0] f = f := idp
+  definition apn_succ (n : ℕ) (f : map₊ A B) : Ω→[n + 1] f = ap1 (Ω→[n] f) := idp
+
   definition pcast [constructor] {A B : Type*} (p : A = B) : A →* B :=
   proof pmap.mk (cast (ap pType.carrier p)) (by induction p; reflexivity) qed
 
   definition pinverse [constructor] {X : Type*} : Ω X →* Ω X :=
   pmap.mk eq.inverse idp
 
-  /- properties about these instances -/
-
-  definition is_equiv_ap1 {A B : Type*} (f : A →* B) [is_equiv f] : is_equiv (ap1 f) :=
-  begin
-    induction B with B b, induction f with f pf, esimp at *, cases pf, esimp,
-    apply is_equiv.homotopy_closed (ap f),
-    intro p, exact !idp_con⁻¹
-  end
-
-  definition ap1_compose (g : B →* C) (f : A →* B) : ap1 (g ∘* f) ~* ap1 g ∘* ap1 f :=
-  begin
-    induction B, induction C, induction g with g pg, induction f with f pf, esimp at *,
-    induction pg, induction pf,
-    fconstructor,
-    { intro p, esimp, apply whisker_left, exact ap_compose g f p ⬝ ap (ap g) !idp_con⁻¹},
-    { reflexivity}
-  end
-
-  definition ap1_compose_pinverse (f : A →* B) : ap1 f ∘* pinverse ~* pinverse ∘* ap1 f :=
-  begin
-    fconstructor,
-    { intro p, esimp, refine !con.assoc ⬝ _ ⬝ !con_inv⁻¹, apply whisker_left,
-      refine whisker_right !ap_inv _ ⬝ _ ⬝ !con_inv⁻¹, apply whisker_left,
-      exact !inv_inv⁻¹},
-    { induction B with B b, induction f with f pf, esimp at *, induction pf, reflexivity},
-  end
-
   /- categorical properties of pointed homotopies -/
 
   protected definition phomotopy.refl [constructor] [refl] (f : A →* B) : f ~* f :=
@@ -420,6 +399,81 @@ namespace pointed
   infix ` ⬝* `:75 := phomotopy.trans
   postfix `⁻¹*`:(max+1) := phomotopy.symm
 
+  /- properties about the given pointed maps -/
+
+  definition is_equiv_ap1 {A B : Type*} (f : A →* B) [is_equiv f] : is_equiv (ap1 f) :=
+  begin
+    induction B with B b, induction f with f pf, esimp at *, cases pf, esimp,
+    apply is_equiv.homotopy_closed (ap f),
+    intro p, exact !idp_con⁻¹
+  end
+
+  definition is_equiv_apn {A B : Type*} (n : ℕ) (f : A →* B) [H : is_equiv f]
+    : is_equiv (apn n f) :=
+  begin
+    induction n with n IH,
+    { exact H},
+    { exact is_equiv_ap1 (apn n f)}
+  end
+
+  definition ap1_id [constructor] {A : Type*} : ap1 (pid A) ~* pid (Ω A) :=
+  begin
+    fapply phomotopy.mk,
+    { intro p, esimp, refine !idp_con ⬝ !ap_id},
+    { reflexivity}
+  end
+
+  definition ap1_pinverse {A : Type*} : ap1 (@pinverse A) ~* @pinverse (Ω A) :=
+  begin
+    fapply phomotopy.mk,
+    { intro p, esimp, refine !idp_con ⬝ _, exact !inverse_eq_inverse2⁻¹ },
+    { reflexivity}
+  end
+
+  definition ap1_compose (g : B →* C) (f : A →* B) : ap1 (g ∘* f) ~* ap1 g ∘* ap1 f :=
+  begin
+    induction B, induction C, induction g with g pg, induction f with f pf, esimp at *,
+    induction pg, induction pf,
+    fconstructor,
+    { intro p, esimp, apply whisker_left, exact ap_compose g f p ⬝ ap (ap g) !idp_con⁻¹},
+    { reflexivity}
+  end
+
+  definition ap1_compose_pinverse (f : A →* B) : ap1 f ∘* pinverse ~* pinverse ∘* ap1 f :=
+  begin
+    fconstructor,
+    { intro p, esimp, refine !con.assoc ⬝ _ ⬝ !con_inv⁻¹, apply whisker_left,
+      refine whisker_right !ap_inv _ ⬝ _ ⬝ !con_inv⁻¹, apply whisker_left,
+      exact !inv_inv⁻¹},
+    { induction B with B b, induction f with f pf, esimp at *, induction pf, reflexivity},
+  end
+
+  theorem ap1_con (f : A →* B) (p q : Ω A) : ap1 f (p ⬝ q) = ap1 f p ⬝ ap1 f q :=
+  begin
+    rewrite [▸*,ap_con, +con.assoc, con_inv_cancel_left], repeat apply whisker_left
+  end
+
+  theorem ap1_inv (f : A →* B) (p : Ω A) : ap1 f p⁻¹ = (ap1 f p)⁻¹ :=
+  begin
+    rewrite [▸*,ap_inv, +con_inv, inv_inv, +con.assoc], repeat apply whisker_left
+  end
+
+  definition pcast_ap_loop_space {A B : Type*} (p : A = B)
+    : pcast (ap ploop_space p) ~* Ω→ (pcast p) :=
+  begin
+    induction p, exact !ap1_id⁻¹*
+  end
+
+  definition pinverse_con [constructor] {X : Type*} (p q : Ω X)
+    : pinverse (p ⬝ q) = pinverse q ⬝ pinverse p :=
+  !con_inv
+
+  definition pinverse_inv [constructor] {X : Type*} (p : Ω X)
+    : pinverse p⁻¹ = (pinverse p)⁻¹ :=
+  idp
+
+  /- more on pointed homotopies -/
+
   definition phomotopy_of_eq [constructor] {A B : Type*} {f g : A →* B} (p : f = g) : f ~* g :=
   phomotopy.mk (ap010 pmap.to_fun p) begin induction p, apply idp_con end
 
@@ -452,20 +506,6 @@ namespace pointed
     (q : h ~* i) (p : f ~* g) : h ∘* f ~* i ∘* g :=
   pwhisker_left _ p ⬝* pwhisker_right _ q
 
-  definition ap1_pinverse {A : Type*} : ap1 (@pinverse A) ~* @pinverse (Ω A) :=
-  begin
-    fapply phomotopy.mk,
-    { intro p, esimp, refine !idp_con ⬝ _, exact !inverse_eq_inverse2⁻¹ },
-    { reflexivity}
-  end
-
-  definition ap1_id [constructor] {A : Type*} : ap1 (pid A) ~* pid (Ω A) :=
-  begin
-    fapply phomotopy.mk,
-    { intro p, esimp, refine !idp_con ⬝ !ap_id},
-    { reflexivity}
-  end
-
   definition eq_of_phomotopy (p : f ~* g) : f = g :=
   begin
     fapply pmap_eq,
@@ -497,6 +537,13 @@ namespace pointed
     { refine ap1_phomotopy IH ⬝* _, apply ap1_compose}
   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]
+
+  theorem apn_inv (n : ℕ)  (f : A →* B) (p : Ω[n+1] A) : apn (n+1) f p⁻¹ = (apn (n+1) f p)⁻¹ :=
+  by rewrite [+apn_succ, ap1_inv]
+
   infix ` ⬝*p `:75 := pconcat_eq
   infix ` ⬝p* `:75 := eq_pconcat
 
diff --git a/hott/types/pointed2.hlean b/hott/types/pointed2.hlean
index 081c025557..fabe736954 100644
--- a/hott/types/pointed2.hlean
+++ b/hott/types/pointed2.hlean
@@ -86,6 +86,9 @@ namespace pointed
   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 *,
diff --git a/hott/types/sum.hlean b/hott/types/sum.hlean
index 65042f410e..02fa076ae4 100644
--- a/hott/types/sum.hlean
+++ b/hott/types/sum.hlean
@@ -204,8 +204,8 @@ namespace sum
     A × (B + C) ≃ (A × B) + (A × C) :=
   calc A × (B + C) ≃ (B + C) × A : prod_comm_equiv
                ... ≃ (B × A) + (C × A) : sum_prod_right_distrib
-               ... ≃ (A × B) + (C × A) : prod_comm_equiv
-               ... ≃ (A × B) + (A × C) : prod_comm_equiv
+               ... ≃ (A × B) + (C × A) : sum_equiv_sum_right !prod_comm_equiv
+               ... ≃ (A × B) + (A × C) : sum_equiv_sum_left  !prod_comm_equiv
 
   section
   variables (H : unit + A ≃ unit + B)
diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean
index 2018b967bf..546d9d32bf 100644
--- a/hott/types/trunc.hlean
+++ b/hott/types/trunc.hlean
@@ -356,6 +356,14 @@ namespace is_trunc
     apply iff.mp !is_trunc_iff_is_contr_loop H
   end
 
+  theorem is_trunc_loop_of_is_trunc (n : ℕ₋₂) (k : ℕ) (A : Type*) [H : is_trunc n A] :
+    is_trunc n (Ω[k] A) :=
+  begin
+    induction k with k IH,
+    { exact H},
+    { apply is_trunc_eq}
+  end
+
 end is_trunc open is_trunc is_trunc.trunc_index
 
 namespace trunc
@@ -452,6 +460,10 @@ namespace trunc
     : ptrunc n X →* ptrunc n Y :=
   pmap.mk (trunc_functor n f) (ap tr (respect_pt f))
 
+  definition ptrunc_pequiv [constructor] (n : ℕ₋₂) {X Y : Type*} (H : X ≃* Y)
+    : ptrunc n X ≃* ptrunc n Y :=
+  pequiv_of_equiv (trunc_equiv_trunc n H) (ap tr (respect_pt H))
+
   definition loop_ptrunc_pequiv [constructor] (n : ℕ₋₂) (A : Type*) :
     Ω (ptrunc (n+1) A) ≃* ptrunc n (Ω A) :=
   pequiv_of_equiv !tr_eq_tr_equiv idp
@@ -467,12 +479,38 @@ namespace trunc
       rewrite succ_add_nat}
   end
 
+  definition ptrunc_functor_pcompose [constructor] {X Y Z : Type*} (n : ℕ₋₂) (g : Y →* Z)
+    (f : X →* Y) : ptrunc_functor n (g ∘* f) ~* ptrunc_functor n g ∘* ptrunc_functor n f :=
+  begin
+    fapply phomotopy.mk,
+    { apply trunc_functor_compose},
+    { esimp, refine !idp_con ⬝ _, refine whisker_right !ap_compose'⁻¹ᵖ _ ⬝ _,
+      esimp, refine whisker_right (ap_compose' tr g _) _ ⬝ _, exact !ap_con⁻¹},
+  end
+
+  definition ptrunc_functor_pid [constructor] (X : Type*) (n : ℕ₋₂) :
+    ptrunc_functor n (pid X) ~* pid (ptrunc n X) :=
+  begin
+    fapply phomotopy.mk,
+    { apply trunc_functor_id},
+    { reflexivity},
+  end
+
+  definition ptrunc_functor_pcast [constructor] {X Y : Type*} (n : ℕ₋₂) (p : X = Y) :
+    ptrunc_functor n (pcast p) ~* pcast (ap (ptrunc n) p) :=
+  begin
+    fapply phomotopy.mk,
+    { intro x, esimp, refine !trunc_functor_cast ⬝ _, refine ap010 cast _ x,
+      refine !ap_compose'⁻¹ ⬝ !ap_compose'},
+    { induction p, reflexivity},
+  end
+
 end trunc open trunc
 
 namespace function
   variables {A B : Type}
   definition is_surjective_of_is_equiv [instance] (f : A → B) [H : is_equiv f] : is_surjective f :=
-  λb, !center
+  λb, begin esimp, apply center end
 
   definition is_equiv_equiv_is_embedding_times_is_surjective [constructor] (f : A → B)
     : is_equiv f ≃ (is_embedding f × is_surjective f) :=
diff --git a/hott/types/unit.hlean b/hott/types/unit.hlean
index 090f14c734..7ce4d19ffc 100644
--- a/hott/types/unit.hlean
+++ b/hott/types/unit.hlean
@@ -13,7 +13,7 @@ namespace unit
   protected definition eta : Π(u : unit), ⋆ = u
   | eta ⋆ := idp
 
-  definition unit_equiv_option_empty : unit ≃ option empty :=
+  definition unit_equiv_option_empty [constructor] : unit ≃ option empty :=
   begin
     fapply equiv.MK,
     { intro u, exact none},
@@ -22,14 +22,8 @@ namespace unit
     { intro u, cases u, reflexivity},
   end
 
-  definition unit_imp_equiv (A : Type) : (unit → A) ≃ A :=
-  begin
-    fapply equiv.MK,
-    { intro f, exact f star},
-    { intro a u, exact a},
-    { intro a, reflexivity},
-    { intro f, apply eq_of_homotopy, intro u, cases u, reflexivity},
-  end
+  -- equivalences involving unit and other type constructors are in the file
+  -- of the other constructor
 
 end unit