diff --git a/hott/algebra/homotopy_group.hlean b/hott/algebra/homotopy_group.hlean
index e5abcf3e3..6a6844d71 100644
--- a/hott/algebra/homotopy_group.hlean
+++ b/hott/algebra/homotopy_group.hlean
@@ -173,10 +173,9 @@ namespace eq
 
   definition is_equiv_homotopy_group_functor_ap1 (n : ℕ) {A B : Type*} (f : A →* B)
     [is_equiv (π→[n + 1] f)] : is_equiv (π→[n] (Ω→ f)) :=
-  have is_equiv (homotopy_group_succ_in B n ∘* π→[n + 1] f),
-  from is_equiv_compose _ (π→[n + 1] f),
   have is_equiv (π→[n] (Ω→ f) ∘ homotopy_group_succ_in A n),
-  from is_equiv.homotopy_closed _ (homotopy_group_functor_succ_phomotopy_in n f),
+  from is_equiv_of_equiv_of_homotopy (equiv.mk (π→[n+1] f) _ ⬝e homotopy_group_succ_in B n)
+                                     (homotopy_group_functor_succ_phomotopy_in n f),
   is_equiv.cancel_right (homotopy_group_succ_in A n) _
 
   definition tinverse [constructor] {X : Type*} : π[1] X →* π[1] X :=
diff --git a/hott/homotopy/EM.hlean b/hott/homotopy/EM.hlean
index adc51424a..a94413757 100644
--- a/hott/homotopy/EM.hlean
+++ b/hott/homotopy/EM.hlean
@@ -170,7 +170,7 @@ namespace EM
       { apply is_equiv_trunc_functor, esimp,
         apply is_equiv.homotopy_closed, rotate 1,
         { symmetry, exact phomotopy_pinv_right_of_phomotopy (loop_EM1_pmap _ _) },
-        apply is_equiv_compose e },
+        apply is_equiv_compose e, apply pequiv.to_is_equiv },
       { apply @is_equiv_of_is_contr,
         do 2 exact trivial_homotopy_group_of_is_trunc _ (succ_lt_succ !zero_lt_succ)}}
   end
