diff --git a/hott/book.md b/hott/book.md
index 0c0c02bee..bd4f1a17c 100644
--- a/hott/book.md
+++ b/hott/book.md
@@ -152,7 +152,7 @@ Every file is in the folder [homotopy](homotopy/homotopy.md)
 - 8.5 (The Hopf fibration): [hit.pushout](hit/pushout.hlean) (Lemma 8.5.3), [hopf](homotopy/hopf.hlean) (The Hopf construction, Lemmas 8.5.5 and 8.5.7), [susp](homotopy/susp.hlean) (Definition 8.5.6), [circle](homotopy/circle.hlean) (multiplication on the circle, Lemma 8.5.8), [join](homotopy/join.hlean) (join is associative, Lemma 8.5.9), [complex_hopf](homotopy/complex_hopf.hlean) (the H-space structure on the circle and the complex Hopf fibration, i.e. Theorem 8.5.1), [sphere2](homotopy/sphere2.hlean) (Corollary 8.5.2)
 - 8.6 (The Freudenthal suspension theorem): [connectedness](homotopy/connectedness.hlean) (Lemma 8.6.1), [wedge](homotopy/wedge.hlean) (Wedge connectivity, Lemma 8.6.2). Corollary 8.6.14 is proven directly in [freudenthal](homotopy/freudenthal.hlean), however, we don't prove Theorem 8.6.4. Stability of iterated suspensions is also in [freudenthal](homotopy/freudenthal.hlean). The homotopy groups of spheres in this section are computed in [sphere2](homotopy/sphere2.hlean).
 - 8.7 (The van Kampen theorem): [vankampen](homotopy/vankampen.hlean) (the pushout of Groupoids is formalized in [algebra.category.constructions.pushout](algebra/category/constructions/pushout.hlean), including the universal property of this pushout. Some preliminary definitions for this pushout are in [algebra.graph](algebra/graph.hlean))
-- 8.8 (Whitehead’s theorem and Whitehead’s principle): 8.8.1 and 8.8.2 at the bottom of [types.trunc](types/trunc.hlean), 8.8.3 in [homotopy_group](homotopy/homotopy_group.hlean). [Rest to be moved]
+- 8.8 (Whitehead’s theorem and Whitehead’s principle): 8.8.1 and 8.8.2 at the bottom of [types.trunc](types/trunc.hlean), 8.8.3-5 in [homotopy_group](homotopy/homotopy_group.hlean). Some properties of infinity-connected maps are also in [homotopy_group](homotopy/homotopy_group.hlean). Infinity-truncated types are not yet defined.
 - 8.9 (A general statement of the encode-decode method): [types.eq](types/eq.hlean).
 - 8.10 (Additional Results): Theorem 8.10.3 is formalized in [homotopy.EM](homotopy/EM.hlean).
 
diff --git a/hott/function.hlean b/hott/function.hlean
index 6363ff8ac..9d3440fac 100644
--- a/hott/function.hlean
+++ b/hott/function.hlean
@@ -300,6 +300,10 @@ namespace function
     ⦃a a' : A⦄ (p : g (f a) = g (f a')) : a = a' :=
   H₂ (H₁ p)
 
+  definition is_embedding_pr1 [instance] [constructor] {A : Type} (B : A → Type) [H : Π a, is_prop (B a)]
+      : is_embedding (@pr1 A B) :=
+  λv v', to_is_equiv (sigma_eq_equiv v v' ⬝e !sigma_equiv_of_is_contr_right)
+
   /-
     The definitions
       is_surjective_of_is_equiv
diff --git a/hott/homotopy/susp.hlean b/hott/homotopy/susp.hlean
index 4aa75c7ce..43c873417 100644
--- a/hott/homotopy/susp.hlean
+++ b/hott/homotopy/susp.hlean
@@ -223,7 +223,7 @@ namespace susp
     : is_equiv (psusp_functor f) :=
   susp.is_equiv_functor f
 
-  definition psusp_equiv [constructor] (f : X ≃* Y) : psusp X ≃* psusp Y :=
+  definition psusp_pequiv [constructor] (f : X ≃* Y) : psusp X ≃* psusp Y :=
   pequiv_of_equiv (susp.equiv f) idp
 
   definition psusp_functor_compose (g : Y →* Z) (f : X →* Y)
@@ -430,7 +430,7 @@ namespace susp
   begin
     induction n with n IH,
     { reflexivity},
-    { exact psusp_equiv IH}
+    { exact psusp_pequiv IH}
   end
 
   definition iterate_psusp_adjoint_loopn [constructor] (X Y : Type*) (n : ℕ) :
@@ -442,5 +442,4 @@ namespace susp
       symmetry, apply loopn_succ_in }
   end
 
-
 end susp
diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean
index 50accbea9..9a6d88164 100644
--- a/hott/types/pointed.hlean
+++ b/hott/types/pointed.hlean
@@ -387,7 +387,7 @@ namespace pointed
   definition eq_of_phomotopy' (p : f ~* g) : f = g :=
   to_inv (pmap_eq_equiv_internal f g) p
 
-  definition pmap_eq_equiv {A B : Type*} (f g : A →* B) : (f = g) ≃ (f ~* g) :=
+  definition pmap_eq_equiv [constructor] {A B : Type*} (f g : A →* B) : (f = g) ≃ (f ~* g) :=
   begin
     refine equiv_change_fun (pmap_eq_equiv_internal f g) _,
     { apply phomotopy_of_eq },