diff --git a/hott/homotopy/quaternionic_hopf.hlean b/hott/homotopy/quaternionic_hopf.hlean
index 08e65736f..698a91a22 100644
--- a/hott/homotopy/quaternionic_hopf.hlean
+++ b/hott/homotopy/quaternionic_hopf.hlean
@@ -103,17 +103,14 @@ namespace hopf
   @h_space_equiv_closed (join S¹ S¹)
       (cd_h_space (S -1.+1) circle_assoc) (S 3) (join.spheres 1 1)
 
-  /- once we know that connectivity is downward closed,
-     we can replace this with an appeal to is_conn_sphere -/
   definition is_conn_sphere_three : is_conn 0 (S 3) :=
   begin
-    fapply is_contr.mk,
-    { exact tr (north : sphere -1.+2.+2) },
-    { intro x, induction x with x,
-      induction x with x,
-      { reflexivity },
-      { apply ap tr, exact merid (north : sphere -1.+2.+1) },
-      { apply is_prop.elimo }, }
+    have le02 : trunc_index.le 0 2,
+    from trunc_index.le.step
+      (trunc_index.le.step (trunc_index.le.tr_refl 0)),
+    exact @is_conn_of_le (S 3) 0 2 le02 (is_conn_sphere 3)
+    -- apply is_conn_of_le (S 3) le02
+    --   doesn't find is_conn_sphere instance
   end
 
   local attribute is_conn_sphere_three [instance]
@@ -125,4 +122,3 @@ namespace hopf
   end
 
 end hopf
-
diff --git a/hott/homotopy/sphere.hlean b/hott/homotopy/sphere.hlean
index fef6351a3..cfa080707 100644
--- a/hott/homotopy/sphere.hlean
+++ b/hott/homotopy/sphere.hlean
@@ -87,6 +87,13 @@ namespace sphere_index
   definition succ_sub_one (n : ℕ) : (nat.succ n)..-1 = n :> ℕ₋₁ :=
   idp
 
+  definition add_sub_one (n m : ℕ) : (n + m)..-1 = n..-1 +1+ m..-1 :> ℕ₋₁ :=
+  begin
+    induction m with m IH,
+    { reflexivity },
+    { exact ap succ IH }
+  end
+
   definition succ_le_succ {n m : ℕ₋₁} (H : n ≤ m) : n.+1 ≤[ℕ₋₁] m.+1 :=
   by induction H with m H IH; apply le.sp_refl; exact le.step IH
 
diff --git a/hott/homotopy/susp.hlean b/hott/homotopy/susp.hlean
index 0b45b000e..7593a460a 100644
--- a/hott/homotopy/susp.hlean
+++ b/hott/homotopy/susp.hlean
@@ -193,25 +193,33 @@ end susp
 
 namespace susp
   open pointed
-
-  variables {X Y Z : pType}
-
-  definition pointed_susp [instance] [constructor] (X : Type) : pointed (susp X) :=
+  definition pointed_susp [instance] [constructor] (X : Type)
+    : pointed (susp X) :=
   pointed.mk north
+end susp
 
-  definition psusp [constructor] (X : Type) : pType :=
-  pointed.mk' (susp X)
+open susp
+definition psusp [constructor] (X : Type) : pType :=
+pointed.mk' (susp X)
+
+namespace susp
+  open pointed
+  variables {X Y Z : pType}
 
   definition psusp_functor (f : X →* Y) : psusp X →* psusp Y :=
   begin
     fconstructor,
-    { intro x, induction x,
-        apply north,
-        apply south,
-        exact merid (f a)},
-    { reflexivity}
+    { exact susp.functor f },
+    { reflexivity }
   end
 
+  definition is_equiv_psusp_functor (f : X →* Y) [Hf : is_equiv f]
+    : is_equiv (psusp_functor f) :=
+  susp.is_equiv_functor f
+
+  definition psusp_equiv (f : X ≃* Y) : psusp X ≃* psusp Y :=
+  pequiv_of_equiv (susp.equiv f) idp
+
   definition psusp_functor_compose (g : Y →* Z) (f : X →* Y)
     : psusp_functor (g ∘* f) ~* psusp_functor g ∘* psusp_functor f :=
   begin