@@ -360,7 +360,7 @@ namespace EM
     { cases H, esimp, apply is_equiv_trunc_functor, esimp,
       apply is_equiv.homotopy_closed, rotate 1,
       { symmetry, exact phomotopy_pinv_right_of_phomotopy (loopn_EMadd1_pmap' _ _) },
-      apply is_equiv_compose (e⁻¹ᵉ*)},
+      apply is_equiv_compose (e⁻¹ᵉ*), apply pequiv.to_is_equiv },
     { apply @is_equiv_of_is_contr,
       do 2 exact trivial_homotopy_group_of_is_trunc _ H}
   end
@@ -441,7 +441,7 @@ namespace EM
 
   definition EM1_functor [constructor] {G H : Group} (φ : G →g H) : EM1 G →* EM1 H :=
   begin
-    fconstructor,
+    fapply pmap.mk,
     { intro g, induction g,
       { exact base },
       { exact pth (φ g) },
diff --git a/hott/homotopy/LES_of_homotopy_groups.hlean b/hott/homotopy/LES_of_homotopy_groups.hlean
index 6e1a358af..c926fcb26 100644
--- a/hott/homotopy/LES_of_homotopy_groups.hlean
+++ b/hott/homotopy/LES_of_homotopy_groups.hlean
@@ -111,86 +111,34 @@ namespace chain_complex
   definition fiber_sequence : type_chain_complex.{0 u} +ℕ :=
   begin
     fconstructor,
-    { exact fiber_sequence_carrier},
-    { exact fiber_sequence_fun},
+    { exact fiber_sequence_carrier },
+    { exact fiber_sequence_fun },
     { intro n x, cases n with n,
-      { exact point_eq x},
-      { exact point_eq x}}
+      { exact point_eq x },
+      { exact point_eq x }}
   end
 
   definition is_exact_fiber_sequence : is_exact_t fiber_sequence :=
   λn x p, fiber.mk (fiber.mk x p) rfl
 
   /- (generalization of) Lemma 8.4.4(i)(ii) -/
-  definition fiber_sequence_carrier_equiv (n : ℕ)
-    : fiber_sequence_carrier (n+3) ≃ Ω(fiber_sequence_carrier n) :=
-  calc
-    fiber_sequence_carrier (n+3) ≃ fiber (fiber_sequence_fun (n+1)) pt : erfl
-    ... ≃ Σ(x : fiber_sequence_carrier _), fiber_sequence_fun (n+1) x = pt
-      : fiber.sigma_char
-    ... ≃ Σ(x : fiber (fiber_sequence_fun n) pt), fiber_sequence_fun _ x = pt
-      : erfl
-    ... ≃ Σ(v : Σ(x : fiber_sequence_carrier _), fiber_sequence_fun _ x = pt),
-            fiber_sequence_fun _ (fiber.mk v.1 v.2) = pt
-      : by exact sigma_equiv_sigma !fiber.sigma_char (λa, erfl)
-    ... ≃ Σ(v : Σ(x : fiber_sequence_carrier _), fiber_sequence_fun _ x = pt),
-            v.1 = pt
-      : erfl
-    ... ≃ Σ(v : Σ(x : fiber_sequence_carrier _), x = pt),
-            fiber_sequence_fun _ v.1 = pt
-      : sigma_assoc_comm_equiv
-    ... ≃ fiber_sequence_fun _ !center.1 = pt
-      : @(sigma_equiv_of_is_contr_left _) !is_contr_sigma_eq'
-    ... ≃ fiber_sequence_fun _ pt = pt
-      : erfl
-    ... ≃ pt = pt
-      : by exact !equiv_eq_closed_left !respect_pt
-    ... ≃ Ω(fiber_sequence_carrier n) : erfl
-
-  /- computation rule -/
-  definition fiber_sequence_carrier_equiv_eq (n : ℕ)
-    (x : fiber_sequence_carrier (n+1)) (p : fiber_sequence_fun n x = pt)
-    (q : fiber_sequence_fun (n+1) (fiber.mk x p) = pt)
-    : fiber_sequence_carrier_equiv n (fiber.mk (fiber.mk x p) q)
-      = !respect_pt⁻¹ ⬝ ap (fiber_sequence_fun n) q⁻¹ ⬝ p :=
-  begin
-    refine _ ⬝ !con.assoc⁻¹,
-    apply whisker_left,
-    refine eq_transport_Fl _ _ ⬝ _,
-    apply whisker_right,
-    refine inverse2 !ap_inv ⬝ !inv_inv ⬝ _,
-    refine ap_compose (fiber_sequence_fun n) pr₁ _ ⬝
-           ap02 (fiber_sequence_fun n) !ap_pr1_center_eq_sigma_eq',
-  end
-
-  definition fiber_sequence_carrier_equiv_inv_eq (n : ℕ)
-    (p : Ω(fiber_sequence_carrier n)) : (fiber_sequence_carrier_equiv n)⁻¹ᵉ p =
-      fiber.mk (fiber.mk pt (respect_pt (fiber_sequence_fun n) ⬝ p)) idp :=
-  begin
-    apply inv_eq_of_eq,
-    refine _ ⬝ !fiber_sequence_carrier_equiv_eq⁻¹, esimp,
-    exact !inv_con_cancel_left⁻¹
-  end
-
   definition fiber_sequence_carrier_pequiv (n : ℕ)
     : fiber_sequence_carrier (n+3) ≃* Ω(fiber_sequence_carrier n) :=
-  pequiv_of_equiv (fiber_sequence_carrier_equiv n)
-    begin
-      esimp,
-      apply con.left_inv
-    end
+  pfiber_ppoint_pequiv (fiber_sequence_fun n)
 
   definition fiber_sequence_carrier_pequiv_eq (n : ℕ)
     (x : fiber_sequence_carrier (n+1)) (p : fiber_sequence_fun n x = pt)
     (q : fiber_sequence_fun (n+1) (fiber.mk x p) = pt)
     : fiber_sequence_carrier_pequiv n (fiber.mk (fiber.mk x p) q)
       = !respect_pt⁻¹ ⬝ ap (fiber_sequence_fun n) q⁻¹ ⬝ p :=
-  fiber_sequence_carrier_equiv_eq n x p q
+  fiber_ppoint_equiv_eq p q
 
   definition fiber_sequence_carrier_pequiv_inv_eq (n : ℕ)
     (p : Ω(fiber_sequence_carrier n)) : (fiber_sequence_carrier_pequiv n)⁻¹ᵉ* p =
       fiber.mk (fiber.mk pt (respect_pt (fiber_sequence_fun n) ⬝ p)) idp :=
-  by rexact fiber_sequence_carrier_equiv_inv_eq n p
+  fiber_ppoint_equiv_inv_eq (fiber_sequence_fun n) p
+
+  /- TODO: prove naturality of pfiber_ppoint_pequiv in general -/
 
   /- Lemma 8.4.4(iii) -/
   definition fiber_sequence_fun_eq_helper (n : ℕ)
@@ -198,7 +146,7 @@ namespace chain_complex
     fiber_sequence_carrier_pequiv n
       (fiber_sequence_fun (n + 3)
         ((fiber_sequence_carrier_pequiv (n + 1))⁻¹ᵉ* p)) =
-          ap1 (fiber_sequence_fun n) p⁻¹ :=
+          Ω→ (fiber_sequence_fun n) p⁻¹ :=
   begin
     refine ap (λx, fiber_sequence_carrier_pequiv n (fiber_sequence_fun (n + 3) x))
               (fiber_sequence_carrier_pequiv_inv_eq (n+1) p) ⬝ _,
@@ -233,7 +181,7 @@ namespace chain_complex
     (fiber_sequence_carrier_pequiv n ∘*
       fiber_sequence_fun (n + 3)) ∘*
         (fiber_sequence_carrier_pequiv (n + 1))⁻¹ᵉ* ~*
-          ap1 (fiber_sequence_fun n) ∘* pinverse :=
+          Ω→ (fiber_sequence_fun n) ∘* pinverse :=
   begin
     fapply phomotopy.mk,
     { exact chain_complex.fiber_sequence_fun_eq_helper f n},
@@ -245,7 +193,7 @@ namespace chain_complex
 
   theorem fiber_sequence_fun_eq (n : ℕ) : Π(x : fiber_sequence_carrier (n + 4)),
     fiber_sequence_carrier_pequiv n (fiber_sequence_fun (n + 3) x) =
-      ap1 (fiber_sequence_fun n) (fiber_sequence_carrier_pequiv (n + 1) x)⁻¹ :=
+      Ω→ (fiber_sequence_fun n) (fiber_sequence_carrier_pequiv (n + 1) x)⁻¹ :=
   begin
     refine @(homotopy_of_inv_homotopy_pre (fiber_sequence_carrier_pequiv (n + 1)))
              !pequiv.to_is_equiv _ _ _,
@@ -255,7 +203,7 @@ namespace chain_complex
   theorem fiber_sequence_fun_phomotopy (n : ℕ) :
     fiber_sequence_carrier_pequiv n ∘*
       fiber_sequence_fun (n + 3) ~*
-          (ap1 (fiber_sequence_fun n) ∘* pinverse) ∘* fiber_sequence_carrier_pequiv (n + 1) :=
+          (Ω→ (fiber_sequence_fun n) ∘* pinverse) ∘* fiber_sequence_carrier_pequiv (n + 1) :=
   begin
     apply phomotopy_of_pinv_right_phomotopy,
     apply fiber_sequence_fun_phomotopy_helper
@@ -268,7 +216,7 @@ namespace chain_complex
     PART 2
  --------------/
 
-  /- Now we are ready to define the long exact sequence of homotopy groups.
+  /- Now we are ready to define the long exact sequence of loop spaces.
      First we define its carrier -/
   definition loop_spaces : ℕ → Type*
   | 0     := Y
@@ -277,16 +225,15 @@ namespace chain_complex
   | (k+3) := Ω (loop_spaces k)
 
   /- The maps between the homotopy groups -/
-  definition loop_spaces_fun
-    : Π(n : ℕ), loop_spaces (n+1) →* loop_spaces n
+  definition loop_spaces_fun : Π(n : ℕ), loop_spaces (n+1) →* loop_spaces n
   | 0     := proof f qed
   | 1     := proof ppoint f qed
   | 2     := proof boundary_map qed
-  | (k+3) := proof ap1 (loop_spaces_fun k) qed
+  | (k+3) := proof Ω→ (loop_spaces_fun k) qed
 
   definition loop_spaces_fun_add3 [unfold_full] (n : ℕ) :
-    loop_spaces_fun (n + 3) = ap1 (loop_spaces_fun n) :=
-  proof idp qed
+    loop_spaces_fun (n + 3) = Ω→ (loop_spaces_fun n) :=
+  idp
 
   definition fiber_sequence_pequiv_loop_spaces :
     Πn, fiber_sequence_carrier n ≃* loop_spaces n
@@ -302,11 +249,11 @@ namespace chain_complex
 
   definition fiber_sequence_pequiv_loop_spaces_add3 (n : ℕ)
     : fiber_sequence_pequiv_loop_spaces (n + 3) =
-      ap1 (fiber_sequence_pequiv_loop_spaces n) ∘* fiber_sequence_carrier_pequiv n :=
+      Ω→ (fiber_sequence_pequiv_loop_spaces n) ∘* fiber_sequence_carrier_pequiv n :=
   by reflexivity
 
   definition fiber_sequence_pequiv_loop_spaces_3_phomotopy
-    : fiber_sequence_pequiv_loop_spaces 3 ~* proof fiber_sequence_carrier_pequiv nat.zero qed :=
+    : fiber_sequence_pequiv_loop_spaces 3 ~* fiber_sequence_carrier_pequiv 0 :=
   begin
     refine pwhisker_right _ ap1_pid ⬝* _,
     apply pid_pcompose
@@ -323,31 +270,9 @@ namespace chain_complex
     : pid_or_pinverse (n + 4) = !pequiv_pinverse ⬝e* loop_pequiv_loop (pid_or_pinverse (n + 1)) :=
   by reflexivity
 
-  definition pid_or_pinverse_add4_rev : Π(n : ℕ),
-    pid_or_pinverse (n + 4) ~* pinverse ∘* Ω→(pid_or_pinverse (n + 1))
-  | 0     := begin rewrite [pid_or_pinverse_add4, + to_pmap_pequiv_trans],
-                   replace pid_or_pinverse (0 + 1) with pequiv.refl X,
-                   refine pwhisker_right _ !loop_pequiv_loop_rfl ⬝* _, refine !pid_pcompose ⬝* _,
-                   exact !pcompose_pid⁻¹* ⬝* pwhisker_left _ !ap1_pid⁻¹* end
-  | 1     := begin rewrite [pid_or_pinverse_add4, + to_pmap_pequiv_trans],
-                   replace pid_or_pinverse (1 + 1) with pequiv.refl (pfiber f),
-                   refine pwhisker_right _ !loop_pequiv_loop_rfl ⬝* _, refine !pid_pcompose ⬝* _,
-                   exact !pcompose_pid⁻¹* ⬝* pwhisker_left _ !ap1_pid⁻¹* end
-  | 2     := begin rewrite [pid_or_pinverse_add4, + to_pmap_pequiv_trans],
-                   replace pid_or_pinverse (2 + 1) with pequiv.refl (Ω Y),
-                   refine pwhisker_right _ !loop_pequiv_loop_rfl ⬝* _, refine !pid_pcompose ⬝* _,
-                   exact !pcompose_pid⁻¹* ⬝* pwhisker_left _ !ap1_pid⁻¹* end
-  | (k+3) :=
-    begin
-      replace (k + 3 + 1) with (k + 4),
-      rewrite [+ pid_or_pinverse_add4, + to_pmap_pequiv_trans],
-      refine _ ⬝* pwhisker_left _ !ap1_pcompose⁻¹*,
-      refine _ ⬝* !passoc,
-      apply pconcat2,
-      { refine ap1_phomotopy (pid_or_pinverse_add4_rev k) ⬝* _,
-        refine !ap1_pcompose ⬝* _, apply pwhisker_right, apply ap1_pinverse},
-      { refine !ap1_pinverse⁻¹*}
-    end
+  definition pid_or_pinverse_add4_rev (n : ℕ) :
+    pid_or_pinverse (n + 4) ~* pinverse ∘* Ω→(pid_or_pinverse (n + 1)) :=
+  !ap1_pcompose_pinverse
 
   theorem fiber_sequence_phomotopy_loop_spaces : Π(n : ℕ),
     fiber_sequence_pequiv_loop_spaces n ∘* fiber_sequence_fun n ~*
@@ -360,7 +285,7 @@ namespace chain_complex
       replace loop_spaces_fun 2 with boundary_map,
       refine _ ⬝* pwhisker_left _ fiber_sequence_pequiv_loop_spaces_3_phomotopy⁻¹*,
       apply phomotopy_of_pinv_right_phomotopy,
-      exact !pid_pcompose⁻¹*
+      exact !pcompose_pid⁻¹*
     end
   | (k+3) :=
     begin
@@ -435,7 +360,7 @@ namespace chain_complex
   | (k+4) :=
     begin
       replace (k + 4 + 1) with (k + 5),
-      rewrite [pid_or_pinverse_left_add5, pid_or_pinverse_add4, to_pmap_pequiv_trans],
+      rewrite [pid_or_pinverse_left_add5, pid_or_pinverse_add4],
       replace (k + 4) with (k + 1 + 3),
       rewrite [loop_spaces_fun_add3],
       refine !passoc⁻¹* ⬝* _ ⬝* !passoc⁻¹*,
diff --git a/hott/homotopy/chain_complex.hlean b/hott/homotopy/chain_complex.hlean
index 9959c3ad5..2e643827c 100644
--- a/hott/homotopy/chain_complex.hlean
+++ b/hott/homotopy/chain_complex.hlean
@@ -217,17 +217,17 @@ namespace chain_complex
     (p : Π{m} (x : X (S (f m))), e (tcc_to_fn X (f m) x) = g (e (cast (ap (λx, X x) (c m)) x)))
     : type_chain_complex M :=
   type_chain_complex.mk Y @g
-    begin
+    abstract begin
       intro m,
       apply equiv_rect (equiv_of_pequiv e),
       apply equiv_rect (equiv_of_eq (ap (λx, X x) (c (S m)))), esimp,
       apply equiv_rect (equiv_of_eq (ap (λx, X (S x)) (c m))), esimp,
       intro x, refine ap g (p _)⁻¹ ⬝ _,
-      refine ap g (ap e (fn_cast_eq_cast_fn (c m) (tcc_to_fn X) x)) ⬝ _,
+      refine ap g (ap e (fn_cast_eq_cast_fn (c m) (λn, pmap.to_fun (tcc_to_fn X n)) x)) ⬝ _,
       refine (p _)⁻¹ ⬝ _,
       refine ap e (tcc_is_chain_complex X (f m) _) ⬝ _,
       apply respect_pt
-    end
+    end end
 
   definition is_exact_at_t_transfer2 {X : type_chain_complex N} {M : succ_str} {Y : M → Type*}
     (f : M ≃ N) (c : Π(m : M), S (f m) = f (S m))
@@ -246,11 +246,11 @@ namespace chain_complex
     induction (H _ H2) with x r,
     refine fiber.mk (e (cast (ap (λx, X x) (c (S m))) (cast (ap (λx, X (S x)) (c m)) x))) _,
     refine (p _)⁻¹ ⬝ _,
-    refine ap e (fn_cast_eq_cast_fn (c m) (tcc_to_fn X) x) ⬝ _,
+    refine ap e (fn_cast_eq_cast_fn (c m) (λn, pmap.to_fun (tcc_to_fn X n)) x) ⬝ _,
     refine ap (λx, e (cast _ x)) r ⬝ _,
     esimp [equiv.symm], rewrite [-ap_inv],
     refine ap e !cast_cast_inv ⬝ _,
-    apply right_inv
+    apply to_right_inv
   end
 
   end
@@ -355,7 +355,7 @@ namespace chain_complex
 
   definition transfer_chain_complex2 [constructor] {M : succ_str} {Y : M → Set*}
     (f : N ≃ M) (c : Π(n : N), f (S n) = S (f n))
-    (g : Π{m : M}, Y (S m) →* Y m) (e : Π{n}, X n ≃* Y (f n))
+    (g : Π{m : M}, pmap (Y (S m)) (Y m)) (e : Π{n}, X n ≃* Y (f n))
     (p : Π{n} (x : X (S n)), e (cc_to_fn X n x) = g (c n ▸ e x)) : chain_complex M :=
   chain_complex.mk Y @g
     begin
@@ -371,7 +371,8 @@ namespace chain_complex
       refine pi.pi_functor _ _ H,
       { intro x, exact (c (S n))⁻¹ ▸ (c n)⁻¹ ▸ x}, -- with implicit arguments, this is:
       -- transport (λx, Y x) (c (S n))⁻¹ (transport (λx, Y (S x)) (c n)⁻¹ x)
-      { intro x, intro p, refine _ ⬝ p, rewrite [tr_inv_tr, fn_tr_eq_tr_fn (c n)⁻¹ @g, tr_inv_tr]}
+      { intro x, intro p, refine _ ⬝ p,
+        rewrite [tr_inv_tr, fn_tr_eq_tr_fn (c n)⁻¹ᵖ (λn, ppi.to_fun g), tr_inv_tr]}
     end
 
   definition is_exact_at_transfer2 {X : chain_complex N} {M : succ_str} {Y : M → Set*}
@@ -389,7 +390,7 @@ namespace chain_complex
     end,
     induction (H _ H2) with x r,
     refine image.mk (c n ▸ c (S n) ▸ e x) _,
-    rewrite [fn_tr_eq_tr_fn (c n) @g],
+    rewrite [fn_tr_eq_tr_fn (c n) (λn, ppi.to_fun g)],
     refine ap (λx, c n ▸ x) (p x)⁻¹ ⬝ _,
     refine ap (λx, c n ▸ e x) r ⬝ _,
     refine ap (λx, c n ▸ x) !right_inv ⬝ _,
diff --git a/hott/homotopy/cofiber.hlean b/hott/homotopy/cofiber.hlean
index adba6a1d3..007d9ed02 100644
--- a/hott/homotopy/cofiber.hlean
+++ b/hott/homotopy/cofiber.hlean
@@ -95,7 +95,7 @@ namespace cofiber
   definition pcofiber_punit (A : Type*) : pcofiber (pconst A punit) ≃* susp A :=
   begin
     fapply pequiv_of_pmap,
-    { fconstructor, intro x, induction x, exact north, exact south, exact merid x,
+    { fapply pmap.mk, intro x, induction x, exact north, exact south, exact merid x,
       exact (merid pt)⁻¹ },
     { esimp, fapply adjointify,
       { intro s, induction s, exact inl ⋆, exact inr ⋆, apply glue a },
diff --git a/hott/homotopy/homotopy_group.hlean b/hott/homotopy/homotopy_group.hlean
index 448c8f404..73e3a12f8 100644
--- a/hott/homotopy/homotopy_group.hlean
+++ b/hott/homotopy/homotopy_group.hlean
@@ -134,6 +134,7 @@ namespace is_trunc
            pmap.to_fun (π→[k + 1] (pmap_of_map (ap f) p))),
       begin
         apply is_equiv_compose, exact this a p,
+        apply is_equiv_trunc_functor
       end,
       apply is_equiv.homotopy_closed, exact this,
       refine !homotopy_group_functor_compose⁻¹* ⬝* _,
@@ -151,6 +152,7 @@ namespace is_trunc
   begin
     apply whitehead_principle n, rexact H 0,
     intro a k, revert a, apply is_conn.elim -1,
+    { intro a, apply is_prop_is_equiv },
     have is_equiv (π→[k + 1] (pointed_eta_pequiv B ⬝e* (pequiv_of_eq_pt (respect_pt f))⁻¹ᵉ*)
            ∘* π→[k + 1] f ∘* π→[k + 1] (pointed_eta_pequiv A)⁻¹ᵉ*),
     begin
diff --git a/hott/homotopy/sphere.hlean b/hott/homotopy/sphere.hlean
index 9f8551aa9..129880d34 100644
--- a/hott/homotopy/sphere.hlean
+++ b/hott/homotopy/sphere.hlean
@@ -104,7 +104,7 @@ namespace is_trunc
     apply is_trunc_equiv_closed, exact !sphere_pmap_pequiv,
     fapply is_contr.mk,
     { exact pmap.mk (λx, a) idp},
-    { intro f, fapply pmap_eq,
+    { intro f, apply eq_of_phomotopy, fapply phomotopy.mk,
       { intro x, esimp, refine !respect_pt⁻¹ ⬝ (!H ⬝ !H⁻¹)},
       { rewrite [▸*,con.right_inv,▸*,con.left_inv]}}
   end
@@ -120,10 +120,10 @@ namespace is_trunc
     (a : A) (f : S n →* pointed.Mk a) (x : S n) : f x = f pt :=
   begin
     let H' := iff.elim_left (is_trunc_iff_is_contr_loop n A) H a,
-    note H'' := @is_trunc_equiv_closed_rev _ _ _ !sphere_pmap_pequiv H',
-    esimp at H'',
+    have H'' : is_contr (S n →* pointed.Mk a), from
+      @is_trunc_equiv_closed_rev _ _ _ !sphere_pmap_pequiv H',
     have p : f = pmap.mk (λx, f pt) (respect_pt f),
-      by apply is_prop.elim,
+      from !is_prop.elim,
     exact ap10 (ap pmap.to_fun p) x
   end
 
diff --git a/hott/homotopy/sphere2.hlean b/hott/homotopy/sphere2.hlean
index 04569477e..7ed5442b3 100644
--- a/hott/homotopy/sphere2.hlean
+++ b/hott/homotopy/sphere2.hlean
@@ -20,7 +20,7 @@ namespace sphere
   /- Corollaries of the complex hopf fibration combined with the LES of homotopy groups -/
   open sphere sphere.ops int circle hopf
 
-  definition π2S2 : πg[1+1] (S 2) ≃g gℤ :=
+  definition π2S2 : πg[2] (S 2) ≃g gℤ :=
   begin
     refine _ ⬝g fundamental_group_of_circle,
     refine _ ⬝g homotopy_group_isomorphism_of_pequiv _ pfiber_complex_hopf,
@@ -37,7 +37,7 @@ namespace sphere
   end
 
   open circle
-  definition πnS3_eq_πnS2 (n : ℕ) : πg[n+2 +1] (S 3) ≃g πg[n+2 +1] (S 2) :=
+  definition πnS3_eq_πnS2 (n : ℕ) : πg[n+3] (S 3) ≃g πg[n+3] (S 2) :=
   begin
     fapply isomorphism_of_equiv,
     { fapply equiv.mk,
@@ -63,8 +63,9 @@ namespace sphere
   iterate_susp_stability_isomorphism pbool H
 
   open int circle hopf
-  definition πnSn (n : ℕ) : πg[n+1] (S (n+1)) ≃g gℤ :=
+  definition πnSn (n : ℕ) [H : is_succ n] : πg[n] (S (n)) ≃g gℤ :=
   begin
+    induction H with n,
     cases n with n IH,
     { exact fundamental_group_of_circle },
     { induction n with n IH,
@@ -77,13 +78,15 @@ namespace sphere
   begin
     intro H,
     note H2 := trivial_ghomotopy_group_of_is_trunc (S (n+1)) n n !le.refl,
-    have H3 : is_contr ℤ, from is_trunc_equiv_closed _ (equiv_of_isomorphism (πnSn n)),
+    have H3 : is_contr ℤ, from is_trunc_equiv_closed _ (equiv_of_isomorphism (πnSn (n+1))),
     have H4 : (0 : ℤ) ≠ (1 : ℤ), from dec_star,
     apply H4,
     apply is_prop.elim,
   end
 
-  definition π3S2 : πg[2+1] (S 2) ≃g gℤ :=
-  (πnS3_eq_πnS2 0)⁻¹ᵍ ⬝g πnSn 2
+  definition π3S2 : πg[3] (S 2) ≃g gℤ :=
+  begin
+    refine _ ⬝g πnSn 3, symmetry, rexact πnS3_eq_πnS2 0
+  end
 
 end sphere
diff --git a/hott/homotopy/susp.hlean b/hott/homotopy/susp.hlean
index a094903c8..6e3af5421 100644
--- a/hott/homotopy/susp.hlean
+++ b/hott/homotopy/susp.hlean
@@ -288,7 +288,7 @@ namespace susp
 
   definition loop_susp_counit [constructor] (X : Type*) : susp (Ω X) →* X :=
   begin
-    fconstructor,
+    fapply pmap.mk,
     { intro x, induction x, exact pt, exact pt, exact a },
     { reflexivity },
   end
diff --git a/hott/init/pointed.hlean b/hott/init/pointed.hlean
index b069e1c16..13b86e208 100644
--- a/hott/init/pointed.hlean
+++ b/hott/init/pointed.hlean
@@ -100,12 +100,20 @@ pointed.MK (pppi' P) (ppi_const P)
 notation `Π*` binders `, ` r:(scoped P, pppi P) := r
 
 -- We could try to define pmap as a special case of ppi
--- definition pmap (A B : Type*) := @ppi A (λa, B)
-structure pmap (A B : Type*) :=
-  (to_fun : A → B)
-  (resp_pt : to_fun (Point A) = Point B)
+-- definition pmap' (A B : Type*) : Type := @pppi' A (λa, B)
+-- todo: make this already pointed?
+definition pmap [reducible] (A B : Type*) : Type := @pppi A (λa, B)
+-- structure pmap (A B : Type*) :=
+--   (to_fun : A → B)
+--   (resp_pt : to_fun (Point A) = Point B)
 
 namespace pointed
+
+  attribute ppi.to_fun [coercion]
+
+  notation `map₊` := pmap
+  infix ` →* `:28 := pmap
+
   definition pppi.mk [constructor] [reducible] {A : Type*} {P : A → Type*} (f : Πa, P a)
     (p : f pt = pt) : pppi P :=
   ppi.mk f p
@@ -114,14 +122,17 @@ namespace pointed
     (a : A) : P a :=
   ppi.to_fun f a
 
-  definition pppi.resp_pt [unfold 3] [reducible] {A : Type*} {P : A → Type*} (f : pppi P) :
-    f pt = pt :=
+	definition pmap.mk [constructor] [reducible] {A B : Type*} (f : A → B)
+    (p : f (Point A) = Point B) : A →* B :=
+	pppi.mk f p
+
+  definition pmap.to_fun [unfold 3] [reducible] {A B : Type*} (f : A →* B) : A → B :=
+  pppi.to_fun f
+
+  definition respect_pt [unfold 4] [reducible] {A : Type*} {P : A → Type} {p₀ : P pt}
+    (f : ppi P p₀) : f pt = p₀ :=
   ppi.resp_pt f
 
-  abbreviation respect_pt [unfold 3] := @pmap.resp_pt
-  notation `map₊` := pmap
-  infix ` →* `:28 := pmap
-  attribute pmap.to_fun ppi.to_fun [coercion]
   -- notation `Π*` binders `, ` r:(scoped P, ppi _ P) := r
   -- definition pmxap.mk [constructor] {A B : Type*} (f : A → B) (p : f pt = pt) : A →* B :=
   -- ppi.mk f p
@@ -130,7 +141,7 @@ namespace pointed
 end pointed open pointed
 
 /- pointed homotopies -/
-definition phomotopy {A B : Type*} (f g : A →* B) : Type :=
+definition phomotopy {A : Type*} {P : A → Type} {p₀ : P pt} (f g : ppi P p₀) : Type :=
 ppi (λa, f a = g a) (respect_pt f ⬝ (respect_pt g)⁻¹)
 
 -- structure phomotopy {A B : Type*} (f g : A →* B) : Type :=
@@ -138,7 +149,7 @@ ppi (λa, f a = g a) (respect_pt f ⬝ (respect_pt g)⁻¹)
 --   (homotopy_pt : homotopy pt ⬝ respect_pt g = respect_pt f)
 
 namespace pointed
-  variables {A B : Type*} {f g : A →* B}
+  variables {A : Type*} {P : A → Type} {p₀ : P pt} {f g : ppi P p₀}
 
   infix ` ~* `:50 := phomotopy
   definition phomotopy.mk [reducible] [constructor] (h : f ~ g)
@@ -148,7 +159,7 @@ namespace pointed
   definition to_homotopy [coercion] [unfold 5] [reducible] (p : f ~* g) : Πa, f a = g a := p
   definition to_homotopy_pt [unfold 5] [reducible] (p : f ~* g) :
     p pt ⬝ respect_pt g = respect_pt f :=
-  con_eq_of_eq_con_inv (ppi.resp_pt p)
+  con_eq_of_eq_con_inv (respect_pt p)
 
 
 end pointed
diff --git a/hott/types/fiber.hlean b/hott/types/fiber.hlean
index 0cf58c340..65a2e07e2 100644
--- a/hott/types/fiber.hlean
+++ b/hott/types/fiber.hlean
@@ -8,7 +8,7 @@ Theorems about fibers
 -/
 
 import .sigma .eq .pi cubical.squareover .pointed .eq
-open equiv sigma sigma.ops eq pi pointed
+open equiv sigma sigma.ops eq pi pointed is_equiv
 
 structure fiber {A B : Type} (f : A → B) (b : B) :=
   (point : A)
@@ -170,7 +170,9 @@ namespace fiber
     fapply pequiv_of_equiv, esimp,
     refine transport_fiber_equiv (g ∘* f) (respect_pt g)⁻¹ ⬝e fiber.equiv_postcompose f g (Point B),
     esimp, apply (ap (fiber.mk (Point A))), refine !con.assoc ⬝ _, apply inv_con_eq_of_eq_con,
-    rewrite [con.assoc, con.right_inv, con_idp, -ap_compose'], apply ap_con_eq_con
+    rewrite [▸*, con.assoc, con.right_inv, con_idp, -ap_compose'],
+    exact ap_con_eq_con (λ x, ap g⁻¹ᵉ* (ap g (pleft_inv' g x)⁻¹) ⬝ ap g⁻¹ᵉ* (pright_inv g (g x)) ⬝
+      pleft_inv' g x) (respect_pt f)
   end
 
   definition pequiv_precompose {A A' B : Type*} (f : A →* B) (g : A' ≃* A)
@@ -249,17 +251,18 @@ namespace fiber
     esimp at *, induction h₀, induction g₀,
     fapply phomotopy.mk,
     { reflexivity },
-    { esimp [pfiber_pequiv_of_phomotopy], exact !point_fiber_eq⁻¹ }
+    { symmetry, rexact point_fiber_eq (idpath pt)
+        (inv_con_eq_of_eq_con (idpath (h pt ⬝ (idp ⬝ point_eq (fiber.mk pt idp))))) }
   end
 
   lemma pequiv_postcompose_ppoint {A B B' : Type*} (f : A →* B) (g : B ≃* B')
     : ppoint f ∘* fiber.pequiv_postcompose f g ~* ppoint (g ∘* f) :=
   begin
     induction f with f f₀, induction g with g hg g₀, induction B with B b₀,
-    induction B' with B' b₀', esimp at *, induction g₀, induction f₀,
+    induction B' with B' b₀', esimp at * ⊢, induction g₀, induction f₀,
     fapply phomotopy.mk,
     { reflexivity },
-    { esimp [pequiv_postcompose], symmetry,
+    { symmetry,
       refine !ap_compose⁻¹ ⬝ _, apply ap_constant }
   end
 
@@ -302,6 +305,38 @@ namespace fiber
     pfiber f ≃* A :=
   pequiv_of_equiv (fiber_equiv_of_is_contr f pt) idp
 
+  definition pfiber_ppoint_equiv {A B : Type*} (f : A →* B) : pfiber (ppoint f) ≃ Ω B :=
+  calc
+    pfiber (ppoint f) ≃ Σ(x : pfiber f), ppoint f x = pt : fiber.sigma_char
+      ... ≃ Σ(x : Σa, f a = pt), x.1 = pt : by exact sigma_equiv_sigma !fiber.sigma_char (λa, erfl)
+      ... ≃ Σ(x : Σa, a = pt), f x.1 = pt : by exact !sigma_assoc_comm_equiv
+      ... ≃ f pt = pt : by exact !sigma_equiv_of_is_contr_left
+      ... ≃ Ω B : by exact !equiv_eq_closed_left !respect_pt
+
+  definition pfiber_ppoint_pequiv {A B : Type*} (f : A →* B) : pfiber (ppoint f) ≃* Ω B :=
+  pequiv_of_equiv (pfiber_ppoint_equiv f) !con.left_inv
+
+  definition fiber_ppoint_equiv_eq {A B : Type*} {f : A →* B} {a : A} (p : f a = pt)
+    (q : ppoint f (fiber.mk a p) = pt) :
+    pfiber_ppoint_equiv f (fiber.mk (fiber.mk a p) q) = (respect_pt f)⁻¹ ⬝ ap f q⁻¹ ⬝ p :=
+  begin
+    refine _ ⬝ !con.assoc⁻¹,
+    apply whisker_left,
+    refine eq_transport_Fl _ _ ⬝ _,
+    apply whisker_right,
+    refine inverse2 !ap_inv ⬝ !inv_inv ⬝ _,
+    refine ap_compose f pr₁ _ ⬝ ap02 f !ap_pr1_center_eq_sigma_eq',
+  end
+
+  definition fiber_ppoint_equiv_inv_eq {A B : Type*} (f : A →* B) (p : Ω B) :
+    (pfiber_ppoint_equiv f)⁻¹ᵉ p = fiber.mk (fiber.mk pt (respect_pt f ⬝ p)) idp :=
+  begin
+    apply inv_eq_of_eq,
+    refine _ ⬝ !fiber_ppoint_equiv_eq⁻¹,
+    exact !inv_con_cancel_left⁻¹
+  end
+
+
 end fiber
 
 open function is_equiv
diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean
index 30b480ccd..bfe2ce8b4 100644
--- a/hott/types/pointed.hlean
+++ b/hott/types/pointed.hlean
@@ -112,14 +112,14 @@ namespace pointed
 end pointed open pointed
 
 namespace pointed
-  variables {A B C D : Type*} {f g h : A →* B}
+  variables {A B C D : Type*} {f g h : A →* B} {P : A → Type} {p₀ : P pt} {k k' l m : ppi P p₀}
 
   /- categorical properties of pointed maps -/
 
-  definition pid [constructor] [refl] (A : Type*) : A →* A :=
+  definition pid [constructor] (A : Type*) : A →* A :=
   pmap.mk id idp
 
-  definition pcompose [constructor] [trans] {A B C : Type*} (g : B →* C) (f : A →* B) : A →* C :=
+  definition pcompose [constructor] {A B C : Type*} (g : B →* C) (f : A →* B) : A →* C :=
   pmap.mk (λa, g (f a)) (ap g (respect_pt f) ⬝ respect_pt g)
 
   infixr ` ∘* `:60 := pcompose
@@ -152,17 +152,21 @@ namespace pointed
 
   /- equivalences and equalities -/
 
-  definition pmap.sigma_char [constructor] {A B : Type*} : (A →* B) ≃ Σ(f : A → B), f pt = pt :=
+  protected definition ppi.sigma_char [constructor] {A : Type*} (B : A → Type) (b₀ : B pt) :
+    ppi B b₀ ≃ Σ(k : Πa, B a), k pt = b₀ :=
   begin
-    fapply equiv.MK : intros f,
-    { exact ⟨f , respect_pt f⟩ },
-    all_goals cases f with f p,
-    { exact pmap.mk f p },
-    all_goals reflexivity
+    fapply equiv.MK: intro x,
+    { constructor, exact respect_pt x },
+    { induction x, constructor, assumption },
+    { induction x, reflexivity },
+    { induction x, reflexivity }
   end
 
+  definition pmap.sigma_char [constructor] {A B : Type*} : (A →* B) ≃ Σ(f : A → B), f pt = pt :=
+  !ppi.sigma_char
+
   definition pmap.eta_expand [constructor] {A B : Type*} (f : A →* B) : A →* B :=
-  pmap.mk f (pmap.resp_pt f)
+  pmap.mk f (respect_pt f)
 
   definition pmap_equiv_right (A : Type*) (B : Type)
     : (Σ(b : B), A →* (pointed.Mk b)) ≃ (A → B) :=
@@ -181,11 +185,11 @@ namespace pointed
 
   -- The constant pointed map between any two types
   definition pconst [constructor] (A B : Type*) : A →* B :=
-  pmap.mk (λ a, Point B) idp
+  !ppi_const
 
-  -- the pointed type of pointed maps
+  -- the pointed type of pointed maps -- TODO: remove
   definition ppmap [constructor] (A B : Type*) : Type* :=
-  pType.mk (A →* B) (pconst A B)
+  @pppi A (λa, B)
 
   definition pcast [constructor] {A B : Type*} (p : A = B) : A →* B :=
   pmap.mk (cast (ap pType.carrier p)) (by induction p; reflexivity)
@@ -303,85 +307,77 @@ namespace pointed
     : pinverse p⁻¹ = (pinverse p)⁻¹ :=
   idp
 
+  definition ap1_pcompose_pinverse [constructor] {X Y : Type*} (f : X →* Y) :
+    Ω→ f ∘* pinverse ~* pinverse ∘* Ω→ f :=
+  phomotopy.mk (ap1_gen_inv f (respect_pt f) (respect_pt f))
+    abstract begin
+      induction Y with Y y₀, induction f with f f₀, esimp at * ⊢, induction f₀, reflexivity
+    end end
+
   definition is_equiv_pcast [instance] {A B : Type*} (p : A = B) : is_equiv (pcast p) :=
   !is_equiv_cast
 
   /- categorical properties of pointed homotopies -/
 
-  protected definition phomotopy.refl [constructor] [refl] (f : A →* B) : f ~* f :=
-  begin
-    fapply phomotopy.mk,
-    { intro a, exact idp},
-    { apply idp_con}
-  end
+  variable (k)
+  protected definition phomotopy.refl [constructor] : k ~* k :=
+  phomotopy.mk homotopy.rfl !idp_con
+  variable {k}
+  protected definition phomotopy.rfl [constructor] [refl] : k ~* k :=
+  phomotopy.refl k
 
-  protected definition phomotopy.rfl [constructor] [reducible] {f : A →* B} : f ~* f :=
-  phomotopy.refl f
+  protected definition phomotopy.symm [constructor] [symm] (p : k ~* l) : l ~* k :=
+  phomotopy.mk p⁻¹ʰᵗʸ (inv_con_eq_of_eq_con (to_homotopy_pt p)⁻¹)
 
-  protected definition phomotopy.trans [constructor] [trans] (p : f ~* g) (q : g ~* h)
-    : f ~* h :=
+  protected definition phomotopy.trans [constructor] [trans] (p : k ~* l) (q : l ~* m) :
+    k ~* m :=
   phomotopy.mk (λa, p a ⬝ q a) (!con.assoc ⬝ whisker_left (p pt) (to_homotopy_pt q) ⬝ to_homotopy_pt p)
 
-  protected definition phomotopy.symm [constructor] [symm] (p : f ~* g) : g ~* f :=
-  phomotopy.mk (λa, (p a)⁻¹) (inv_con_eq_of_eq_con (to_homotopy_pt p)⁻¹)
-
   infix ` ⬝* `:75 := phomotopy.trans
   postfix `⁻¹*`:(max+1) := phomotopy.symm
 
   /- equalities and equivalences relating pointed homotopies -/
 
-  definition phomotopy.rec' [recursor] (P : f ~* g → Type)
-    (H : Π(h : f ~ g) (p : h pt ⬝ respect_pt g = respect_pt f), P (phomotopy.mk h p))
-    (h : f ~* g) : P h :=
+  definition phomotopy.rec' [recursor] (B : k ~* l → Type)
+    (H : Π(h : k ~ l) (p : h pt ⬝ respect_pt l = respect_pt k), B (phomotopy.mk h p))
+    (h : k ~* l) : B h :=
   begin
     induction h with h p,
-    refine transport (λp, P (ppi.mk h p)) _ (H h (con_eq_of_eq_con_inv p)),
+    refine transport (λp, B (ppi.mk h p)) _ (H h (con_eq_of_eq_con_inv p)),
     apply to_left_inv !eq_con_inv_equiv_con_eq p
   end
 
-  definition phomotopy.sigma_char [constructor] {A B : Type*} (f g : A →* B)
-    : (f ~* g) ≃ Σ(p : f ~ g), p pt ⬝ respect_pt g = respect_pt f :=
-  begin
-    fapply equiv.MK : intros h,
-    { exact ⟨h , to_homotopy_pt h⟩ },
-    { cases h with h p, exact phomotopy.mk h p },
-    { cases h with h p, exact ap (dpair h) (to_right_inv !eq_con_inv_equiv_con_eq p) },
-    { induction h using phomotopy.rec' with h p, esimp,
-      exact ap (phomotopy.mk h) (to_right_inv !eq_con_inv_equiv_con_eq p) },
-  end
-
-  definition phomotopy.eta_expand [constructor] {A B : Type*} {f g : A →* B} (p : f ~* g) :
-    f ~* g :=
+  definition phomotopy.eta_expand [constructor] (p : k ~* l) : k ~* l :=
   phomotopy.mk p (to_homotopy_pt p)
 
+  definition is_trunc_ppi [instance] (n : ℕ₋₂) {A : Type*} (B : A → Type) (b₀ : B pt) [Πa, is_trunc n (B a)] :
+    is_trunc n (ppi B b₀) :=
+  is_trunc_equiv_closed_rev _ !ppi.sigma_char
+
   definition is_trunc_pmap [instance] (n : ℕ₋₂) (A B : Type*) [is_trunc n B] :
     is_trunc n (A →* B) :=
-  is_trunc_equiv_closed_rev _ !pmap.sigma_char
+  !is_trunc_ppi
 
   definition is_trunc_ppmap [instance] (n : ℕ₋₂) {A B : Type*} [is_trunc n B] :
     is_trunc n (ppmap A B) :=
   !is_trunc_pmap
 
-  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
+  definition phomotopy_of_eq [constructor] (p : k = l) : k ~* l :=
+  phomotopy.mk (ap010 ppi.to_fun p) begin induction p, refine !idp_con end
 
-  definition phomotopy_of_eq_idp {A B : Type*} (f : A →* B) :
-    phomotopy_of_eq idp = phomotopy.refl f :=
+  definition phomotopy_of_eq_idp (k : ppi P p₀) : phomotopy_of_eq idp = phomotopy.refl k :=
   idp
 
-  definition pconcat_eq [constructor] {A B : Type*} {f g h : A →* B} (p : f ~* g) (q : g = h)
-    : f ~* h :=
+  definition pconcat_eq [constructor] (p : k ~* l) (q : l = m) : k ~* m :=
   p ⬝* phomotopy_of_eq q
 
-  definition eq_pconcat [constructor] {A B : Type*} {f g h : A →* B} (p : f = g) (q : g ~* h)
-    : f ~* h :=
+  definition eq_pconcat [constructor] (p : k = l) (q : l ~* m) : k ~* m :=
   phomotopy_of_eq p ⬝* q
 
   infix ` ⬝*p `:75 := pconcat_eq
   infix ` ⬝p* `:75 := eq_pconcat
 
-  definition pr1_phomotopy_eq {A B : Type*} {f g : A →* B} {p q : f ~* g} (r : p = q) (a : A) :
-    p a = q a :=
+  definition pr1_phomotopy_eq {p q : k ~* l} (r : p = q) (a : A) : p a = q a :=
   ap010 to_homotopy r a
 
   definition pwhisker_left [constructor] (h : B →* C) (p : f ~* g) : h ∘* f ~* h ∘* g :=
@@ -397,43 +393,59 @@ namespace pointed
     (q : h ~* i) (p : f ~* g) : h ∘* f ~* i ∘* g :=
   pwhisker_left _ p ⬝* pwhisker_right _ q
 
-  definition pmap_eq_equiv_internal {A B : Type*} (f g : A →* B) : (f = g) ≃ (f ~* g) :=
-  calc (f = g) ≃ pmap.sigma_char f = pmap.sigma_char g
-                 : eq_equiv_fn_eq pmap.sigma_char f g
-          ...  ≃ Σ(p : pmap.to_fun f = pmap.to_fun g),
-                   pathover (λh, h pt = pt) (respect_pt f) p (respect_pt g)
-                 : sigma_eq_equiv _ _
-          ...  ≃ Σ(p : pmap.to_fun f = pmap.to_fun g), respect_pt f = ap (λh, h pt) p ⬝ respect_pt g
-                 : sigma_equiv_sigma_right (λp, eq_pathover_equiv_Fl p (respect_pt f)
-                                                                       (respect_pt g))
-          ...  ≃ Σ(p : pmap.to_fun f = pmap.to_fun g), respect_pt f = ap10 p pt ⬝ respect_pt g
-                 : sigma_equiv_sigma_right
-                     (λp, equiv_eq_closed_right _ (whisker_right _ (ap_eq_apd10 p _)))
-          ...  ≃ Σ(p : pmap.to_fun f ~ pmap.to_fun g), respect_pt f = p pt ⬝ respect_pt g
-                 : sigma_equiv_sigma_left' eq_equiv_homotopy
-          ...  ≃ Σ(p : pmap.to_fun f ~ pmap.to_fun g), p pt ⬝ respect_pt g = respect_pt f
-                 : sigma_equiv_sigma_right (λp, eq_equiv_eq_symm _ _)
-          ...  ≃ (f ~* g) : phomotopy.sigma_char f g
+  variables (k l)
 
-  definition pmap_eq_equiv_internal_idp {A B : Type*} (f : A →* B) :
-    pmap_eq_equiv_internal f f idp = phomotopy.refl f  :=
+  definition phomotopy.sigma_char [constructor]
+    : (k ~* l) ≃ Σ(p : k ~ l), p pt ⬝ respect_pt l = respect_pt k :=
   begin
-    apply ap (phomotopy.mk (homotopy.refl _)), induction B with B b₀, induction f with f f₀,
-    esimp at *, induction f₀, reflexivity
+    fapply equiv.MK : intros h,
+    { exact ⟨h , to_homotopy_pt h⟩ },
+    { cases h with h p, exact phomotopy.mk h p },
+    { cases h with h p, exact ap (dpair h) (to_right_inv !eq_con_inv_equiv_con_eq p) },
+    { induction h using phomotopy.rec' with h p,
+      exact ap (phomotopy.mk h) (to_right_inv !eq_con_inv_equiv_con_eq p) }
   end
 
-  definition eq_of_phomotopy' (p : f ~* g) : f = g :=
-  to_inv (pmap_eq_equiv_internal f g) p
+  definition ppi_eq_equiv_internal : (k = l) ≃ (k ~* l) :=
+    calc (k = l) ≃ ppi.sigma_char P p₀ k = ppi.sigma_char P p₀ l
+                   : eq_equiv_fn_eq (ppi.sigma_char P p₀) k l
+            ...  ≃ Σ(p : k = l),
+                     pathover (λh, h pt = p₀) (respect_pt k) p (respect_pt l)
+                   : sigma_eq_equiv _ _
+            ...  ≃ Σ(p : k = l),
+                     respect_pt k = ap (λh, h pt) p ⬝ respect_pt l
+                   : sigma_equiv_sigma_right
+                       (λp, eq_pathover_equiv_Fl p (respect_pt k) (respect_pt l))
+            ...  ≃ Σ(p : k = l),
+                     respect_pt k = apd10 p pt ⬝ respect_pt l
+                   : sigma_equiv_sigma_right
+                       (λp, equiv_eq_closed_right _ (whisker_right _ (ap_eq_apd10 p _)))
+            ...  ≃ Σ(p : k ~ l), respect_pt k = p pt ⬝ respect_pt l
+                   : sigma_equiv_sigma_left' eq_equiv_homotopy
+            ...  ≃ Σ(p : k ~ l), p pt ⬝ respect_pt l = respect_pt k
+                   : sigma_equiv_sigma_right (λp, eq_equiv_eq_symm _ _)
+            ...  ≃ (k ~* l) : phomotopy.sigma_char k l
 
-  definition pmap_eq_equiv [constructor] {A B : Type*} (f g : A →* B) : (f = g) ≃ (f ~* g) :=
+  definition ppi_eq_equiv_internal_idp :
+    ppi_eq_equiv_internal k k idp = phomotopy.refl k :=
   begin
-    refine equiv_change_fun (pmap_eq_equiv_internal f g) _,
+    apply ap (phomotopy.mk (homotopy.refl _)), induction k with k k₀,
+    esimp at * ⊢, induction k₀, reflexivity
+  end
+
+  definition ppi_eq_equiv [constructor] : (k = l) ≃ (k ~* l) :=
+  begin
+    refine equiv_change_fun (ppi_eq_equiv_internal k l) _,
     { apply phomotopy_of_eq },
-    { intro p, induction p, exact pmap_eq_equiv_internal_idp f }
+    { intro p, induction p, exact ppi_eq_equiv_internal_idp k }
   end
+  variables {k l}
 
-  definition eq_of_phomotopy (p : f ~* g) : f = g :=
-  to_inv (pmap_eq_equiv f g) p
+  definition pmap_eq_equiv [constructor] (f g : A →* B) : (f = g) ≃ (f ~* g) :=
+  ppi_eq_equiv f g
+
+  definition eq_of_phomotopy (p : k ~* l) : k = l :=
+  to_inv (ppi_eq_equiv k l) p
 
   definition eq_of_phomotopy_refl {X Y : Type*} (f : X →* Y) :
     eq_of_phomotopy (phomotopy.refl f) = idpath f :=
@@ -441,77 +453,76 @@ namespace pointed
     apply to_inv_eq_of_eq, reflexivity
   end
 
-  definition phomotopy_of_homotopy {X Y : Type*} {f g : X →* Y} (h : f ~ g) [is_set Y] : f ~* g :=
+  definition phomotopy_of_homotopy (h : k ~ l) [Πa, is_set (P a)] : k ~* l :=
   begin
     fapply phomotopy.mk,
     { exact h },
     { apply is_set.elim }
   end
 
-  -- TODO: flip arguments in s
-  definition pmap_eq (r : Πa, f a = g a) (s : respect_pt f = (r pt) ⬝ respect_pt g) : f = g :=
-  eq_of_phomotopy (phomotopy.mk r s⁻¹)
+  definition ppi_eq_of_homotopy [Πa, is_set (P a)] (p : k ~ l) : k = l :=
+  eq_of_phomotopy (phomotopy_of_homotopy p)
 
-  definition pmap_eq_of_homotopy {A B : Type*} {f g : A →* B} [is_set B] (p : f ~ g) : f = g :=
-  pmap_eq p !is_set.elim
+  definition pmap_eq_of_homotopy [is_set B] (p : f ~ g) : f = g :=
+  ppi_eq_of_homotopy p
 
-  definition phomotopy_of_eq_of_phomotopy {A B : Type*} {f g : A →* B} (p : f ~* g) :
-    phomotopy_of_eq (eq_of_phomotopy p) = p :=
-  to_right_inv (pmap_eq_equiv f g) p
+  definition phomotopy_of_eq_of_phomotopy (p : k ~* l) : phomotopy_of_eq (eq_of_phomotopy p) = p :=
+  to_right_inv (ppi_eq_equiv k l) p
 
-  definition phomotopy_rec_on_eq [recursor] {A B : Type*} {f g : A →* B}
-    {Q : (f ~* g) → Type} (p : f ~* g) (H : Π(q : f = g), Q (phomotopy_of_eq q)) : Q p :=
+  definition phomotopy_rec_eq [recursor] {Q : (k ~* k') → Type} (p : k ~* k')
+    (H : Π(q : k = k'), Q (phomotopy_of_eq q)) : Q p :=
   phomotopy_of_eq_of_phomotopy p ▸ H (eq_of_phomotopy p)
 
-  definition phomotopy_rec_on_idp [recursor] {A B : Type*} {f : A →* B}
-    {Q : Π{g}, (f ~* g) → Type} {g : A →* B} (p : f ~* g) (H : Q (phomotopy.refl f)) : Q p :=
+  definition phomotopy_rec_idp [recursor] {Q : Π {k' : ppi P p₀}, (k ~* k') → Type}
+    {k' : ppi P p₀} (H : k ~* k') (q : Q (phomotopy.refl k)) : Q H :=
   begin
-    induction p using phomotopy_rec_on_eq,
-    induction q, exact H
+    induction H using phomotopy_rec_eq with t,
+    induction t, exact phomotopy_of_eq_idp k ▸ q,
   end
+
   attribute phomotopy.rec' [recursor]
 
-  definition phomotopy_rec_on_eq_phomotopy_of_eq {A B : Type*} {f g: A →* B}
+  definition phomotopy_rec_eq_phomotopy_of_eq {A B : Type*} {f g: A →* B}
     {Q : (f ~* g) → Type} (p : f = g) (H : Π(q : f = g), Q (phomotopy_of_eq q)) :
-    phomotopy_rec_on_eq (phomotopy_of_eq p) H = H p :=
+    phomotopy_rec_eq (phomotopy_of_eq p) H = H p :=
   begin
-    unfold phomotopy_rec_on_eq,
+    unfold phomotopy_rec_eq,
     refine ap (λp, p ▸ _) !adj ⬝ _,
     refine !tr_compose⁻¹ ⬝ _,
     apply apdt
   end
 
-  definition phomotopy_rec_on_idp_refl {A B : Type*} (f : A →* B)
+  definition phomotopy_rec_idp_refl {A B : Type*} (f : A →* B)
     {Q : Π{g}, (f ~* g) → Type} (H : Q (phomotopy.refl f)) :
-    phomotopy_rec_on_idp phomotopy.rfl H = H :=
-  !phomotopy_rec_on_eq_phomotopy_of_eq
+    phomotopy_rec_idp phomotopy.rfl H = H :=
+  !phomotopy_rec_eq_phomotopy_of_eq
 
   /- adjunction between (-)₊ : Type → Type* and pType.carrier : Type* → Type  -/
   definition pmap_equiv_left (A : Type) (B : Type*) : A₊ →* B ≃ (A → B) :=
   begin
     fapply equiv.MK,
-    { intro f a, cases f with f p, exact f (some a)},
+    { intro f a, cases f with f p, exact f (some a) },
     { intro f, fconstructor,
         intro a, cases a, exact pt, exact f a,
-        reflexivity},
-    { intro f, reflexivity},
-    { intro f, cases f with f p, esimp, fapply pmap_eq,
-      { intro a, cases a; all_goals (esimp at *), exact p⁻¹},
-      { esimp, exact !con.left_inv⁻¹}},
+        reflexivity },
+    { intro f, reflexivity },
+    { intro f, cases f with f p, esimp, fapply eq_of_phomotopy, fapply phomotopy.mk,
+      { intro a, cases a; all_goals (esimp at *), exact p⁻¹ },
+      { esimp, exact !con.left_inv }},
   end
 
   -- pmap_pbool_pequiv is the pointed equivalence
   definition pmap_pbool_equiv [constructor] (B : Type*) : (pbool →* B) ≃ B :=
   begin
     fapply equiv.MK,
-    { intro f, cases f with f p, exact f tt},
+    { intro f, cases f with f p, exact f tt },
     { intro b, fconstructor,
         intro u, cases u, exact pt, exact b,
-        reflexivity},
-    { intro b, reflexivity},
-    { intro f, cases f with f p, esimp, fapply pmap_eq,
-      { intro a, cases a; all_goals (esimp at *), exact p⁻¹},
-      { esimp, exact !con.left_inv⁻¹}},
+        reflexivity },
+    { intro b, reflexivity },
+    { intro f, cases f with f p, esimp, fapply eq_of_phomotopy, fapply phomotopy.mk,
+      { intro a, cases a; all_goals (esimp at *), exact p⁻¹ },
+      { esimp, exact !con.left_inv }},
   end
 
   /-
@@ -524,12 +535,12 @@ namespace pointed
   -/
   definition pap (F : (A →* B) → (C →* D)) {f g : A →* B} (p : f ~* g) : F f ~* F g :=
   begin
-    induction p using phomotopy_rec_on_idp, reflexivity
+    induction p using phomotopy_rec_idp, reflexivity
   end
 
   definition pap_refl (F : (A →* B) → (C →* D)) (f : A →* B) :
     pap F (phomotopy.refl f) = phomotopy.refl (F f) :=
-  !phomotopy_rec_on_idp_refl
+  !phomotopy_rec_idp_refl
 
   definition ap1_phomotopy {f g : A →* B} (p : f ~* g) : Ω→ f ~* Ω→ g :=
   pap Ω→ p
@@ -542,7 +553,7 @@ namespace pointed
   definition ap1_phomotopy_explicit {f g : A →* B} (p : f ~* g) : Ω→ f ~* Ω→ g :=
   begin
     induction p with p q, induction f with f pf, induction g with g pg, induction B with B b,
-    esimp at *, induction q, induction pg,
+    esimp at * ⊢, induction q, induction pg,
     fapply phomotopy.mk,
     { intro l, refine _ ⬝ !idp_con⁻¹ᵖ, refine !con.assoc ⬝ _, apply inv_con_eq_of_eq_con,
       apply ap_con_eq_con_ap},
@@ -565,14 +576,14 @@ namespace pointed
   definition to_fun_eq_of_phomotopy {A B : Type*} {f g : A →* B} (p : f ~* g) (a : A) :
     ap010 pmap.to_fun (eq_of_phomotopy p) a = p a :=
   begin
-    induction p using phomotopy_rec_on_idp,
+    induction p using phomotopy_rec_idp,
     exact ap (λx, ap010 pmap.to_fun x a) !eq_of_phomotopy_refl
   end
 
   definition ap1_eq_of_phomotopy {A B : Type*} {f g : A →* B} (p : f ~* g) :
     ap Ω→ (eq_of_phomotopy p) = eq_of_phomotopy (ap1_phomotopy p) :=
   begin
-    induction p using phomotopy_rec_on_idp,
+    induction p using phomotopy_rec_idp,
     refine ap02 _ !eq_of_phomotopy_refl ⬝ !eq_of_phomotopy_refl⁻¹ ⬝ ap eq_of_phomotopy _,
     exact !ap1_phomotopy_refl⁻¹
   end
@@ -609,15 +620,6 @@ namespace pointed
   phomotopy.mk (ap1_gen_compose g f (respect_pt f) (respect_pt f) (respect_pt g) (respect_pt g))
                (ap1_gen_compose_idp g f (respect_pt f) (respect_pt g))
 
-  definition ap1_pcompose_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
-
   definition ap1_pconst [constructor] (A B : Type*) : Ω→(pconst A B) ~* pconst (Ω A) (Ω B) :=
   phomotopy.mk (λp, ap1_gen_idp_left (const A pt) p ⬝ ap_constant p pt) rfl
 
@@ -708,9 +710,12 @@ namespace pointed
          (pright_inv : to_pmap ∘* to_pinv1 ~* pid B)
          (pleft_inv : to_pinv2 ∘* to_pmap ~* pid A)
 
-  attribute pequiv.to_pmap [coercion]
   infix ` ≃* `:25 := pequiv
 
+  definition pmap_of_pequiv [unfold 3] [coercion] [reducible] {A B : Type*} (f : A ≃* B) :
+    @ppi A (λa, B) pt :=
+  pequiv.to_pmap f
+
   definition to_pinv [unfold 3] (f : A ≃* B) : B →* A :=
   pequiv.to_pinv1 f
 
@@ -728,14 +733,14 @@ namespace pointed
   have is_equiv f, from adjointify f (to_pinv f) (pequiv.pright_inv f) (pleft_inv' f),
   equiv.mk f _
 
-  attribute pointed._trans_of_equiv_of_pequiv pequiv._trans_of_to_pmap [unfold 3]
+  attribute pointed._trans_of_equiv_of_pequiv pointed._trans_of_pmap_of_pequiv [unfold 3]
 
   definition pequiv.to_is_equiv [instance] [constructor] (f : A ≃* B) :
     is_equiv (pointed._trans_of_equiv_of_pequiv f) :=
   adjointify f (to_pinv f) (pequiv.pright_inv f) (pleft_inv' f)
 
   definition pequiv.to_is_equiv' [instance] [constructor] (f : A ≃* B) :
-    is_equiv (pequiv._trans_of_to_pmap f) :=
+    is_equiv (pointed._trans_of_pmap_of_pequiv f) :=
   pequiv.to_is_equiv f
 
   protected definition pequiv.MK [constructor] (f : A →* B) (g : B →* A)
@@ -1067,9 +1072,9 @@ namespace pointed
     ppmap A B →* ppmap A' B' :=
   pmap.mk (λh, g ∘* h ∘* f)
     abstract begin
-      fapply pmap_eq,
+      fapply eq_of_phomotopy, fapply phomotopy.mk,
       { esimp, intro a, exact respect_pt g},
-      { rewrite [▸*, ap_constant], apply idp_con}
+      { rewrite [▸*, ap_constant], exact !idp_con⁻¹ }
     end end
 
   definition pequiv_pinverse (A : Type*) : Ω A ≃* Ω A :=
diff --git a/hott/types/pointed2.hlean b/hott/types/pointed2.hlean
index faaf5c4aa..ff62d2644 100644
--- a/hott/types/pointed2.hlean
+++ b/hott/types/pointed2.hlean
@@ -184,13 +184,13 @@ namespace pointed
   definition eq_of_phomotopy_trans {X Y : Type*} {f g h : X →* Y} (p : f ~* g) (q : g ~* h) :
     eq_of_phomotopy (p ⬝* q) = eq_of_phomotopy p ⬝ eq_of_phomotopy q :=
   begin
-    induction p using phomotopy_rec_on_idp, induction q using phomotopy_rec_on_idp,
+    induction p using phomotopy_rec_idp, induction q using phomotopy_rec_idp,
     exact ap eq_of_phomotopy !trans_refl ⬝ whisker_left _ !eq_of_phomotopy_refl⁻¹
   end
 
   definition refl_trans {A B : Type*} {f g : A →* B} (p : f ~* g) : phomotopy.refl f ⬝* p = p :=
   begin
-    induction p using phomotopy_rec_on_idp,
+    induction p using phomotopy_rec_idp,
     induction A with A a₀, induction B with B b₀,
     induction f with f f₀, esimp at *, induction f₀,
     reflexivity
@@ -199,9 +199,9 @@ namespace pointed
   definition trans_assoc {A B : Type*} {f g h i : A →* B} (p : f ~* g) (q : g ~* h)
     (r : h ~* i) : p ⬝* q ⬝* r = p ⬝* (q ⬝* r) :=
   begin
-    induction r using phomotopy_rec_on_idp,
-    induction q using phomotopy_rec_on_idp,
-    induction p using phomotopy_rec_on_idp,
+    induction r using phomotopy_rec_idp,
+    induction q using phomotopy_rec_idp,
+    induction p using phomotopy_rec_idp,
     induction B with B b₀,
     induction f with f f₀, esimp at *, induction f₀,
     reflexivity
@@ -217,18 +217,18 @@ namespace pointed
   definition symm_symm {A B : Type*} {f g : A →* B} (p : f ~* g) : p⁻¹*⁻¹* = p :=
   phomotopy_eq (λa, !inv_inv)
     begin
-      induction p using phomotopy_rec_on_idp, induction f with f f₀, induction B with B b₀,
+      induction p using phomotopy_rec_idp, induction f with f f₀, induction B with B b₀,
       esimp at *, induction f₀, reflexivity
     end
 
   definition trans_right_inv {A B : Type*} {f g : A →* B} (p : f ~* g) : p ⬝* p⁻¹* = phomotopy.rfl :=
   begin
-    induction p using phomotopy_rec_on_idp, exact !refl_trans ⬝ !refl_symm
+    induction p using phomotopy_rec_idp, exact !refl_trans ⬝ !refl_symm
   end
 
   definition trans_left_inv {A B : Type*} {f g : A →* B} (p : f ~* g) : p⁻¹* ⬝* p = phomotopy.rfl :=
   begin
-    induction p using phomotopy_rec_on_idp, exact !trans_refl ⬝ !refl_symm
+    induction p using phomotopy_rec_idp, exact !trans_refl ⬝ !refl_symm
   end
 
   definition trans2 {A B : Type*} {f g h : A →* B} {p p' : f ~* g} {q q' : g ~* h}
@@ -249,7 +249,7 @@ namespace pointed
   definition trans_symm {A B : Type*} {f g h : A →* B} (p : f ~* g) (q : g ~* h) :
     (p ⬝* q)⁻¹* = q⁻¹* ⬝* p⁻¹* :=
   begin
-    induction p using phomotopy_rec_on_idp, induction q using phomotopy_rec_on_idp,
+    induction p using phomotopy_rec_idp, induction q using phomotopy_rec_idp,
     exact !trans_refl⁻²** ⬝ !trans_refl⁻¹ ⬝ idp ◾** !refl_symm⁻¹
   end
 
@@ -293,8 +293,8 @@ namespace pointed
     (p : f₁ ~* f₂) (q : f₂ ~* f₃) :
     pwhisker_left g (p ⬝* q) = pwhisker_left g p ⬝* pwhisker_left g q :=
   begin
-    induction p using phomotopy_rec_on_idp,
-    induction q using phomotopy_rec_on_idp,
+    induction p using phomotopy_rec_idp,
+    induction q using phomotopy_rec_idp,
     refine _ ⬝ !pwhisker_left_refl⁻¹ ◾** !pwhisker_left_refl⁻¹,
     refine ap (pwhisker_left g) !trans_refl ⬝ !pwhisker_left_refl ⬝ !trans_refl⁻¹
   end
@@ -303,8 +303,8 @@ namespace pointed
     (p : g₁ ~* g₂) (q : g₂ ~* g₃) :
     pwhisker_right f (p ⬝* q) = pwhisker_right f p ⬝* pwhisker_right f q :=
   begin
-    induction p using phomotopy_rec_on_idp,
-    induction q using phomotopy_rec_on_idp,
+    induction p using phomotopy_rec_idp,
+    induction q using phomotopy_rec_idp,
     refine _ ⬝ !pwhisker_right_refl⁻¹ ◾** !pwhisker_right_refl⁻¹,
     refine ap (pwhisker_right f) !trans_refl ⬝ !pwhisker_right_refl ⬝ !trans_refl⁻¹
   end
@@ -312,7 +312,7 @@ namespace pointed
   definition pwhisker_left_symm {A B C : Type*} (g : B →* C) {f₁ f₂ : A →* B} (p : f₁ ~* f₂) :
     pwhisker_left g p⁻¹* = (pwhisker_left g p)⁻¹* :=
   begin
-    induction p using phomotopy_rec_on_idp,
+    induction p using phomotopy_rec_idp,
     refine _ ⬝ ap phomotopy.symm !pwhisker_left_refl⁻¹,
     refine ap (pwhisker_left g) !refl_symm ⬝ !pwhisker_left_refl ⬝ !refl_symm⁻¹
   end
@@ -320,7 +320,7 @@ namespace pointed
   definition pwhisker_right_symm {A B C : Type*} (f : A →* B) {g₁ g₂ : B →* C} (p : g₁ ~* g₂) :
     pwhisker_right f p⁻¹* = (pwhisker_right f p)⁻¹* :=
   begin
-    induction p using phomotopy_rec_on_idp,
+    induction p using phomotopy_rec_idp,
     refine _ ⬝ ap phomotopy.symm !pwhisker_right_refl⁻¹,
     refine ap (pwhisker_right f) !refl_symm ⬝ !pwhisker_right_refl ⬝ !refl_symm⁻¹
   end
@@ -469,7 +469,7 @@ namespace pointed
     (p : f ~* f') : phsquare (passoc h g f) (passoc h g f')
       (pwhisker_left (h ∘* g) p) (pwhisker_left h (pwhisker_left g p)) :=
   begin
-    induction p using phomotopy_rec_on_idp,
+    induction p using phomotopy_rec_idp,
     refine idp ◾** (ap (pwhisker_left h) !pwhisker_left_refl ⬝ !pwhisker_left_refl) ⬝ _ ⬝
           !pwhisker_left_refl⁻¹ ◾** idp,
     exact !trans_refl ⬝ !refl_trans⁻¹
@@ -479,7 +479,7 @@ namespace pointed
     (p : g ~* g') : phsquare (passoc h g f) (passoc h g' f)
       (pwhisker_right f (pwhisker_left h p)) (pwhisker_left h (pwhisker_right f p)) :=
   begin
-    induction p using phomotopy_rec_on_idp,
+    induction p using phomotopy_rec_idp,
     rewrite [pwhisker_right_refl, pwhisker_left_refl],
     rewrite [pwhisker_right_refl, pwhisker_left_refl],
     exact phvrfl
@@ -489,8 +489,8 @@ namespace pointed
     (p : g ~* g') (q : f ~* f') :
     phsquare (pwhisker_right f p) (pwhisker_right f' p) (pwhisker_left g q) (pwhisker_left g' q) :=
   begin
-    induction p using phomotopy_rec_on_idp,
-    induction q using phomotopy_rec_on_idp,
+    induction p using phomotopy_rec_idp,
+    induction q using phomotopy_rec_idp,
     exact !pwhisker_right_refl ◾** !pwhisker_left_refl ⬝
           !pwhisker_left_refl⁻¹ ◾** !pwhisker_right_refl⁻¹
   end
@@ -514,7 +514,7 @@ namespace pointed
   definition pcompose_left_eq_of_phomotopy {A B C : Type*} (g : B →* C) {f f' : A →* B}
     (H : f ~* f') : ap (λf, g ∘* f) (eq_of_phomotopy H) = eq_of_phomotopy (pwhisker_left g H) :=
   begin
-    induction H using phomotopy_rec_on_idp,
+    induction H using phomotopy_rec_idp,
     refine ap02 _ !eq_of_phomotopy_refl ⬝ !eq_of_phomotopy_refl⁻¹ ⬝ ap eq_of_phomotopy _,
     exact !pwhisker_left_refl⁻¹
   end
@@ -522,7 +522,7 @@ namespace pointed
   definition pcompose_right_eq_of_phomotopy {A B C : Type*} {g g' : B →* C} (f : A →* B)
     (H : g ~* g') : ap (λg, g ∘* f) (eq_of_phomotopy H) = eq_of_phomotopy (pwhisker_right f H) :=
   begin
-    induction H using phomotopy_rec_on_idp,
+    induction H using phomotopy_rec_idp,
     refine ap02 _ !eq_of_phomotopy_refl ⬝ !eq_of_phomotopy_refl⁻¹ ⬝ ap eq_of_phomotopy _,
     exact !pwhisker_right_refl⁻¹
   end
@@ -606,9 +606,9 @@ namespace pointed
     fapply pequiv.MK',
     { exact papply B tt },
     { exact pbool_pmap },
-    { intro f, fapply pmap_eq,
+    { intro f, fapply eq_of_phomotopy, fapply phomotopy.mk,
       { intro b, cases b, exact !respect_pt⁻¹, reflexivity },
-      { exact !con.left_inv⁻¹ }},
+      { exact !con.left_inv }},
     { intro b, reflexivity },
   end
 
@@ -628,7 +628,7 @@ namespace pointed
   begin
     assert H : Π(p : pconst A B ~* f),
       pconst_pcompose f = pwhisker_left (pconst B C) p⁻¹* ⬝* pcompose_pconst (pconst B C),
-    { intro p, induction p using phomotopy_rec_on_idp, reflexivity },
+    { intro p, induction p using phomotopy_rec_idp, reflexivity },
     refine H p⁻¹* ⬝ ap (pwhisker_left _) !symm_symm ◾** idp,
   end
 
@@ -702,7 +702,7 @@ namespace pointed
   begin
     fapply phomotopy_eq,
     { intro a, exact to_homotopy_pt p },
-    { induction p using phomotopy_rec_on_idp, induction C with C c₀, induction f with f f₀,
+    { induction p using phomotopy_rec_idp, induction C with C c₀, induction f with f f₀,
       esimp at *, induction f₀, reflexivity }
   end
 
@@ -731,13 +731,13 @@ namespace pointed
   definition ppcompose_left_phomotopy [constructor] {A B C : Type*} {g g' : B →* C} (p : g ~* g') :
     @ppcompose_left A _ _ g ~* ppcompose_left g' :=
   begin
-    induction p using phomotopy_rec_on_idp,
+    induction p using phomotopy_rec_idp,
     reflexivity
   end
 
   definition ppcompose_left_phomotopy_refl {A B C : Type*} (g : B →* C) :
     ppcompose_left_phomotopy (phomotopy.refl g) = phomotopy.refl (@ppcompose_left A _ _ g) :=
-  !phomotopy_rec_on_idp_refl
+  !phomotopy_rec_idp_refl
 
     /- a more explicit proof of ppcompose_left_phomotopy, which might be useful if we need to prove properties about it
     -/
@@ -749,7 +749,7 @@ namespace pointed
   definition ppcompose_right_phomotopy [constructor] {A B C : Type*} {f f' : A →* B} (p : f ~* f') :
     @ppcompose_right _ _ C f ~* ppcompose_right f' :=
   begin
-    induction p using phomotopy_rec_on_idp,
+    induction p using phomotopy_rec_idp,
     reflexivity
   end
 
@@ -791,12 +791,12 @@ namespace pointed
   theorem pwhisker_left_phomotopy_hconcat {f₀₁'} (r : f₀₁' ~* f₀₁)
     (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : psquare f₁₂ f₁₄ f₀₃ f₂₃) :
     pwhisker_left f₀₃ r ⬝ph* (p ⬝v* q) = (r ⬝ph* p) ⬝v* q :=
-  by induction r using phomotopy_rec_on_idp; rewrite [pwhisker_left_refl, +refl_phomotopy_hconcat]
+  by induction r using phomotopy_rec_idp; rewrite [pwhisker_left_refl, +refl_phomotopy_hconcat]
 
   theorem pvcompose_pwhisker_left {f₀₁'} (r : f₀₁ ~* f₀₁')
     (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : psquare f₁₂ f₁₄ f₀₃ f₂₃) :
     (p ⬝v* q) ⬝* (pwhisker_left f₁₄ (pwhisker_left f₀₃ r)) = (p ⬝* pwhisker_left f₁₂ r) ⬝v* q :=
-  by induction r using phomotopy_rec_on_idp; rewrite [+pwhisker_left_refl, + trans_refl]
+  by induction r using phomotopy_rec_idp; rewrite [+pwhisker_left_refl, + trans_refl]
 
   definition phconcat2 {p p' : psquare f₁₀ f₁₂ f₀₁ f₂₁} {q q' : psquare f₃₀ f₃₂ f₂₁ f₄₁}
     (r : p = p') (s : q = q') : p ⬝h* q = p' ⬝h* q' :=