From 9a693f1ee3117f893069151ba139b2df1d7b2067 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Fri, 21 Jul 2017 15:55:27 +0100
Subject: [PATCH] define pmap in terms of ppi. Also move many facts about ppi
 to the standard library

---
 algebra/arrow_group.hlean     | 251 +++++++++----------
 algebra/cogroup.hlean         |  12 +-
 cohomology/serre.hlean        |   6 +-
 colim.hlean                   |   4 +-
 homology/basic.hlean          |  14 +-
 homotopy/EM.hlean             |   8 +-
 homotopy/degree.hlean         |  10 +-
 homotopy/fwedge.hlean         |   6 +-
 homotopy/realprojective.hlean |   2 +-
 homotopy/smash.hlean          |  20 +-
 homotopy/smash_adjoint.hlean  |   4 +-
 homotopy/wedge.hlean          |   6 +-
 move_to_lib.hlean             |  35 +--
 pointed.hlean                 |  23 +-
 pointed_cubes.hlean           |  20 +-
 pointed_pi.hlean              | 439 +++++++++-------------------------
 spectrum/basic.hlean          |  32 +--
 spectrum/trunc.hlean          |   5 +-
 18 files changed, 323 insertions(+), 574 deletions(-)

diff --git a/algebra/arrow_group.hlean b/algebra/arrow_group.hlean
index 0f7550d..3db123c 100644
--- a/algebra/arrow_group.hlean
+++ b/algebra/arrow_group.hlean
@@ -4,24 +4,132 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn, Ulrik Buchholtz
 
 Various groups of maps. Most importantly we define a group structure
-on trunc 0 (A →* Ω B), which is used in the definition of cohomology.
+on trunc 0 (A →* Ω B) and the dependent version trunc 0 (ppi _ _),
+which are used in the definition of cohomology.
 -/
 
 import algebra.group_theory ..pointed ..pointed_pi eq2
 open pi pointed algebra group eq equiv is_trunc trunc susp
 namespace group
 
+  /- Group of dependent functions into a loop space -/
+  definition ppi_mul [constructor] {A : Type*} {B : A → Type*} (f g : Π*a, Ω (B a)) : Π*a, Ω (B a) :=
+  proof ppi.mk (λa, f a ⬝ g a) (respect_pt f ◾ respect_pt g ⬝ !idp_con) qed
+
+  definition ppi_inv [constructor] {A : Type*} {B : A → Type*} (f : Π*a, Ω (B a)) : Π*a, Ω (B a) :=
+  proof ppi.mk (λa, (f a)⁻¹ᵖ) (respect_pt f)⁻² qed
+
+  definition inf_group_ppi [constructor] [instance] {A : Type*} (B : A → Type*) :
+    inf_group (Π*a, Ω (B a)) :=
+  begin
+    fapply inf_group.mk,
+    { exact ppi_mul },
+    { intro f g h, apply eq_of_phomotopy, fapply phomotopy.mk,
+      { intro a, exact con.assoc (f a) (g a) (h a) },
+      { symmetry, rexact eq_of_square (con2_assoc (respect_pt f) (respect_pt g) (respect_pt h)) }},
+    { apply ppi_const },
+    { intros f, apply eq_of_phomotopy, fapply phomotopy.mk,
+      { intro a, exact one_mul (f a) },
+      { symmetry, apply eq_of_square, refine _ ⬝vp !ap_id, apply natural_square_tr }},
+    { intros f, apply eq_of_phomotopy, fapply phomotopy.mk,
+      { intro a, exact mul_one (f a) },
+      { reflexivity }},
+    { exact ppi_inv },
+    { intro f, apply eq_of_phomotopy, fapply phomotopy.mk,
+      { intro a, exact con.left_inv (f a) },
+      { exact !con_left_inv_idp }},
+  end
+
+  definition group_trunc_ppi [constructor] [instance] {A : Type*} (B : A → Type*) :
+    group (trunc 0 (Π*a, Ω (B a))) :=
+  !trunc_group
+
+  definition Group_trunc_ppi [reducible] [constructor] {A : Type*} (B : A → Type*) : Group :=
+  Group.mk (trunc 0 (Π*a, Ω (B a))) _
+
+  definition ab_inf_group_ppi [constructor] [instance] {A : Type*} (B : A → Type*) :
+    ab_inf_group (Π*a, Ω (Ω (B a))) :=
+  ⦃ab_inf_group, inf_group_ppi (λa, Ω (B a)), mul_comm :=
+    begin
+      intro f g, apply eq_of_phomotopy, fapply phomotopy.mk,
+      { intro a, exact eckmann_hilton (f a) (g a) },
+      { symmetry, rexact eq_of_square (eckmann_hilton_con2 (respect_pt f) (respect_pt g)) }
+    end⦄
+
+  definition ab_group_trunc_ppi [constructor] [instance] {A : Type*} (B : A → Type*) :
+    ab_group (trunc 0 (Π*a, Ω (Ω (B a)))) :=
+  !trunc_ab_group
+
+  definition AbGroup_trunc_ppi [reducible] [constructor] {A : Type*} (B : A → Type*) : AbGroup :=
+  AbGroup.mk (trunc 0 (Π*a, Ω (Ω (B a)))) _
+
+  definition trunc_ppi_isomorphic_pmap (A B : Type*)
+    : Group.mk (trunc 0 (Π*(a : A), Ω B)) !trunc_group
+      ≃g Group.mk (trunc 0 (A →* Ω B)) !trunc_group :=
+  begin
+    apply trunc_isomorphism_of_equiv (pppi_equiv_pmap A (Ω B)),
+    intro h k, induction h with h h_pt, induction k with k k_pt, reflexivity
+  end
+
+  section
+
+  universe variables u v
+
+  variables {A : pType.{u}} {B : A → Type.{v}} {x₀ : B pt} {k l m : ppi B x₀}
+
+  definition phomotopy_of_eq_homomorphism (p : k = l) (q : l = m)
+    : phomotopy_of_eq (p ⬝ q) = phomotopy_of_eq p ⬝* phomotopy_of_eq q :=
+  begin
+    induction q, induction p, induction k with k q, induction q, reflexivity
+  end
+
+  protected definition ppi_mul_loop.lemma1 {X : Type} {x : X} (p q : x = x) (p_pt : idp = p) (q_pt : idp = q)
+    : refl (p ⬝ q) ⬝ whisker_left p q_pt⁻¹ ⬝ p_pt⁻¹ = p_pt⁻¹ ◾ q_pt⁻¹ :=
+  by induction p_pt; induction q_pt; reflexivity
+
+  protected definition ppi_mul_loop.lemma2 {X : Type} {x : X} (p q : x = x) (p_pt : p = idp) (q_pt : q = idp)
+    : refl (p ⬝ q) ⬝ whisker_left p q_pt ⬝ p_pt = p_pt ◾ q_pt :=
+  by rewrite [-(inv_inv p_pt),-(inv_inv q_pt)]; exact ppi_mul_loop.lemma1 p q p_pt⁻¹ q_pt⁻¹
+
+  definition ppi_mul_loop {h : Πa, B a} (f g : ppi.mk h idp ~* ppi.mk h idp) : f ⬝* g = ppi_mul f g :=
+  begin
+    apply ap (ppi.mk (λa, f a ⬝ g a)),
+    apply ppi.rec_on f, intros f' f_pt, apply ppi.rec_on g, intros g' g_pt,
+    clear f g, esimp at *, exact ppi_mul_loop.lemma2 (f' pt) (g' pt) f_pt g_pt
+  end
+
+  variable (k)
+
+  definition trunc_ppi_loop_isomorphism_lemma
+    : isomorphism.{(max u v) (max u v)}
+      (Group.mk (trunc 0 (k = k)) (@trunc_group (k = k) !inf_group_loop))
+      (Group.mk (trunc 0 (Π*(a : A), Ω (pType.mk (B a) (k a)))) !trunc_group) :=
+  begin
+    apply @trunc_isomorphism_of_equiv _ _ !inf_group_loop !inf_group_ppi (ppi_loop_equiv k),
+    intro f g, induction k with k p, induction p,
+    apply trans (phomotopy_of_eq_homomorphism f g),
+    exact ppi_mul_loop (phomotopy_of_eq f) (phomotopy_of_eq g)
+  end
+
+  end
+
+  definition trunc_ppi_loop_isomorphism {A : Type*} (B : A → Type*)
+    : Group.mk (trunc 0 (Ω (Π*(a : A), B a))) !trunc_group
+      ≃g Group.mk (trunc 0 (Π*(a : A), Ω (B a))) !trunc_group :=
+  trunc_ppi_loop_isomorphism_lemma (ppi_const B)
+
+
   /- We first define the group structure on A →* Ω B (except for truncatedness).
      Instead of Ω B, we could also choose any infinity group. However, we need various 2-coherences,
      so it's easier to just do it for the loop space. -/
   definition pmap_mul [constructor] {A B : Type*} (f g : A →* Ω B) : A →* Ω B :=
-  pmap.mk (λa, f a ⬝ g a) (respect_pt f ◾ respect_pt g ⬝ !idp_con)
+  ppi_mul f g
 
   definition pmap_inv [constructor] {A B : Type*} (f : A →* Ω B) : A →* Ω B :=
-  pmap.mk (λa, (f a)⁻¹ᵖ) (respect_pt f)⁻²
+  ppi_inv f
 
-  /- we prove some coherences of the multiplication. We don't need them for the group structure, but they
-     are used to show that cohomology satisfies the Eilenberg-Steenrod axioms -/
+  /- we prove some coherences of the multiplication. We don't need them for the group structure,
+    but they are used to show that cohomology satisfies the Eilenberg-Steenrod axioms -/
   definition ap1_pmap_mul {X Y : Type*} (f g : X →* Ω Y) :
     Ω→ (pmap_mul f g) ~* pmap_mul (Ω→ f) (Ω→ g) :=
   begin
@@ -63,24 +171,7 @@ namespace group
   pwhisker_right _ !ap1_pmap_mul ⬝* !pmap_mul_pcompose
 
   definition inf_group_pmap [constructor] [instance] (A B : Type*) : inf_group (A →* Ω B) :=
-  begin
-    fapply inf_group.mk,
-    { exact pmap_mul },
-    { intro f g h, fapply pmap_eq,
-      { intro a, exact con.assoc (f a) (g a) (h a) },
-      { rexact eq_of_square (con2_assoc (respect_pt f) (respect_pt g) (respect_pt h)) }},
-    { apply pconst },
-    { intros f, fapply pmap_eq,
-      { intro a, exact one_mul (f a) },
-      { esimp, apply eq_of_square, refine _ ⬝vp !ap_id, apply natural_square_tr }},
-    { intros f, fapply pmap_eq,
-      { intro a, exact mul_one (f a) },
-      { reflexivity }},
-    { exact pmap_inv },
-    { intro f, fapply pmap_eq,
-      { intro a, exact con.left_inv (f a) },
-      { exact !con_left_inv_idp⁻¹ }},
-  end
+  !inf_group_ppi
 
   definition group_trunc_pmap [constructor] [instance] (A B : Type*) : group (trunc 0 (A →* Ω B)) :=
   !trunc_group
@@ -94,9 +185,9 @@ namespace group
     fapply homomorphism.mk,
     { apply trunc_functor, intro g, exact g ∘* f},
     { intro g h, induction g with g, induction h with h, apply ap tr,
-      fapply pmap_eq,
+      apply eq_of_phomotopy, fapply phomotopy.mk,
       { intro a, reflexivity },
-      { refine _ ⬝ !idp_con⁻¹,
+      { symmetry, refine _ ⬝ !idp_con⁻¹,
         refine whisker_right _ !ap_con_fn ⬝ _, apply con2_con_con2 }}
   end
 
@@ -152,9 +243,9 @@ namespace group
     ab_inf_group (A →* Ω (Ω B)) :=
   ⦃ab_inf_group, inf_group_pmap A (Ω B), mul_comm :=
     begin
-      intro f g, fapply pmap_eq,
+      intro f g, apply eq_of_phomotopy, fapply phomotopy.mk,
       { intro a, exact eckmann_hilton (f a) (g a) },
-      { rexact eq_of_square (eckmann_hilton_con2 (respect_pt f) (respect_pt g)) }
+      { symmetry, rexact eq_of_square (eckmann_hilton_con2 (respect_pt f) (respect_pt g)) }
     end⦄
 
   definition ab_group_trunc_pmap [constructor] [instance] (A B : Type*) :
@@ -195,110 +286,4 @@ namespace group
     { intro g h, apply eq_of_homotopy, intro a, exact respect_mul (f a) g h }
   end
 
-  /- Group of dependent functions into a loop space -/
-  definition ppi_mul [constructor] {A : Type*} {B : A → Type*} (f g : Π*a, Ω (B a)) : Π*a, Ω (B a) :=
-  proof ppi.mk (λa, f a ⬝ g a) (ppi.resp_pt f ◾ ppi.resp_pt g ⬝ !idp_con) qed
-
-  definition ppi_inv [constructor] {A : Type*} {B : A → Type*} (f : Π*a, Ω (B a)) : Π*a, Ω (B a) :=
-  proof ppi.mk (λa, (f a)⁻¹ᵖ) (ppi.resp_pt f)⁻² qed
-
-  definition inf_group_ppi [constructor] [instance] {A : Type*} (B : A → Type*) :
-    inf_group (Π*a, Ω (B a)) :=
-  begin
-    fapply inf_group.mk,
-    { exact ppi_mul },
-    { intro f g h, apply ppi_eq, fapply ppi_homotopy.mk,
-      { intro a, exact con.assoc (f a) (g a) (h a) },
-      { symmetry, rexact eq_of_square (con2_assoc (ppi.resp_pt f) (ppi.resp_pt g) (ppi.resp_pt h)) }},
-    { apply ppi_const },
-    { intros f, apply ppi_eq, fapply ppi_homotopy.mk,
-      { intro a, exact one_mul (f a) },
-      { symmetry, apply eq_of_square, refine _ ⬝vp !ap_id, apply natural_square_tr }},
-    { intros f, apply ppi_eq, fapply ppi_homotopy.mk,
-      { intro a, exact mul_one (f a) },
-      { reflexivity }},
-    { exact ppi_inv },
-    { intro f, apply ppi_eq, fapply ppi_homotopy.mk,
-      { intro a, exact con.left_inv (f a) },
-      { exact !con_left_inv_idp }},
-  end
-
-  definition group_trunc_ppi [constructor] [instance] {A : Type*} (B : A → Type*) :
-    group (trunc 0 (Π*a, Ω (B a))) :=
-  !trunc_group
-
-  definition Group_trunc_ppi [reducible] [constructor] {A : Type*} (B : A → Type*) : Group :=
-  Group.mk (trunc 0 (Π*a, Ω (B a))) _
-
-  definition ab_inf_group_ppi [constructor] [instance] {A : Type*} (B : A → Type*) :
-    ab_inf_group (Π*a, Ω (Ω (B a))) :=
-  ⦃ab_inf_group, inf_group_ppi (λa, Ω (B a)), mul_comm :=
-    begin
-      intro f g, apply ppi_eq, fapply ppi_homotopy.mk,
-      { intro a, exact eckmann_hilton (f a) (g a) },
-      { symmetry, rexact eq_of_square (eckmann_hilton_con2 (ppi.resp_pt f) (ppi.resp_pt g)) }
-    end⦄
-
-  definition ab_group_trunc_ppi [constructor] [instance] {A : Type*} (B : A → Type*) :
-    ab_group (trunc 0 (Π*a, Ω (Ω (B a)))) :=
-  !trunc_ab_group
-
-  definition AbGroup_trunc_ppi [reducible] [constructor] {A : Type*} (B : A → Type*) : AbGroup :=
-  AbGroup.mk (trunc 0 (Π*a, Ω (Ω (B a)))) _
-
-  definition trunc_ppi_isomorphic_pmap (A B : Type*)
-    : Group.mk (trunc 0 (Π*(a : A), Ω B)) !trunc_group
-      ≃g Group.mk (trunc 0 (A →* Ω B)) !trunc_group :=
-  begin
-    apply trunc_isomorphism_of_equiv (pppi_equiv_pmap A (Ω B)),
-    intro h k, induction h with h h_pt, induction k with k k_pt, reflexivity
-  end
-
-  section
-
-  universe variables u v
-
-  variables {A : pType.{u}} {B : A → Type.{v}} {x₀ : B pt} {k l m : ppi B x₀}
-
-  definition ppi_homotopy_of_eq_homomorphism (p : k = l) (q : l = m)
-    : ppi_homotopy_of_eq (p ⬝ q) = ppi_homotopy_of_eq p ⬝*' ppi_homotopy_of_eq q :=
-  begin
-    induction q, induction p, induction k with k q, induction q, reflexivity
-  end
-
-  protected definition ppi_mul_loop.lemma1 {X : Type} {x : X} (p q : x = x) (p_pt : idp = p) (q_pt : idp = q)
-    : refl (p ⬝ q) ⬝ whisker_left p q_pt⁻¹ ⬝ p_pt⁻¹ = p_pt⁻¹ ◾ q_pt⁻¹ :=
-  by induction p_pt; induction q_pt; reflexivity
-
-  protected definition ppi_mul_loop.lemma2 {X : Type} {x : X} (p q : x = x) (p_pt : p = idp) (q_pt : q = idp)
-    : refl (p ⬝ q) ⬝ whisker_left p q_pt ⬝ p_pt = p_pt ◾ q_pt :=
-  by rewrite [-(inv_inv p_pt),-(inv_inv q_pt)]; exact ppi_mul_loop.lemma1 p q p_pt⁻¹ q_pt⁻¹
-
-  definition ppi_mul_loop {h : Πa, B a} (f g : ppi.mk h idp ~~* ppi.mk h idp) : f ⬝*' g = ppi_mul f g :=
-  begin
-    apply ap (ppi.mk (λa, f a ⬝ g a)),
-    apply ppi.rec_on f, intros f' f_pt, apply ppi.rec_on g, intros g' g_pt,
-    clear f g, esimp at *, exact ppi_mul_loop.lemma2 (f' pt) (g' pt) f_pt g_pt
-  end
-
-  variable (k)
-
-  definition trunc_ppi_loop_isomorphism_lemma
-    : isomorphism.{(max u v) (max u v)}
-      (Group.mk (trunc 0 (k = k)) (@trunc_group (k = k) !inf_group_loop))
-      (Group.mk (trunc 0 (Π*(a : A), Ω (pType.mk (B a) (k a)))) !trunc_group) :=
-  begin
-    apply @trunc_isomorphism_of_equiv _ _ !inf_group_loop !inf_group_ppi (ppi_loop_equiv k),
-    intro f g, induction k with k p, induction p,
-    apply trans (ppi_homotopy_of_eq_homomorphism f g),
-    exact ppi_mul_loop (ppi_homotopy_of_eq f) (ppi_homotopy_of_eq g)
-  end
-
-  end
-
-  definition trunc_ppi_loop_isomorphism {A : Type*} (B : A → Type*)
-    : Group.mk (trunc 0 (Ω (Π*(a : A), B a))) !trunc_group
-      ≃g Group.mk (trunc 0 (Π*(a : A), Ω (B a))) !trunc_group :=
-  trunc_ppi_loop_isomorphism_lemma (ppi_const B)
-
 end group
diff --git a/algebra/cogroup.hlean b/algebra/cogroup.hlean
index 563167b..dc9eaed 100644
--- a/algebra/cogroup.hlean
+++ b/algebra/cogroup.hlean
@@ -16,17 +16,17 @@ section
     apply equiv.MK (λ f, (ppr1 ∘* f, ppr2 ∘* f))
                    (λ w, prod.elim w prod.pair_pmap),
     { intro p, induction p with f g, apply pair_eq,
-      { fapply pmap_eq,
+      { apply eq_of_phomotopy, fapply phomotopy.mk,
         { intro x, reflexivity },
-        { apply trans (prod_eq_pr1 (respect_pt f) (respect_pt g)),
+        { symmetry, apply trans (prod_eq_pr1 (respect_pt f) (respect_pt g)),
           apply inverse, apply idp_con } },
-      { fapply pmap_eq,
+      { apply eq_of_phomotopy, fapply phomotopy.mk,
         { intro x, reflexivity },
-        { apply trans (prod_eq_pr2 (respect_pt f) (respect_pt g)),
+        { symmetry, apply trans (prod_eq_pr2 (respect_pt f) (respect_pt g)),
           apply inverse, apply idp_con } } },
-    { intro f, fapply pmap_eq,
+    { intro f, apply eq_of_phomotopy, fapply phomotopy.mk,
       { intro x, apply prod.eta },
-      { exact prod.pair_eq_eta (respect_pt f) } }
+      { symmetry, exact prod.pair_eq_eta (respect_pt f) } }
   end
 
   -- since ~* is the identity type of pointed maps,
diff --git a/cohomology/serre.hlean b/cohomology/serre.hlean
index 9aec38d..035d1d3 100644
--- a/cohomology/serre.hlean
+++ b/cohomology/serre.hlean
@@ -111,11 +111,11 @@ definition postnikov_smap_postnikov_map (A : spectrum) (n k l : ℤ) (p : n + k
     (ptrunc_maxm2_change_int p (A k)) (ptrunc_maxm2_pred (A k) (ap pred p⁻¹ ⬝ add.right_comm n k (- 1))) :=
 begin
   cases l with l,
-  { cases l with l, apply phomotopy_of_is_contr_cod, apply is_contr_ptrunc_minus_one,
+  { cases l with l, apply phomotopy_of_is_contr_cod_pmap, apply is_contr_ptrunc_minus_one,
     refine psquare_postnikov_map_ptrunc_elim (A k) _ _ _ ⬝hp* _,
     exact ap maxm2 (add.right_comm n (- 1) k ⬝ ap pred p ⬝ !pred_succ),
     apply ptrunc_maxm2_pred_nat },
-  { apply phomotopy_of_is_contr_cod, apply is_trunc_trunc }
+  { apply phomotopy_of_is_contr_cod_pmap, apply is_trunc_trunc }
 end
 
 definition sfiber_postnikov_smap_pequiv (A : spectrum) (n : ℤ) (k : ℤ) :
@@ -148,7 +148,7 @@ section atiyah_hirzebruch
       (ppi_pequiv_right (λx, ptrunc_pequiv_ptrunc_of_is_trunc _ _ (H x n))) _,
     { intro x, apply maxm2_monotone, apply add_le_add_right, exact le.trans !le_add_one Hs },
     { intro x, apply maxm2_monotone, apply add_le_add_right, exact le_sub_one_of_lt Hs },
-    intro f, apply eq_of_ppi_homotopy,
+    intro f, apply eq_of_phomotopy,
     apply pmap_compose_ppi_phomotopy_left, intro x,
     fapply phomotopy.mk,
     { refine @trunc.rec _ _ _ _ _,
diff --git a/colim.hlean b/colim.hlean
index 5d398a6..2e822c7 100644
--- a/colim.hlean
+++ b/colim.hlean
@@ -246,7 +246,7 @@ namespace seq_colim
   begin
     fapply pequiv_of_equiv,
     { apply shift_equiv },
-    { exact ap (ι _) !respect_pt }
+    { exact ap (ι _) (respect_pt (f 0)) }
   end
 
   definition pshift_equiv_pinclusion {A : ℕ → Type*} (f : Πn, A n →* A (succ n)) (n : ℕ) :
@@ -356,7 +356,7 @@ namespace seq_colim
       xrewrite[-IH],
       rewrite[-+ap_compose', -+con.assoc],
       apply whisker_right, esimp,
-      rewrite[(eq_con_inv_of_con_eq (!to_homotopy_pt))],
+      rewrite[(eq_con_inv_of_con_eq (to_homotopy_pt (@p _)))],
       rewrite[ap_con], esimp,
       rewrite[-+con.assoc, ap_con, -ap_compose', +ap_inv],
       rewrite[-+con.assoc],
diff --git a/homology/basic.hlean b/homology/basic.hlean
index 30aff2b..0ead27e 100644
--- a/homology/basic.hlean
+++ b/homology/basic.hlean
@@ -56,7 +56,12 @@ namespace homology
     calc       Hh theory n f x
              = Hh theory n (pmap.mk f (respect_pt f)) x : by exact ap (λ f, Hh theory n f x) (pmap.eta f)⁻¹
          ... = Hh theory n (pmap.mk f (h pt ⬝ respect_pt g)) x : by exact Hh_homotopy' n f (respect_pt f) (h pt ⬝ respect_pt g) x
-         ... = Hh theory n g x : by exact ap (λ f, Hh theory n f x) (@pmap_eq _ _ (pmap.mk f (h pt ⬝ respect_pt g)) _ h (refl (h pt ⬝ respect_pt g)))
+         ... = Hh theory n g x :
+               begin
+                 apply ap (λ f, Hh theory n f x), apply eq_of_phomotopy, fapply phomotopy.mk,
+                 { exact h },
+                 reflexivity
+               end
 
     definition HH_isomorphism (n : ℤ) {A B : Type*} (e : A ≃* B)
       : HH theory n A ≃g HH theory n B :=
@@ -175,12 +180,9 @@ definition homology_functor [constructor] {X Y : Type*} {E F : prespectrum} (f :
   (g : E →ₛ F) (n : ℤ) : homology X E n →g homology Y F n :=
 pshomotopy_group_fun n (smash_prespectrum_fun f g)
 
-print is_exact_g
-print is_exact
-definition homology_theory_spectrum_is_exact.{u} (E : spectrum.{u}) (n : ℤ) {X Y : Type*} (f : X →* Y) :
-  is_exact_g (homology_functor f (sid E) n) (homology_functor (pcod f) (sid E) n) :=
+definition homology_theory_spectrum_is_exact.{u} (E : spectrum.{u}) (n : ℤ) {X Y : Type*}
+  (f : X →* Y) : is_exact_g (homology_functor f (sid E) n) (homology_functor (pcod f) (sid E) n) :=
 begin
-  esimp [is_exact_g],
   -- fconstructor,
   -- { intro a, exact sorry },
   -- { intro a, exact sorry }
diff --git a/homotopy/EM.hlean b/homotopy/EM.hlean
index 1ac553b..9f75635 100644
--- a/homotopy/EM.hlean
+++ b/homotopy/EM.hlean
@@ -585,12 +585,14 @@ namespace EM
 
   /- fiber of EM_functor -/
   open fiber
-  definition is_trunc_fiber_EM1_functor {G H : Group} (φ : G →g H) : is_trunc 1 (pfiber (EM1_functor φ)) :=
+  definition is_trunc_fiber_EM1_functor {G H : Group} (φ : G →g H) :
+    is_trunc 1 (pfiber (EM1_functor φ)) :=
   !is_trunc_fiber
 
-  definition is_conn_fiber_EM1_functor {G H : Group} (φ : G →g H) : is_conn -1 (pfiber (EM1_functor φ)) :=
+  definition is_conn_fiber_EM1_functor {G H : Group} (φ : G →g H) :
+    is_conn -1 (pfiber (EM1_functor φ)) :=
   begin
-    apply is_conn_fiber, apply is_conn_of_is_conn_succ
+    apply is_conn_fiber
   end
 
   definition is_trunc_fiber_EMadd1_functor {G H : AbGroup} (φ : G →g H) (n : ℕ) :
diff --git a/homotopy/degree.hlean b/homotopy/degree.hlean
index bc8635b..7a69dbe 100644
--- a/homotopy/degree.hlean
+++ b/homotopy/degree.hlean
@@ -79,7 +79,7 @@ namespace sphere
 --                 (pair 1 2))
 --              (tr surf))
 
-  definition πnSn_surf (n : ℕ) : πnSn n (tr surf) = 1 :> ℤ :=
+  definition πnSn_surf (n : ℕ) : πnSn (n+1) (tr surf) = 1 :> ℤ :=
   begin
     cases n with n IH,
     { refine ap (πnSn _ ∘ tr) surf_eq_loop ⬝ _, apply transport_code_loop },
@@ -87,17 +87,17 @@ namespace sphere
   end
 
   definition deg {n : ℕ} [H : is_succ n] (f : S n →* S n) : ℤ :=
-  by induction H with n; exact πnSn n (π→g[n+1] f (tr surf))
+  by induction H with n; exact πnSn (n+1) (π→g[n+1] f (tr surf))
 
   definition deg_id (n : ℕ) [H : is_succ n] : deg (pid (S n)) = (1 : ℤ) :=
   by induction H with n;
-     exact ap (πnSn n) (homotopy_group_functor_pid (succ n) (S (succ n)) (tr surf)) ⬝ πnSn_surf n
+     exact ap (πnSn (n+1)) (homotopy_group_functor_pid (succ n) (S (succ n)) (tr surf)) ⬝ πnSn_surf n
 
   definition deg_phomotopy {n : ℕ} [H : is_succ n] {f g : S n →* S n} (p : f ~* g) :
     deg f = deg g :=
   begin
     induction H with n,
-    exact ap (πnSn n) (homotopy_group_functor_phomotopy (succ n) p (tr surf)),
+    exact ap (πnSn (n+1)) (homotopy_group_functor_phomotopy (succ n) p (tr surf)),
   end
 
   definition endomorphism_int (f : gℤ →g gℤ) (n : ℤ) : f n = f (1 : ℤ) *[ℤ] n :=
@@ -119,7 +119,7 @@ namespace sphere
     deg (g ∘* f) = deg g *[ℤ] deg f :=
   begin
     induction H with n,
-    refine ap (πnSn n) (homotopy_group_functor_compose (succ n) g f (tr surf)) ⬝ _,
+    refine ap (πnSn (n+1)) (homotopy_group_functor_compose (succ n) g f (tr surf)) ⬝ _,
     apply endomorphism_equiv_Z !πnSn !πnSn_surf (π→g[n+1] g)
   end
 
diff --git a/homotopy/fwedge.hlean b/homotopy/fwedge.hlean
index 387e389..c249aa2 100644
--- a/homotopy/fwedge.hlean
+++ b/homotopy/fwedge.hlean
@@ -96,7 +96,7 @@ namespace fwedge
 
   definition fwedge_pmap [constructor] {I : Type} {F : I → Type*} {X : Type*} (f : Πi, F i →* X) : ⋁F →* X :=
   begin
-    fconstructor,
+    fapply pmap.mk,
     { intro x, induction x,
         exact f i x,
         exact pt,
@@ -205,9 +205,9 @@ namespace fwedge
   definition fwedge_pmap_nat_square {A B X Y : Type*} (f : X →* Y) :
        hsquare (fwedge_pmap_equiv (bool.rec A B) X)⁻¹ᵉ (fwedge_pmap_equiv (bool.rec A B) Y)⁻¹ᵉ (left_comp_pi_bool_funct f) (pcompose f) :=
   begin
-   intro h, esimp, fapply pmap_eq,
+   intro h, esimp, fapply eq_of_phomotopy, fapply phomotopy.mk,
    exact fwedge_pmap_nat₂ (λ u, bool.rec A B u) f h,
-   esimp,
+   reflexivity
   end
 
 -- hsquare 3:
diff --git a/homotopy/realprojective.hlean b/homotopy/realprojective.hlean
index 1dc0a54..e4eaec0 100644
--- a/homotopy/realprojective.hlean
+++ b/homotopy/realprojective.hlean
@@ -3,7 +3,7 @@
 
 import homotopy.join
 
-open eq nat susp pointed pmap sigma is_equiv equiv fiber is_trunc trunc
+open eq nat susp pointed sigma is_equiv equiv fiber is_trunc trunc
   trunc_index is_conn bool unit join pushout
 
 definition of_is_contr (A : Type) : is_contr A → A := @center A
diff --git a/homotopy/smash.hlean b/homotopy/smash.hlean
index 04d0fd4..137b92a 100644
--- a/homotopy/smash.hlean
+++ b/homotopy/smash.hlean
@@ -228,8 +228,8 @@ namespace smash
   definition smash_functor_phomotopy {f f' : A →* C} {g g' : B →* D}
     (h₁ : f ~* f') (h₂ : g ~* g') : f ∧→ g ~* f' ∧→ g' :=
   begin
-    induction h₁ using phomotopy_rec_on_idp,
-    induction h₂ using phomotopy_rec_on_idp,
+    induction h₁ using phomotopy_rec_idp,
+    induction h₂ using phomotopy_rec_idp,
     reflexivity
   end
 
@@ -265,13 +265,13 @@ namespace smash
 
   definition smash_functor_phomotopy_refl (f : A →* C) (g : B →* D) :
     smash_functor_phomotopy (phomotopy.refl f) (phomotopy.refl g) = phomotopy.rfl :=
-  !phomotopy_rec_on_idp_refl ⬝ !phomotopy_rec_on_idp_refl
+  !phomotopy_rec_idp_refl ⬝ !phomotopy_rec_idp_refl
 
   definition smash_functor_phomotopy_symm {f₁ f₂ : A →* C} {g₁ g₂ : B →* D}
     (h : f₁ ~* f₂) (k : g₁ ~* g₂) :
     smash_functor_phomotopy h⁻¹* k⁻¹* = (smash_functor_phomotopy h k)⁻¹* :=
   begin
-    induction h using phomotopy_rec_on_idp, induction k using phomotopy_rec_on_idp,
+    induction h using phomotopy_rec_idp, induction k using phomotopy_rec_idp,
     exact ap011 smash_functor_phomotopy !refl_symm !refl_symm ⬝ !smash_functor_phomotopy_refl ⬝
       !refl_symm⁻¹ ⬝ !smash_functor_phomotopy_refl⁻¹⁻²**
   end
@@ -281,8 +281,8 @@ namespace smash
     smash_functor_phomotopy (h₁ ⬝* h₂) (k₁ ⬝* k₂) =
     smash_functor_phomotopy h₁ k₁ ⬝* smash_functor_phomotopy h₂ k₂ :=
   begin
-    induction h₁ using phomotopy_rec_on_idp, induction h₂ using phomotopy_rec_on_idp,
-    induction k₁ using phomotopy_rec_on_idp, induction k₂ using phomotopy_rec_on_idp,
+    induction h₁ using phomotopy_rec_idp, induction h₂ using phomotopy_rec_idp,
+    induction k₁ using phomotopy_rec_idp, induction k₂ using phomotopy_rec_idp,
     refine ap011 smash_functor_phomotopy !trans_refl !trans_refl ⬝ !trans_refl⁻¹ ⬝ idp ◾** _,
     exact !smash_functor_phomotopy_refl⁻¹
   end
@@ -310,7 +310,7 @@ namespace smash
     (p : g ~* g') : ap (smash_functor f) (eq_of_phomotopy p) =
     eq_of_phomotopy (smash_functor_phomotopy phomotopy.rfl p) :=
   begin
-    induction p using phomotopy_rec_on_idp,
+    induction p using phomotopy_rec_idp,
     refine ap02 _ !eq_of_phomotopy_refl ⬝ _,
     refine !eq_of_phomotopy_refl⁻¹ ⬝ _,
     apply ap eq_of_phomotopy,
@@ -397,8 +397,8 @@ namespace smash
              (smash_functor_phomotopy (h₂ ◾* h₁) (k₂ ◾* k₁))
              (smash_functor_phomotopy h₂ k₂ ◾* smash_functor_phomotopy h₁ k₁) :=
   begin
-    induction h₁ using phomotopy_rec_on_idp, induction h₂ using phomotopy_rec_on_idp,
-    induction k₁ using phomotopy_rec_on_idp, induction k₂ using phomotopy_rec_on_idp,
+    induction h₁ using phomotopy_rec_idp, induction h₂ using phomotopy_rec_idp,
+    induction k₁ using phomotopy_rec_idp, induction k₂ using phomotopy_rec_idp,
     refine (ap011 smash_functor_phomotopy !pcompose2_refl !pcompose2_refl ⬝
       !smash_functor_phomotopy_refl) ⬝ph** phvrfl ⬝hp**
       (ap011 pcompose2 !smash_functor_phomotopy_refl !smash_functor_phomotopy_refl ⬝
@@ -457,7 +457,7 @@ namespace smash
     smash_functor_phomotopy p (phomotopy.refl (pconst B D)) ⬝* smash_functor_pconst_right f' =
     smash_functor_pconst_right f :=
   begin
-    induction p using phomotopy_rec_on_idp,
+    induction p using phomotopy_rec_idp,
     exact !smash_functor_phomotopy_refl ◾** idp ⬝ !refl_trans
   end
 
diff --git a/homotopy/smash_adjoint.hlean b/homotopy/smash_adjoint.hlean
index 4aa47c8..c910498 100644
--- a/homotopy/smash_adjoint.hlean
+++ b/homotopy/smash_adjoint.hlean
@@ -305,7 +305,7 @@ namespace smash
   definition smash_elim_eq_of_phomotopy {f f' : A →* ppmap B C}
     (p : f ~* f') : ap smash_elim (eq_of_phomotopy p) = eq_of_phomotopy (smash_elim_phomotopy p) :=
   begin
-    induction p using phomotopy_rec_on_idp,
+    induction p using phomotopy_rec_idp,
     refine ap02 _ !eq_of_phomotopy_refl ⬝ _,
     refine !eq_of_phomotopy_refl⁻¹ ⬝ _,
     apply ap eq_of_phomotopy,
@@ -316,7 +316,7 @@ namespace smash
   definition smash_elim_inv_eq_of_phomotopy {f f' : A ∧ B →* C} (p : f ~* f') :
     ap smash_elim_inv (eq_of_phomotopy p) = eq_of_phomotopy (smash_elim_inv_phomotopy p) :=
   begin
-    induction p using phomotopy_rec_on_idp,
+    induction p using phomotopy_rec_idp,
     refine ap02 _ !eq_of_phomotopy_refl ⬝ _,
     refine !eq_of_phomotopy_refl⁻¹ ⬝ _,
     apply ap eq_of_phomotopy,
diff --git a/homotopy/wedge.hlean b/homotopy/wedge.hlean
index 45e2531..d971bc3 100644
--- a/homotopy/wedge.hlean
+++ b/homotopy/wedge.hlean
@@ -28,8 +28,10 @@ namespace wedge
      exact ap_compose wedge_flip' _ _ ⬝ ap02 _ !elim_glue ⬝ !ap_inv ⬝ !elim_glue⁻² ⬝ !inv_inv }
   end
 
-  definition wedge_flip_wedge_flip (A B : Type*) : wedge_flip B A ∘* wedge_flip A B ~* pid (A ∨ B) :=
-  phomotopy.mk wedge_flip'_wedge_flip' (whisker_right _ (!ap_inv ⬝ !wedge.elim_glue⁻²) ⬝ !con.left_inv)⁻¹
+  definition wedge_flip_wedge_flip (A B : Type*) :
+    wedge_flip B A ∘* wedge_flip A B ~* pid (A ∨ B) :=
+  phomotopy.mk wedge_flip'_wedge_flip'
+    proof (whisker_right _ (!ap_inv ⬝ !wedge.elim_glue⁻²) ⬝ !con.left_inv)⁻¹ qed
 
   definition wedge_comm [constructor] (A B : Type*) : A ∨ B ≃* B ∨ A :=
   begin
diff --git a/move_to_lib.hlean b/move_to_lib.hlean
index 8413d76..93ef0f4 100644
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@@ -2,7 +2,7 @@
 
 import homotopy.sphere2 homotopy.cofiber homotopy.wedge hit.prop_trunc hit.set_quotient eq2 types.pointed2
 
-open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc pi group
+open eq nat int susp pointed sigma is_equiv equiv fiber algebra trunc pi group
      is_trunc function unit prod bool
 
 attribute pType.sigma_char sigma_pi_equiv_pi_sigma sigma.coind_unc [constructor]
@@ -149,31 +149,6 @@ namespace eq
     {D : Π⦃a⦄ ⦃b : B a⦄, C a b → Type} {f : Πa b (c : C a b), D c} : f ~3 f :=
   λa b c, idp
 
-  definition homotopy.rec_idp [recursor] {A : Type} {P : A → Type} {f : Πa, P a}
-    (Q : Π{g}, (f ~ g) → Type) (H : Q (homotopy.refl f)) {g : Π x, P x} (p : f ~ g) : Q p :=
-  homotopy.rec_on_idp p H
-
-  open funext
-  definition homotopy_rec_on_apd10 {A : Type} {P : A → Type} {f g : Πa, P a}
-    (Q : f ~ g → Type) (H : Π(q : f = g), Q (apd10 q)) (p : f = g) :
-    homotopy.rec_on (apd10 p) H = H p :=
-  begin
-    unfold [homotopy.rec_on],
-    refine ap (λp, p ▸ _) !adj ⬝ _,
-    refine !tr_compose⁻¹ ⬝ _,
-    apply apdt
-  end
-
-  definition homotopy_rec_idp_refl {A : Type} {P : A → Type} {f : Πa, P a}
-    (Q : Π{g}, f ~ g → Type) (H : Q homotopy.rfl) :
-    homotopy.rec_idp @Q H homotopy.rfl = H :=
-  !homotopy_rec_on_apd10
-
-  definition phomotopy_rec_on_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
-
   definition eq_tr_of_pathover_con_tr_eq_of_pathover {A : Type} {B : A → Type}
     {a₁ a₂ : A} (p : a₁ = a₂) {b₁ : B a₁} {b₂ : B a₂} (q : b₁ =[p] b₂) :
     eq_tr_of_pathover q ⬝ tr_eq_of_pathover q⁻¹ᵒ = idp :=
@@ -963,16 +938,16 @@ notation `Ω⇒`:(max+5) := ap1_phomotopy
 
 definition ap1_phomotopy_symm {A B : Type*} {f g : A →* B} (p : f ~* g) : (Ω⇒ p)⁻¹* = Ω⇒ (p⁻¹*) :=
 begin
-  induction p using phomotopy_rec_on_idp,
+  induction p using phomotopy_rec_idp,
   rewrite ap1_phomotopy_refl,
-  rewrite [+refl_symm],
+  xrewrite [+refl_symm],
   rewrite ap1_phomotopy_refl
 end
 
 definition ap1_phomotopy_trans {A B : Type*} {f g h : A →* B} (q : g ~* h) (p : f ~* g) : Ω⇒ (p ⬝* q) = Ω⇒ p ⬝* Ω⇒ 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,
   rewrite trans_refl,
   rewrite [+ap1_phomotopy_refl],
   rewrite trans_refl
diff --git a/pointed.hlean b/pointed.hlean
index bb50a18..554e2c3 100644
--- a/pointed.hlean
+++ b/pointed.hlean
@@ -33,10 +33,6 @@ namespace pointed
   --     apply equiv_eq_closed_right, exact !idp_con⁻¹ }
   -- end
 
-  definition pmap_eq_idp {X Y : Type*} (f : X →* Y) :
-    pmap_eq (λx, idpath (f x)) !idp_con⁻¹ = idpath f :=
-  ap (λx, eq_of_phomotopy (phomotopy.mk _ x)) !inv_inv ⬝ eq_of_phomotopy_refl f
-
   /- remove some duplicates: loop_ppmap_commute, loop_ppmap_pequiv, loop_ppmap_pequiv', pfunext -/
   definition pfunext (X Y : Type*) : ppmap X (Ω Y) ≃* Ω (ppmap X Y) :=
   (loop_ppmap_commute X Y)⁻¹ᵉ*
@@ -130,11 +126,11 @@ namespace pointed
     (to_fun : Π a : A, P a)
     (resp_pt : to_fun (Point A) = p)
   attribute ppi'.to_fun [coercion]
-  definition ppi_homotopy' {A : Type*} {P : A → Type} {x : P pt} (f g : ppi' A P x) : Type :=
+  definition phomotopy' {A : Type*} {P : A → Type} {x : P pt} (f g : ppi' A P x) : Type :=
   ppi' A (λa, f a = g a) (ppi'.resp_pt f ⬝ (ppi'.resp_pt g)⁻¹)
-  definition ppi_homotopy2' {A : Type*} {P : A → Type} {x : P pt} {f g : ppi' A P x}
-    (p q : ppi_homotopy' f g) : Type :=
-  ppi_homotopy' p q
+  definition phomotopy2' {A : Type*} {P : A → Type} {x : P pt} {f g : ppi' A P x}
+    (p q : phomotopy' f g) : Type :=
+  phomotopy' p q
 
   -- infix ` ~*2 `:50 := phomotopy2
 
@@ -145,7 +141,7 @@ namespace pointed
 
 /- Homotopy between a function and its eta expansion -/
 
-  definition pmap_eta {X Y : Type*} (f : X →* Y) : f ~* pmap.mk f (pmap.resp_pt f) :=
+  definition pmap_eta {X Y : Type*} (f : X →* Y) : f ~* pmap.mk f (respect_pt f) :=
   begin
     fapply phomotopy.mk,
     reflexivity,
@@ -219,15 +215,6 @@ namespace pointed
   definition loop_punit : Ω punit ≃* punit :=
   loop_pequiv_punit_of_is_set punit
 
-  definition phomotopy_of_is_contr_cod [constructor] {X Y : Type*} (f g : X →* Y) [is_contr Y] :
-    f ~* g :=
-  phomotopy.mk (λa, !eq_of_is_contr) !eq_of_is_contr
-
-  definition phomotopy_of_is_contr_dom [constructor] {X Y : Type*} (f g : X →* Y) [is_contr X] :
-    f ~* g :=
-  phomotopy.mk (λa, ap f !is_prop.elim ⬝ respect_pt f ⬝ (respect_pt g)⁻¹ ⬝ ap g !is_prop.elim)
-    begin rewrite [▸*, is_prop_elim_self, +ap_idp, idp_con, con_idp, inv_con_cancel_right] end
-
   definition add_point_over [unfold 3] {A : Type} (B : A → Type*) : A₊ → Type*
   | (some a) := B a
   | none     := plift punit
diff --git a/pointed_cubes.hlean b/pointed_cubes.hlean
index 592f8ea..79392cc 100644
--- a/pointed_cubes.hlean
+++ b/pointed_cubes.hlean
@@ -16,22 +16,22 @@ open eq pointed
 
 definition psquare_of_phtpy_top {A B C D : Type*}  {ftop : A →* B} {fbot : C →* D} {fleft : A →* C} {fright : B →* D} {ftop' : A →* B} (phtpy : ftop ~* ftop') (psq : psquare ftop' fbot fleft fright) : psquare ftop fbot fleft fright :=
 begin
-  induction phtpy using phomotopy_rec_on_idp, exact psq,
+  induction phtpy using phomotopy_rec_idp, exact psq,
 end
 
 definition psquare_of_phtpy_bot {A B C D : Type*} {ftop : A →* B} {fbot : C →* D} {fleft : A →* C} {fright : B →* D} {fbot' : C →* D} (phtpy : fbot ~* fbot') (psq : psquare ftop fbot' fleft fright) : psquare ftop fbot fleft fright :=
 begin
-  induction phtpy using phomotopy_rec_on_idp, exact psq,
+  induction phtpy using phomotopy_rec_idp, exact psq,
 end
 
 definition psquare_of_phtpy_left {A B C D : Type*} {ftop : A →* B} {fbot : C →* D} {fleft : A →* C} {fright : B →* D} {fleft' : A →* C} (phtpy : fleft ~* fleft') (psq : psquare ftop fbot fleft fright) : psquare ftop fbot fleft' fright :=
 begin
-  induction phtpy using phomotopy_rec_on_idp, exact psq,
+  induction phtpy using phomotopy_rec_idp, exact psq,
 end
 
 definition psquare_of_phtpy_right {A B C D : Type*} {ftop : A →* B} {fbot : C →* D} {fleft : A →* C} {fright : B →* D} {fright' : B →* D} (phtpy : fright ~* fright') (psq : psquare ftop fbot fleft fright) : psquare ftop fbot fleft fright' :=
 begin
-  induction phtpy using phomotopy_rec_on_idp, exact psq,
+  induction phtpy using phomotopy_rec_idp, exact psq,
 end
 
 definition psquare_of_pid_top_bot {A B : Type*} {fleft : A →* B} {fright : A →* B} (phtpy : fright ~* fleft) : psquare (pid A) (pid B) fleft fright :=
@@ -91,8 +91,8 @@ begin
   exact (pconst_pcompose fleft)⁻¹*,
 end
 
-definition phsquare_of_ppi_homotopy {A B : Type*} {f g h i : A →* B} {phtpy_top : f ~* g} {phtpy_bot : h ~* i} {phtpy_left : f ~* h} {phtpy_right : g ~* i} (H : phtpy_top ⬝* phtpy_right ~~* phtpy_left ⬝* phtpy_bot) : phsquare phtpy_top phtpy_bot phtpy_left phtpy_right :=
-  eq_of_ppi_homotopy H
+definition phsquare_of_phomotopy {A B : Type*} {f g h i : A →* B} {phtpy_top : f ~* g} {phtpy_bot : h ~* i} {phtpy_left : f ~* h} {phtpy_right : g ~* i} (H : phtpy_top ⬝* phtpy_right ~* phtpy_left ⬝* phtpy_bot) : phsquare phtpy_top phtpy_bot phtpy_left phtpy_right :=
+  eq_of_phomotopy H
 
 definition ptube_v {A B C D : Type*} {ftop ftop' : A →* B} (phtpy_top : ftop ~* ftop') {fbot fbot' : C →* D} (phtpy_bot : fbot ~* fbot') {fleft : A →* C} {fright : B →* D} (psq_back : psquare ftop fbot fleft fright) (psq_front : psquare ftop' fbot' fleft fright) : Type :=
 phsquare (pwhisker_left fright phtpy_top) (pwhisker_right fleft phtpy_bot) psq_back psq_front
@@ -127,7 +127,7 @@ structure p2homotopy {A B : Type*} {f g : A →* B} (H K : f ~* g) : Type :=
 
 definition ptube_v_phtpy_bot {A B C D : Type*}
   {ftop ftop' : A →* B} {phtpy_top : ftop ~* ftop'}
-  {fbot fbot' : C →* D} {phtpy_bot phtpy_bot' : fbot ~* fbot'} (ppi_htpy_bot : phtpy_bot ~~* phtpy_bot')
+  {fbot fbot' : C →* D} {phtpy_bot phtpy_bot' : fbot ~* fbot'} (ppi_htpy_bot : phtpy_bot ~* phtpy_bot')
   {fleft : A →* C} {fright : B →* D}
   {psq_back : psquare ftop fbot fleft fright}
   {psq_front : psquare ftop' fbot' fleft fright}
@@ -135,7 +135,7 @@ definition ptube_v_phtpy_bot {A B C D : Type*}
   : ptube_v phtpy_top phtpy_bot' psq_back psq_front
   :=
 begin
-  induction ppi_htpy_bot using ppi_homotopy_rec_on_idp,
+  induction ppi_htpy_bot using phomotopy_rec_idp,
   exact ptb,
 end
 
@@ -156,6 +156,6 @@ definition ptube_v_left_inv {A B C D : Type*} {ftop : A ≃* B} {fbot : C ≃* D
 begin
   refine ptube_v_phtpy_bot _ _,
   exact pleft_inv fbot,
-  exact ppi_homotopy.rfl,
-  fapply phsquare_of_ppi_homotopy, repeat exact sorry,
+  exact phomotopy.rfl,
+  fapply phsquare_of_phomotopy, repeat exact sorry,
 end
diff --git a/pointed_pi.hlean b/pointed_pi.hlean
index 4e843b8..05fe709 100644
--- a/pointed_pi.hlean
+++ b/pointed_pi.hlean
@@ -283,7 +283,7 @@ namespace pointed
     (h₃ : squareover B₂ (square_of_eq (to_homotopy_pt h₁)⁻¹) p₁ p₂ (h₂ b₁) idpo) :
     psigma_gen_functor f₁ g₁ p₁ ~* psigma_gen_functor f₂ g₂ p₂ :=
   begin
-    induction h₁ using phomotopy_rec_on_idp,
+    induction h₁ using phomotopy_rec_idp,
     fapply phomotopy.mk,
     { intro x, induction x with a b, exact ap (dpair (f₁ a)) (eq_of_pathover_idp (h₂ b)) },
     { induction f₁ with f f₀, induction A₂ with A₂ a₂₀, esimp at * ⊢,
@@ -330,260 +330,49 @@ namespace pointed
     ppi (λx, f x = g x) (respect_pt f ⬝ (respect_pt g)⁻¹) :=
   h
 
-  abbreviation pppi_resp_pt [unfold 3] := @pppi.resp_pt
-
-  definition ppi_homotopy {A : Type*} {P : A → Type} {x : P pt} (f g : ppi P x) : Type :=
-  ppi (λa, f a = g a) (ppi.resp_pt f ⬝ (ppi.resp_pt g)⁻¹)
+  definition phomotopy {A : Type*} {P : A → Type} {x : P pt} (f g : ppi P x) : Type :=
+  ppi (λa, f a = g a) (respect_pt f ⬝ (respect_pt g)⁻¹)
 
   variables {A : Type*} {P Q R : A → Type*} {f g h : Π*a, P a}
                         {B C D : A → Type} {b₀ : B pt} {c₀ : C pt} {d₀ : D pt}
                         {k k' l m : ppi B b₀}
 
-  infix ` ~~* `:50 := ppi_homotopy
-
-  definition ppi_homotopy.mk [constructor] [reducible] (h : k ~ l)
-    (p : h pt ⬝ ppi.resp_pt l = ppi.resp_pt k) : k ~~* l :=
-  ppi.mk h (eq_con_inv_of_con_eq p)
-  definition ppi_to_homotopy [coercion] [unfold 6] [reducible] (p : k ~~* l) : Πa, k a = l a := p
-  definition ppi_to_homotopy_pt [unfold 6] [reducible] (p : k ~~* l) :
-    p pt ⬝ ppi.resp_pt l = ppi.resp_pt k :=
-  con_eq_of_eq_con_inv (ppi.resp_pt p)
-
-  variable (k)
-  protected definition ppi_homotopy.refl [constructor] : k ~~* k :=
-  ppi_homotopy.mk homotopy.rfl !idp_con
-  variable {k}
-  protected definition ppi_homotopy.rfl [constructor] [refl] : k ~~* k :=
-  ppi_homotopy.refl k
-
-  protected definition ppi_homotopy.symm [constructor] [symm] (p : k ~~* l) : l ~~* k :=
-  ppi_homotopy.mk p⁻¹ʰᵗʸ (inv_con_eq_of_eq_con (ppi_to_homotopy_pt p)⁻¹)
-
-  protected definition ppi_homotopy.trans [constructor] [trans] (p : k ~~* l) (q : l ~~* m) :
-    k ~~* m :=
-  ppi_homotopy.mk (λa, p a ⬝ q a) (!con.assoc ⬝ whisker_left (p pt) (ppi_to_homotopy_pt q) ⬝ ppi_to_homotopy_pt p)
-
-  infix ` ⬝*' `:75 := ppi_homotopy.trans
-  postfix `⁻¹*'`:(max+1) := ppi_homotopy.symm
-
-  definition ppi_trans2 {p p' : k ~~* l} {q q' : l ~~* m}
-    (r : p = p') (s : q = q') : p ⬝*' q = p' ⬝*' q' :=
-  ap011 ppi_homotopy.trans r s
-
-  definition ppi_symm2 {p p' : k ~~* l} (r : p = p') : p⁻¹*' = p'⁻¹*' :=
-  ap ppi_homotopy.symm r
-
-  infixl ` ◾**' `:80 := ppi_trans2
-  postfix `⁻²**'`:(max+1) := ppi_symm2
-
   definition pppi_equiv_pmap [constructor] (A B : Type*) : (Π*(a : A), B) ≃ (A →* B) :=
-  begin
-    fapply equiv.MK,
-    { intro k, induction k with k p, exact pmap.mk k p },
-    { intro k, induction k with k p, exact pppi.mk k p },
-    { intro k, induction k with k p, reflexivity },
-    { intro k, induction k with k p, reflexivity }
-  end
+  by reflexivity
 
   definition pppi_pequiv_ppmap [constructor] (A B : Type*) : (Π*(a : A), B) ≃* ppmap A B :=
-  pequiv_of_equiv (pppi_equiv_pmap A B) idp
+  by reflexivity
 
-  protected definition ppi.sigma_char [constructor] {A : Type*} (B : A → Type) (b₀ : B pt) :
-    ppi B b₀ ≃ Σ(k : Πa, B a), k pt = b₀ :=
+  definition apd10_to_fun_eq_of_phomotopy (h : f ~* g)
+    : apd10 (ap (λ k, pppi.to_fun k) (eq_of_phomotopy h)) = h :=
   begin
-    fapply equiv.MK: intro x,
-    { constructor, exact ppi.resp_pt x },
-    { induction x, constructor, assumption },
-    { induction x, reflexivity },
-    { induction x, reflexivity }
+    induction h using phomotopy_rec_idp,
+    xrewrite [eq_of_phomotopy_refl f]
   end
 
-  -- definition pppi.sigma_char [constructor] {A : Type*} (B : A → Type*)
-  --   : (Π*(a : A), B a) ≃ Σ(k : (Π (a : A), B a)), k pt = pt :=
-  -- ppi.sigma_char
-
-  definition ppi_homotopy_of_eq (p : k = l) : k ~~* l :=
-  ppi_homotopy.mk (ap010 ppi.to_fun p) begin induction p, refine !idp_con end
-
-  variables (k l)
-
-  definition ppi_homotopy.rec' [recursor] (B : k ~~* l → Type)
-    (H : Π(h : k ~ l) (p : h pt ⬝ ppi.resp_pt l = ppi.resp_pt k), B (ppi_homotopy.mk h p))
-    (h : k ~~* l) : B h :=
-  begin
-    induction h with h 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 ppi_homotopy.sigma_char [constructor]
-    : (k ~~* l) ≃ Σ(p : k ~ l), p pt ⬝ ppi.resp_pt l = ppi.resp_pt k :=
-  begin
-    fapply equiv.MK : intros h,
-    { exact ⟨h , ppi_to_homotopy_pt h⟩ },
-    { cases h with h p, exact ppi_homotopy.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 ppi_homotopy.rec' with h p,
-      exact ap (ppi_homotopy.mk h) (to_right_inv !eq_con_inv_equiv_con_eq p) }
-  end
-
-  -- the same as pmap_eq_equiv
-  definition ppi_eq_equiv_internal : (k = l) ≃ (k ~~* l) :=
-    calc (k = l) ≃ ppi.sigma_char B b₀ k = ppi.sigma_char B b₀ l
-                   : eq_equiv_fn_eq (ppi.sigma_char B b₀) k l
-            ...  ≃ Σ(p : k = l),
-                     pathover (λh, h pt = b₀) (ppi.resp_pt k) p (ppi.resp_pt l)
-                   : sigma_eq_equiv _ _
-            ...  ≃ Σ(p : k = l),
-                     ppi.resp_pt k = ap (λh, h pt) p ⬝ ppi.resp_pt l
-                   : sigma_equiv_sigma_right
-                       (λp, eq_pathover_equiv_Fl p (ppi.resp_pt k) (ppi.resp_pt l))
-            ...  ≃ Σ(p : k = l),
-                     ppi.resp_pt k = apd10 p pt ⬝ ppi.resp_pt l
-                   : sigma_equiv_sigma_right
-                       (λp, equiv_eq_closed_right _ (whisker_right _ (ap_eq_apd10 p _)))
-            ...  ≃ Σ(p : k ~ l), ppi.resp_pt k = p pt ⬝ ppi.resp_pt l
-                   : sigma_equiv_sigma_left' eq_equiv_homotopy
-            ...  ≃ Σ(p : k ~ l), p pt ⬝ ppi.resp_pt l = ppi.resp_pt k
-                   : sigma_equiv_sigma_right (λp, eq_equiv_eq_symm _ _)
-            ...  ≃ (k ~~* l) : ppi_homotopy.sigma_char k l
-
-  definition ppi_eq_equiv_internal_idp :
-    ppi_eq_equiv_internal k k idp = ppi_homotopy.refl k :=
-  begin
-    apply ap (ppi_homotopy.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 ppi_homotopy_of_eq },
-    { intro p, induction p, exact ppi_eq_equiv_internal_idp k }
-  end
-
-  variables {k l}
-
-  -- the same as pmap_eq
-  definition ppi_eq (h : k ~~* l) : k = l :=
-  (ppi_eq_equiv k l)⁻¹ᵉ h
-
-  definition eq_of_ppi_homotopy (h : k ~~* l) : k = l := ppi_eq h
-
-  definition ppi_homotopy_of_eq_of_ppi_homotopy (h : k ~~* l) :
-    ppi_homotopy_of_eq (eq_of_ppi_homotopy h) = h :=
-  proof to_right_inv (ppi_eq_equiv k l) h qed
-
-  variable (k)
-
-  definition eq_ppi_homotopy_refl_ppi_homotopy_of_eq_refl :
-    ppi_homotopy.refl k = ppi_homotopy_of_eq (refl k) :=
-  begin
-    reflexivity
-  end
-
-  definition ppi_homotopy_of_eq_refl : ppi_homotopy.refl k = ppi_homotopy_of_eq (refl k) :=
-  begin
-    reflexivity,
-  end
-
-  definition ppi_eq_refl : ppi_eq (ppi_homotopy.refl k) = refl k :=
-  to_inv_eq_of_eq !ppi_eq_equiv idp
-
-  variable {k}
-  definition ppi_homotopy_rec_on_eq [recursor]
-    {Q : (k ~~* k') → Type} (p : k ~~* k') (H : Π(q : k = k'), Q (ppi_homotopy_of_eq q)) : Q p :=
-  ppi_homotopy_of_eq_of_ppi_homotopy p ▸ H (eq_of_ppi_homotopy p)
-
-  definition ppi_homotopy_rec_on_idp [recursor]
-    {Q : Π {k' : ppi B b₀}, (k ~~* k') → Type} {k' : ppi B b₀} (H : k ~~* k')
-    (q : Q (ppi_homotopy.refl k)) : Q H :=
-  begin
-    induction H using ppi_homotopy_rec_on_eq with t,
-    induction t, exact eq_ppi_homotopy_refl_ppi_homotopy_of_eq_refl k ▸ q,
-  end
-
-  attribute ppi_homotopy.rec' [recursor]
-
-  definition ppi_homotopy_rec_on_eq_ppi_homotopy_of_eq
-    {Q : (k ~~* k') → Type} (H : Π(q : k = k'), Q (ppi_homotopy_of_eq q))
-    (p : k = k') : ppi_homotopy_rec_on_eq (ppi_homotopy_of_eq p) H = H p :=
-  begin
-    refine ap (λp, p ▸ _) !adj ⬝ _,
-    refine !tr_compose⁻¹ ⬝ _,
-    apply apdt
-  end
-
-  definition ppi_homotopy_rec_on_idp_refl {Q : Π {k' : ppi B b₀}, (k ~~* k') → Type}
-    (q : Q (ppi_homotopy.refl k)) : ppi_homotopy_rec_on_idp ppi_homotopy.rfl q = q :=
-  ppi_homotopy_rec_on_eq_ppi_homotopy_of_eq _ idp
-
-  definition ppi_homotopy_rec_idp'
-    (Q : Π ⦃k' : ppi B b₀⦄, (k ~~* k') → (k = k') → Type)
-    (q : Q (ppi_homotopy.refl k) idp) ⦃k' : ppi B b₀⦄ (H : k ~~* k') : Q H (ppi_eq H) :=
-  begin
-    induction H using ppi_homotopy_rec_on_idp,
-    exact transport (Q ppi_homotopy.rfl) !ppi_eq_refl⁻¹ q
-  end
-
-  definition ppi_homotopy_rec_idp'_refl
-    (Q : Π ⦃k' : ppi B b₀⦄, (k ~~* k') → (k = k') → Type)
-    (q : Q (ppi_homotopy.refl k) idp) :
-    ppi_homotopy_rec_idp' Q q ppi_homotopy.rfl = transport (Q ppi_homotopy.rfl) !ppi_eq_refl⁻¹ q :=
-  !ppi_homotopy_rec_on_idp_refl
-
-  definition ppi_trans_refl (p : k ~~* l) : p ⬝*' ppi_homotopy.refl l = p :=
-  begin
-    unfold ppi_homotopy.trans,
-    induction A with A a₀,
-    induction k with k k₀, induction l with l l₀, induction p with p p₀, esimp at p, induction l₀, esimp at p₀, induction p₀, reflexivity,
-  end
-
-  definition ppi_refl_trans (p : k ~~* l) :  ppi_homotopy.refl k ⬝*' p = p :=
-  begin
-    induction p using ppi_homotopy_rec_on_idp,
-    apply ppi_trans_refl
-  end
-
-  definition ppi_homotopy_of_eq_con {A : Type*} {B : A → Type*} {f g h : Π* (a : A), B a} (p : f = g) (q : g = h) :
-    ppi_homotopy_of_eq (p ⬝ q) = ppi_homotopy_of_eq p ⬝*' ppi_homotopy_of_eq q :=
-  begin induction q, induction p,
-    fapply eq_of_ppi_homotopy,
-    rewrite [!idp_con],
-    refine transport (λ x, x ~~* x ⬝*' x) !ppi_homotopy_of_eq_refl _,
-    fapply ppi_homotopy_of_eq,
-    refine (ppi_trans_refl (ppi_homotopy.refl f))⁻¹ᵖ
-  end
-
-  definition apd10_to_fun_ppi_eq (h : f ~~* g)
-    : apd10 (ap (λ k, pppi.to_fun k) (ppi_eq h)) = ppi_to_homotopy h :=
-  begin
-    induction h using ppi_homotopy_rec_on_idp, rewrite ppi_eq_refl
-  end
-
---  definition ppi_homotopy_of_eq_of_ppi_homotopy
+--  definition phomotopy_of_eq_of_phomotopy
 
   definition phomotopy_mk_ppi [constructor] {A : Type*} {B : Type*} {C : B → Type*}
-    {f g : A →* (Π*b, C b)} (p : Πa, f a ~~* g a)
-    (q : p pt ⬝*' ppi_homotopy_of_eq (respect_pt g) = ppi_homotopy_of_eq (respect_pt f)) : f ~* g :=
+    {f g : A →* (Π*b, C b)} (p : Πa, f a ~* g a)
+    (q : p pt ⬝* phomotopy_of_eq (respect_pt g) = phomotopy_of_eq (respect_pt f)) : f ~* g :=
   begin
-    apply phomotopy.mk (λa, eq_of_ppi_homotopy (p a)),
+    apply phomotopy.mk (λa, eq_of_phomotopy (p a)),
     apply eq_of_fn_eq_fn !ppi_eq_equiv,
-    refine !ppi_homotopy_of_eq_con ⬝ _, esimp,
-    refine ap (λx, x ⬝*' _) !ppi_homotopy_of_eq_of_ppi_homotopy ⬝ q
+    refine !phomotopy_of_eq_con ⬝ _, esimp,
+    refine ap (λx, x ⬝* _) !phomotopy_of_eq_of_phomotopy ⬝ q
   end
 
---   definition ppi_homotopy_mk_ppmap [constructor]
+--   definition phomotopy_mk_ppmap [constructor]
 --     {A : Type*} {X : A → Type*} {Y : Π (a : A), X a → Type*}
 --     {f g : Π* (a : A), Π*(x : (X a)), (Y a x)}
---     (p : Πa, f a ~~* g a)
---     (q : p pt ⬝*' ppi_homotopy_of_eq (ppi_resp_pt g) = ppi_homotopy_of_eq (ppi_resp_pt f))
---     : f ~~* g :=
+--     (p : Πa, f a ~* g a)
+--     (q : p pt ⬝* phomotopy_of_eq (ppi_resp_pt g) = phomotopy_of_eq (ppi_resp_pt f))
+--     : f ~* g :=
 --   begin
---     apply ppi_homotopy.mk (λa, eq_of_ppi_homotopy (p a)),
+--     apply phomotopy.mk (λa, eq_of_phomotopy (p a)),
 --     apply eq_of_fn_eq_fn (ppi_eq_equiv _ _),
---     refine !ppi_homotopy_of_eq_con ⬝ _,
--- --    refine !ppi_homotopy_of_eq_of_ppi_homotopy ◾** idp ⬝ q,
+--     refine !phomotopy_of_eq_con ⬝ _,
+-- --    refine !phomotopy_of_eq_of_phomotopy ◾** idp ⬝ q,
 --   end
 
   variable {k}
@@ -597,54 +386,54 @@ namespace pointed
   end
 
   variables {k l}
-  -- definition eq_of_ppi_homotopy (h : k ~~* l) : k = l :=
+  -- definition eq_of_phomotopy (h : k ~* l) : k = l :=
   -- (ppi_eq_equiv k l)⁻¹ᵉ h
 
   definition ppi_functor_right [constructor] {A : Type*} {B B' : A → Type}
     {b : B pt} {b' : B' pt} (f : Πa, B a → B' a) (p : f pt b = b') (g : ppi B b)
     : ppi B' b' :=
-  ppi.mk (λa, f a (g a)) (ap (f pt) (ppi.resp_pt g) ⬝ p)
+  ppi.mk (λa, f a (g a)) (ap (f pt) (respect_pt g) ⬝ p)
 
   definition ppi_functor_right_compose [constructor] {A : Type*} {B₁ B₂ B₃ : A → Type}
     {b₁ : B₁ pt} {b₂ : B₂ pt} {b₃ : B₃ pt} (f₂ : Πa, B₂ a → B₃ a) (p₂ : f₂ pt b₂ = b₃)
     (f₁ : Πa, B₁ a → B₂ a) (p₁ : f₁ pt b₁ = b₂)
-    (g : ppi B₁ b₁) : ppi_functor_right (λa, f₂ a ∘ f₁ a) (ap (f₂ pt) p₁ ⬝ p₂) g ~~*
+    (g : ppi B₁ b₁) : ppi_functor_right (λa, f₂ a ∘ f₁ a) (ap (f₂ pt) p₁ ⬝ p₂) g ~*
     ppi_functor_right f₂ p₂ (ppi_functor_right f₁ p₁ g) :=
   begin
-    fapply ppi_homotopy.mk,
+    fapply phomotopy.mk,
     { reflexivity },
     { induction p₁, induction p₂, exact !idp_con ⬝ !ap_compose⁻¹ }
   end
 
   definition ppi_functor_right_id [constructor] {A : Type*} {B : A → Type}
-    {b : B pt} (g : ppi B b) : ppi_functor_right (λa, id) idp g ~~* g :=
+    {b : B pt} (g : ppi B b) : ppi_functor_right (λa, id) idp g ~* g :=
   begin
-    fapply ppi_homotopy.mk,
+    fapply phomotopy.mk,
     { reflexivity },
     { reflexivity }
   end
 
-  definition ppi_functor_right_ppi_homotopy [constructor] {g g' : Π(a : A), B a → C a}
+  definition ppi_functor_right_phomotopy [constructor] {g g' : Π(a : A), B a → C a}
     {g₀ : g pt b₀ = c₀} {g₀' : g' pt b₀ = c₀} {f f' : ppi B b₀}
-    (p : g ~2 g') (q : f ~~* f') (r : p pt b₀ ⬝ g₀' = g₀) :
-    ppi_functor_right g g₀ f ~~* ppi_functor_right g' g₀' f' :=
-  ppi_homotopy.mk (λa, p a (f a) ⬝ ap (g' a) (q a))
+    (p : g ~2 g') (q : f ~* f') (r : p pt b₀ ⬝ g₀' = g₀) :
+    ppi_functor_right g g₀ f ~* ppi_functor_right g' g₀' f' :=
+  phomotopy.mk (λa, p a (f a) ⬝ ap (g' a) (q a))
     abstract begin
-      induction q using ppi_homotopy_rec_on_idp,
+      induction q using phomotopy_rec_idp,
       induction r, revert g p, refine rec_idp_of_equiv _ homotopy2.rfl _ _ _,
       { intro h h', exact !eq_equiv_eq_symm ⬝e !eq_equiv_homotopy2 },
       { reflexivity },
       induction g₀', induction f with f f₀, induction f₀, reflexivity
     end end
 
-  definition ppi_functor_right_ppi_homotopy_refl [constructor] (g : Π(a : A), B a → C a)
+  definition ppi_functor_right_phomotopy_refl [constructor] (g : Π(a : A), B a → C a)
     (g₀ : g pt b₀ = c₀) (f : ppi B b₀) :
-    ppi_functor_right_ppi_homotopy (homotopy2.refl g) (ppi_homotopy.refl f) !idp_con =
-    ppi_homotopy.refl (ppi_functor_right g g₀ f) :=
+    ppi_functor_right_phomotopy (homotopy2.refl g) (phomotopy.refl f) !idp_con =
+    phomotopy.refl (ppi_functor_right g g₀ f) :=
   begin
     induction g₀,
-    apply ap (ppi_homotopy.mk homotopy.rfl),
-    refine !ppi_homotopy_rec_on_idp_refl ⬝ _,
+    apply ap (phomotopy.mk homotopy.rfl),
+    refine !phomotopy_rec_idp_refl ⬝ _,
     esimp,
     refine !rec_idp_of_equiv_idp ⬝ _,
     induction f with f f₀, induction f₀, reflexivity
@@ -655,16 +444,16 @@ namespace pointed
     ppi B b ≃ ppi B' b' :=
   equiv.MK (ppi_functor_right f p) (ppi_functor_right (λa, (f a)⁻¹ᵉ) (inv_eq_of_eq p⁻¹))
     abstract begin
-      intro g, apply ppi_eq,
-      refine !ppi_functor_right_compose⁻¹*' ⬝*' _,
-      refine ppi_functor_right_ppi_homotopy (λa, to_right_inv (f a)) (ppi_homotopy.refl g) _ ⬝*'
+      intro g, apply eq_of_phomotopy,
+      refine !ppi_functor_right_compose⁻¹* ⬝* _,
+      refine ppi_functor_right_phomotopy (λa, to_right_inv (f a)) (phomotopy.refl g) _ ⬝*
             !ppi_functor_right_id, induction p, exact adj (f pt) b ⬝ ap02 (f pt) !idp_con⁻¹
 
     end end
     abstract begin
-      intro g, apply ppi_eq,
-      refine !ppi_functor_right_compose⁻¹*' ⬝*' _,
-      refine ppi_functor_right_ppi_homotopy (λa, to_left_inv (f a)) (ppi_homotopy.refl g) _ ⬝*'
+      intro g, apply eq_of_phomotopy,
+      refine !ppi_functor_right_compose⁻¹* ⬝* _,
+      refine ppi_functor_right_phomotopy (λa, to_left_inv (f a)) (phomotopy.refl g) _ ⬝*
             !ppi_functor_right_id, induction p, exact (!idp_con ⬝ !idp_con)⁻¹,
     end end
 
@@ -677,75 +466,76 @@ namespace pointed
   ppi_functor_right g (respect_pt (g pt)) f
 
   definition pmap_compose_ppi_ppi_const [constructor] (g : Π(a : A), ppmap (P a) (Q a)) :
-    pmap_compose_ppi g (ppi_const P) ~~* ppi_const Q :=
-  proof ppi_homotopy.mk (λa, respect_pt (g a)) !idp_con⁻¹ qed
+    pmap_compose_ppi g (ppi_const P) ~* ppi_const Q :=
+  proof phomotopy.mk (λa, respect_pt (g a)) !idp_con⁻¹ qed
 
   definition pmap_compose_ppi_pconst [constructor] (f : Π*(a : A), P a) :
-    pmap_compose_ppi (λa, pconst (P a) (Q a)) f ~~* ppi_const Q :=
-  ppi_homotopy.mk homotopy.rfl !ap_constant⁻¹
+    pmap_compose_ppi (λa, pconst (P a) (Q a)) f ~* ppi_const Q :=
+  phomotopy.mk homotopy.rfl !ap_constant⁻¹
 
   definition pmap_compose_ppi2 [constructor] {g g' : Π(a : A), ppmap (P a) (Q a)}
-    {f f' : Π*(a : A), P a} (p : Πa, g a ~* g' a) (q : f ~~* f') :
-    pmap_compose_ppi g f ~~* pmap_compose_ppi g' f' :=
-  ppi_functor_right_ppi_homotopy p q (to_homotopy_pt (p pt))
+    {f f' : Π*(a : A), P a} (p : Πa, g a ~* g' a) (q : f ~* f') :
+    pmap_compose_ppi g f ~* pmap_compose_ppi g' f' :=
+  ppi_functor_right_phomotopy p q (to_homotopy_pt (p pt))
 
   definition pmap_compose_ppi2_refl [constructor] (g : Π(a : A), P a →* Q a) (f : Π*(a : A), P a) :
-    pmap_compose_ppi2 (λa, phomotopy.refl (g a)) (ppi_homotopy.refl f) = ppi_homotopy.rfl :=
+    pmap_compose_ppi2 (λa, phomotopy.refl (g a)) (phomotopy.refl f) = phomotopy.rfl :=
   begin
-    refine _ ⬝ ppi_functor_right_ppi_homotopy_refl g (respect_pt (g pt)) f,
-    exact ap (ppi_functor_right_ppi_homotopy _ _) (to_right_inv !eq_con_inv_equiv_con_eq _)
+    refine _ ⬝ ppi_functor_right_phomotopy_refl g (respect_pt (g pt)) f,
+    exact ap (ppi_functor_right_phomotopy _ _) (to_right_inv !eq_con_inv_equiv_con_eq _)
   end
 
   definition pmap_compose_ppi_phomotopy_left [constructor] {g g' : Π(a : A), ppmap (P a) (Q a)}
-    (f : Π*(a : A), P a) (p : Πa, g a ~* g' a) : pmap_compose_ppi g f ~~* pmap_compose_ppi g' f :=
-  pmap_compose_ppi2 p ppi_homotopy.rfl
+    (f : Π*(a : A), P a) (p : Πa, g a ~* g' a) : pmap_compose_ppi g f ~* pmap_compose_ppi g' f :=
+  pmap_compose_ppi2 p phomotopy.rfl
 
   definition pmap_compose_ppi_phomotopy_right [constructor] (g : Π(a : A), ppmap (P a) (Q a))
-    {f f' : Π*(a : A), P a} (p : f ~~* f') : pmap_compose_ppi g f ~~* pmap_compose_ppi g f' :=
+    {f f' : Π*(a : A), P a} (p : f ~* f') : pmap_compose_ppi g f ~* pmap_compose_ppi g f' :=
   pmap_compose_ppi2 (λa, phomotopy.rfl) p
 
   definition pmap_compose_ppi_pid_left [constructor]
-    (f : Π*(a : A), P a) : pmap_compose_ppi (λa, pid (P a)) f ~~* f :=
-  ppi_homotopy.mk homotopy.rfl idp
+    (f : Π*(a : A), P a) : pmap_compose_ppi (λa, pid (P a)) f ~* f :=
+  phomotopy.mk homotopy.rfl idp
 
   definition pmap_compose_ppi_pcompose [constructor] (h : Π(a : A), ppmap (Q a) (R a))
     (g : Π(a : A), ppmap (P a) (Q a)) :
-    pmap_compose_ppi (λa, h a ∘* g a) f ~~* pmap_compose_ppi h (pmap_compose_ppi g f)  :=
-  ppi_homotopy.mk homotopy.rfl
+    pmap_compose_ppi (λa, h a ∘* g a) f ~* pmap_compose_ppi h (pmap_compose_ppi g f)  :=
+  phomotopy.mk homotopy.rfl
     abstract !idp_con ⬝ whisker_right _ (!ap_con ⬝ whisker_right _ !ap_compose'⁻¹) ⬝ !con.assoc end
 
   definition ppi_assoc [constructor] (h : Π (a : A), Q a →* R a) (g : Π (a : A), P a →* Q a)
     (f : Π*a, P a) :
-    pmap_compose_ppi (λa, h a ∘* g a) f ~~* pmap_compose_ppi h (pmap_compose_ppi g f) :=
+    pmap_compose_ppi (λa, h a ∘* g a) f ~* pmap_compose_ppi h (pmap_compose_ppi g f) :=
   begin
-    fapply ppi_homotopy.mk,
+    fapply phomotopy.mk,
     { intro a, reflexivity },
     exact !idp_con ⬝ whisker_right _ (!ap_con ⬝ whisker_right _ !ap_compose⁻¹) ⬝ !con.assoc
   end
 
-  definition pmap_compose_ppi_eq (g : Πa, P a →* Q a) {f f' : Π*a, P a} (p : f ~~* f') :
-    ap (pmap_compose_ppi g) (ppi_eq p) = ppi_eq (pmap_compose_ppi_phomotopy_right g p) :=
+  definition pmap_compose_ppi_eq_of_phomotopy (g : Πa, P a →* Q a) {f f' : Π*a, P a} (p : f ~* f') :
+    ap (pmap_compose_ppi g) (eq_of_phomotopy p) =
+    eq_of_phomotopy (pmap_compose_ppi_phomotopy_right g p) :=
   begin
-    induction p using ppi_homotopy_rec_on_idp,
-    refine ap02 _ !ppi_eq_refl ⬝ !ppi_eq_refl⁻¹ ⬝ ap ppi_eq _,
+    induction p using phomotopy_rec_idp,
+    refine ap02 _ !eq_of_phomotopy_refl ⬝ !eq_of_phomotopy_refl⁻¹ ⬝ ap eq_of_phomotopy _,
     exact !pmap_compose_ppi2_refl⁻¹
   end
 
   definition ppi_assoc_ppi_const_right (g : Πa, Q a →* R a) (f : Πa, P a →* Q a) :
-    ppi_assoc g f (ppi_const P) ⬝*'
-    (pmap_compose_ppi_phomotopy_right _ (pmap_compose_ppi_ppi_const f) ⬝*'
+    ppi_assoc g f (ppi_const P) ⬝*
+    (pmap_compose_ppi_phomotopy_right _ (pmap_compose_ppi_ppi_const f) ⬝*
     pmap_compose_ppi_ppi_const g) = pmap_compose_ppi_ppi_const (λa, g a ∘* f a) :=
   begin
     revert R g, refine fiberwise_pointed_map_rec _ _,
     revert Q f, refine fiberwise_pointed_map_rec _ _,
     intro Q f R g,
-    refine ap (λx, _ ⬝*' (x ⬝*' _)) !pmap_compose_ppi2_refl ⬝ _,
+    refine ap (λx, _ ⬝* (x ⬝* _)) !pmap_compose_ppi2_refl ⬝ _,
     reflexivity
   end
 
   definition pppi_compose_left [constructor] (g : Π(a : A), ppmap (P a) (Q a)) :
     (Π*(a : A), P a) →* Π*(a : A), Q a :=
-  pmap.mk (pmap_compose_ppi g) (ppi_eq (pmap_compose_ppi_ppi_const g))
+  pmap.mk (pmap_compose_ppi g) (eq_of_phomotopy (pmap_compose_ppi_ppi_const g))
 
   -- pppi_compose_left is a functor in the following sense
   definition pppi_compose_left_pcompose (g : Π (a : A), Q a →* R a) (f : Π (a : A), P a →* Q a)
@@ -753,9 +543,9 @@ namespace pointed
   begin
     fapply phomotopy_mk_ppi,
     { exact ppi_assoc g f },
-    { refine idp ◾**' (!ppi_homotopy_of_eq_con ⬝
-        (ap ppi_homotopy_of_eq !pmap_compose_ppi_eq ⬝ !ppi_homotopy_of_eq_of_ppi_homotopy) ◾**'
-        !ppi_homotopy_of_eq_of_ppi_homotopy) ⬝ _ ⬝ !ppi_homotopy_of_eq_of_ppi_homotopy⁻¹,
+    { refine idp ◾** (!phomotopy_of_eq_con ⬝
+        (ap phomotopy_of_eq !pmap_compose_ppi_eq_of_phomotopy ⬝ !phomotopy_of_eq_of_phomotopy) ◾**
+        !phomotopy_of_eq_of_phomotopy) ⬝ _ ⬝ !phomotopy_of_eq_of_phomotopy⁻¹,
       apply ppi_assoc_ppi_const_right },
   end
 
@@ -787,13 +577,13 @@ namespace pointed
   begin
     apply pequiv_of_pmap (pppi_compose_left g),
     apply adjointify _ (pppi_compose_left (λa, (g a)⁻¹ᵉ*)),
-    { intro f, apply ppi_eq,
-      refine !pmap_compose_ppi_pcompose⁻¹*' ⬝*' _,
-      refine pmap_compose_ppi_phomotopy_left _ (λa, !pright_inv) ⬝*' _,
+    { intro f, apply eq_of_phomotopy,
+      refine !pmap_compose_ppi_pcompose⁻¹* ⬝* _,
+      refine pmap_compose_ppi_phomotopy_left _ (λa, !pright_inv) ⬝* _,
       apply pmap_compose_ppi_pid_left },
-    { intro f, apply ppi_eq,
-      refine !pmap_compose_ppi_pcompose⁻¹*' ⬝*' _,
-      refine pmap_compose_ppi_phomotopy_left _ (λa, !pleft_inv) ⬝*' _,
+    { intro f, apply eq_of_phomotopy,
+      refine !pmap_compose_ppi_pcompose⁻¹* ⬝* _,
+      refine pmap_compose_ppi_phomotopy_left _ (λa, !pleft_inv) ⬝* _,
       apply pmap_compose_ppi_pid_left }
   end
 
@@ -837,7 +627,7 @@ namespace pointed
       fapply sigma_eq2,
       { refine !sigma_eq_pr1 ⬝ _ ⬝ !ap_sigma_pr1⁻¹,
         apply eq_of_fn_eq_fn eq_equiv_homotopy,
-        refine !apd10_eq_of_homotopy ⬝ _ ⬝ !apd10_to_fun_ppi_eq⁻¹,
+        refine !apd10_eq_of_homotopy ⬝ _ ⬝ !apd10_to_fun_eq_of_phomotopy⁻¹,
         apply eq_of_homotopy, intro a, reflexivity },
       { exact sorry } }
   end
@@ -869,7 +659,7 @@ namespace pointed
   definition ppi_psigma.{u v w} {A : pType.{u}} {B : A → pType.{v}} (C : Πa, B a → Type.{w})
     (c : Πa, C a pt) : (Π*(a : A), (psigma_gen (C a) (c a))) ≃*
     psigma_gen (λ(f : Π*(a : A), B a), ppi (λa, C a (f a))
-                 (transport (C pt) (pppi.resp_pt f)⁻¹ (c pt))) (ppi_const _) :=
+                 (transport (C pt) (respect_pt f)⁻¹ (c pt))) (ppi_const _) :=
   proof
   calc (Π*(a : A), psigma_gen (C a) (c a))
           ≃* @psigma_gen (Πᵘ*a, psigma_gen (C a) (c a)) (λf, f pt = pt) idp : pppi.sigma_char
@@ -881,7 +671,7 @@ namespace pointed
                          (λv, Σ(g : Πa, C a (v.1 a)), g pt =[v.2] c pt) ⟨c, idpo⟩ :
              by apply psigma_gen_swap
       ... ≃* psigma_gen (λ(f : Π*(a : A), B a), ppi (λa, C a (f a))
-                                                        (transport (C pt) (pppi.resp_pt f)⁻¹ (c pt)))
+                                                        (transport (C pt) (respect_pt f)⁻¹ (c pt)))
                         (ppi_const _) :
              by exact (psigma_gen_pequiv_psigma_gen (pppi.sigma_char B)
                 (λf, !ppi.sigma_char ⬝e sigma_equiv_sigma_right (λg, !pathover_equiv_eq_tr⁻¹ᵉ))
@@ -901,25 +691,26 @@ namespace pointed
   calc
     pfiber (pppi_compose_left f) ≃*
              psigma_gen (λ(g : Π*(a : A), B a), pmap_compose_ppi f g = ppi_const C)
-               proof (ppi_eq (pmap_compose_ppi_ppi_const f)) qed : by exact !pfiber.sigma_char'
-      ... ≃* psigma_gen (λ(g : Π*(a : A), B a), pmap_compose_ppi f g ~~* ppi_const C)
+               proof (eq_of_phomotopy (pmap_compose_ppi_ppi_const f)) qed :
+            by exact !pfiber.sigma_char'
+      ... ≃* psigma_gen (λ(g : Π*(a : A), B a), pmap_compose_ppi f g ~* ppi_const C)
                proof (pmap_compose_ppi_ppi_const f) qed :
              by exact psigma_gen_pequiv_psigma_gen_right (λa, !ppi_eq_equiv)
-                        !ppi_homotopy_of_eq_of_ppi_homotopy
-      ... ≃* psigma_gen (λ(g : Π*(a : A), B a), ppi (λa, f a (g a) = pt)
-               (transport (λb, f pt b = pt) (pppi.resp_pt g)⁻¹ (respect_pt (f pt))))
+                        !phomotopy_of_eq_of_phomotopy
+      ... ≃* @psigma_gen (Π*(a : A), B a) (λ(g : Π*(a : A), B a), ppi (λa, f a (g a) = pt)
+               (transport (λb, f pt b = pt) (respect_pt g)⁻¹ (respect_pt (f pt))))
                (ppi_const _) :
              begin
                refine psigma_gen_pequiv_psigma_gen_right
                         (λg, ppi_equiv_ppi_basepoint (_ ⬝ !eq_transport_Fl⁻¹)) _,
                intro g, refine !con_idp ⬝ _, apply whisker_right,
                exact ap02 (f pt) !inv_inv⁻¹ ⬝ !ap_inv,
-               apply ppi_eq, fapply ppi_homotopy.mk,
+               apply eq_of_phomotopy, fapply phomotopy.mk,
                  intro x, reflexivity,
                  refine !idp_con ⬝ _, symmetry, refine !ap_id ◾ !idp_con ⬝ _, apply con.right_inv
              end
       ... ≃* Π*(a : A), (psigma_gen (λb, f a b = pt) (respect_pt (f a))) :
-             by exact (ppi_psigma _ _)⁻¹ᵉ*
+            by exact (ppi_psigma _ _)⁻¹ᵉ*
       ... ≃* Π*(a : A), pfiber (f a) : by exact ppi_pequiv_right (λa, !pfiber.sigma_char'⁻¹ᵉ*)
 
   /- TODO: proof the following as a special case of pfiber_pppi_compose_left -/
@@ -941,7 +732,7 @@ namespace pointed
                         (λg, ppi_equiv_ppi_basepoint (_ ⬝ !eq_transport_Fl⁻¹)) _,
                intro g, refine !con_idp ⬝ _, apply whisker_right,
                exact ap02 f !inv_inv⁻¹ ⬝ !ap_inv,
-               apply ppi_eq, fapply ppi_homotopy.mk,
+               apply eq_of_phomotopy, fapply phomotopy.mk,
                  intro x, reflexivity,
                  refine !idp_con ⬝ _, symmetry, refine !ap_id ◾ !idp_con ⬝ _, apply con.right_inv
              end
@@ -961,7 +752,7 @@ namespace pointed
         intro a, cases a, exact pt, exact f a,
         reflexivity },
     { intro f, reflexivity },
-    { intro f, cases f with f p, apply ppi_eq, fapply ppi_homotopy.mk,
+    { intro f, cases f with f p, apply eq_of_phomotopy, fapply phomotopy.mk,
       { intro a, cases a, exact p⁻¹, reflexivity },
       { exact con.left_inv p }},
   end
@@ -978,52 +769,52 @@ namespace pointed
      Ω (Π*a, B a) ≃* Π*(a : A), Ω (B a) -/
   definition ppi_eq_equiv_natural_gen_lem {B C : A → Type} {b₀ : B pt} {c₀ : C pt}
     {f : Π(a : A), B a → C a} {f₀ : f pt b₀ = c₀} {k : ppi B b₀} {k' : ppi C c₀}
-    (p : ppi_functor_right f f₀ k ~~* k') :
-    ap1_gen (f pt) (p pt) f₀ (ppi.resp_pt k) = ppi.resp_pt k' :=
+    (p : ppi_functor_right f f₀ k ~* k') :
+    ap1_gen (f pt) (p pt) f₀ (respect_pt k) = respect_pt k' :=
   begin
     symmetry,
     refine _ ⬝ !con.assoc⁻¹,
-    exact eq_inv_con_of_con_eq (ppi_to_homotopy_pt p),
+    exact eq_inv_con_of_con_eq (to_homotopy_pt p),
   end
 
   definition ppi_eq_equiv_natural_gen_lem2 {B C : A → Type} {b₀ : B pt} {c₀ : C pt}
     {f : Π(a : A), B a → C a} {f₀ : f pt b₀ = c₀} {k l : ppi B b₀}
-    {k' l' : ppi C c₀} (p : ppi_functor_right f f₀ k ~~* k')
-    (q : ppi_functor_right f f₀ l ~~* l') :
-      ap1_gen (f pt) (p pt) (q pt) (ppi.resp_pt k ⬝ (ppi.resp_pt l)⁻¹) =
-      ppi.resp_pt k' ⬝ (ppi.resp_pt l')⁻¹ :=
+    {k' l' : ppi C c₀} (p : ppi_functor_right f f₀ k ~* k')
+    (q : ppi_functor_right f f₀ l ~* l') :
+      ap1_gen (f pt) (p pt) (q pt) (respect_pt k ⬝ (respect_pt l)⁻¹) =
+      respect_pt k' ⬝ (respect_pt l')⁻¹ :=
   (ap1_gen_con (f pt) _ f₀ _ _ _ ⬝ (ppi_eq_equiv_natural_gen_lem p) ◾
   (!ap1_gen_inv ⬝ (ppi_eq_equiv_natural_gen_lem q)⁻²))
 
   definition ppi_eq_equiv_natural_gen {B C : A → Type} {b₀ : B pt} {c₀ : C pt}
     {f : Π(a : A), B a → C a} {f₀ : f pt b₀ = c₀} {k l : ppi B b₀}
-    {k' l' : ppi C c₀} (p : ppi_functor_right f f₀ k ~~* k')
-    (q : ppi_functor_right f f₀ l ~~* l') :
-    hsquare (ap1_gen (ppi_functor_right f f₀) (ppi_eq p) (ppi_eq q))
+    {k' l' : ppi C c₀} (p : ppi_functor_right f f₀ k ~* k')
+    (q : ppi_functor_right f f₀ l ~* l') :
+    hsquare (ap1_gen (ppi_functor_right f f₀) (eq_of_phomotopy p) (eq_of_phomotopy q))
             (ppi_functor_right (λa, ap1_gen (f a) (p a) (q a))
               (ppi_eq_equiv_natural_gen_lem2 p q))
-            ppi_homotopy_of_eq
-            ppi_homotopy_of_eq :=
+            phomotopy_of_eq
+            phomotopy_of_eq :=
   begin
     intro r, induction r,
     induction f₀,
     induction k with k k₀,
     induction k₀,
     refine idp ⬝ _,
-    revert l' q, refine ppi_homotopy_rec_idp' _ _,
-    revert k' p, refine ppi_homotopy_rec_idp' _ _,
+    revert l' q, refine phomotopy_rec_idp' _ _,
+    revert k' p, refine phomotopy_rec_idp' _ _,
     reflexivity
   end
 
   definition ppi_eq_equiv_natural_gen_refl {B C : A → Type}
     {f : Π(a : A), B a → C a} {k : Πa, B a} :
-    ppi_eq_equiv_natural_gen (ppi_homotopy.refl (ppi_functor_right f idp (ppi.mk k idp)))
-      (ppi_homotopy.refl (ppi_functor_right f idp (ppi.mk k idp))) idp =
-    ap ppi_homotopy_of_eq !ap1_gen_idp :=
+    ppi_eq_equiv_natural_gen (phomotopy.refl (ppi_functor_right f idp (ppi.mk k idp)))
+      (phomotopy.refl (ppi_functor_right f idp (ppi.mk k idp))) idp =
+    ap phomotopy_of_eq !ap1_gen_idp :=
   begin
     refine !idp_con ⬝ _,
-    refine ppi_homotopy_rec_idp'_refl _ _ ⬝ _,
-    refine ap (transport _ _) !ppi_homotopy_rec_idp'_refl ⬝ _,
+    refine !phomotopy_rec_idp'_refl ⬝ _,
+    refine ap (transport _ _) !phomotopy_rec_idp'_refl ⬝ _,
     refine !tr_diag_eq_tr_tr⁻¹ ⬝ _,
     refine !eq_transport_Fl ⬝ _,
     refine !ap_inv⁻² ⬝ !inv_inv ⬝ !ap_compose ⬝ ap02 _ _,
@@ -1045,7 +836,7 @@ namespace pointed
     fapply phomotopy.mk,
     { exact ppi_eq_equiv_natural_gen (pmap_compose_ppi_ppi_const (λa, pmap_of_map (f a) pt))
               (pmap_compose_ppi_ppi_const (λa, pmap_of_map (f a) pt)) },
-    { exact !ppi_eq_equiv_natural_gen_refl ◾ (!idp_con ⬝ !ppi_eq_refl) }
+    { exact !ppi_eq_equiv_natural_gen_refl ◾ (!idp_con ⬝ !eq_of_phomotopy_refl) }
   end
 
 
@@ -1095,7 +886,7 @@ namespace is_conn
   begin
     apply is_contr.mk pt,
     intro f, induction f with f p,
-    apply ppi_eq, fapply ppi_homotopy.mk,
+    apply eq_of_phomotopy, fapply phomotopy.mk,
     { apply is_conn.elim n, exact p⁻¹ },
     { krewrite (is_conn.elim_β n), apply con.left_inv }
   end
diff --git a/spectrum/basic.hlean b/spectrum/basic.hlean
index 871f3ce..851c89d 100644
--- a/spectrum/basic.hlean
+++ b/spectrum/basic.hlean
@@ -363,13 +363,13 @@ namespace spectrum
     (eq.eq_equiv_homotopy) ⬝e pi_equiv_pi_right (λ n, pmap_eq_equiv (f n) (g n))
 
 /-
-  definition ppi_homotopy_rec_on_eq [recursor]
+  definition phomotopy_rec_on_eq [recursor]
     {k' : ppi B x₀}
-    {Q : (k ~~* k') → Type}
-    (p : k ~~* k')
-    (H : Π(q : k = k'), Q (ppi_homotopy_of_eq q))
+    {Q : (k ~* k') → Type}
+    (p : k ~* k')
+    (H : Π(q : k = k'), Q (phomotopy_of_eq q))
     : Q p :=
-  ppi_homotopy_of_eq_of_ppi_homotopy p ▸ H (eq_of_ppi_homotopy p)
+  phomotopy_of_eq_of_phomotopy p ▸ H (eq_of_phomotopy p)
 -/
   definition fam_phomotopy_rec_on_eq {N : Type} {X Y : N → Type*} (f g : Π n, X n →* Y n)
     {Q : (Π n, f n ~* g n) → Type}
@@ -383,18 +383,18 @@ namespace spectrum
   end
 
 /-
-  definition ppi_homotopy_rec_on_idp [recursor]
-    {Q : Π {k' : ppi B x₀},  (k ~~* k') → Type}
-    (q : Q (ppi_homotopy.refl k)) {k' : ppi B x₀} (H : k ~~* k') : Q H :=
+  definition phomotopy_rec_idp [recursor]
+    {Q : Π {k' : ppi B x₀},  (k ~* k') → Type}
+    (q : Q (phomotopy.refl k)) {k' : ppi B x₀} (H : k ~* k') : Q H :=
   begin
-    induction H using ppi_homotopy_rec_on_eq with t,
-    induction t, exact eq_ppi_homotopy_refl_ppi_homotopy_of_eq_refl k ▸ q,
+    induction H using phomotopy_rec_on_eq with t,
+    induction t, exact eq_phomotopy_refl_phomotopy_of_eq_refl k ▸ q,
   end
 -/
 
 --set_option pp.coercions true
 
-  definition fam_phomotopy_rec_on_idp {N : Type} {X Y : N → Type*} (f : Π n, X n →* Y n)
+  definition fam_phomotopy_rec_idp {N : Type} {X Y : N → Type*} (f : Π n, X n →* Y n)
     (Q : Π (g : Π n, X n →* Y n) (H : Π n, f n ~* g n), Type)
     (q : Q f (λ n, phomotopy.rfl))
     (g : Π n, X n →* Y n) (H : Π n, f n ~* g n) : Q g H :=
@@ -418,14 +418,14 @@ namespace spectrum
     intro n,
     esimp at *,
     revert g H gsq Hsq n,
-    refine fam_phomotopy_rec_on_idp f _ _,
+    refine fam_phomotopy_rec_idp f _ _,
     intro gsq Hsq n,
     refine change_path _ _,
 --    have p : eq_of_homotopy (λ n, eq_of_phomotopy phomotopy.rfl) = refl f,
     reflexivity,
     refine (eq_of_homotopy_eta rfl)⁻¹ ⬝ _,
     fapply ap (eq_of_homotopy), fapply eq_of_homotopy, intro n, refine (eq_of_phomotopy_refl _)⁻¹,
---    fapply eq_of_ppi_homotopy,
+--    fapply eq_of_phomotopy,
     fapply pathover_idp_of_eq,
     note Hsq' := ptube_v_eq_bot phomotopy.rfl (ap1_phomotopy_refl _) (fsq n) (gsq n) (Hsq n),
     unfold ptube_v at *,
@@ -600,7 +600,11 @@ namespace spectrum
   homotopy_group_pequiv 2 (equiv_glue_neg X n)
 
   definition πg_glue (X : spectrum) (n : ℤ) : πg[2] (X (2 - succ n)) ≃g πg[3] (X (2 - n)) :=
-  by rexact homotopy_group_isomorphism_of_pequiv _ (equiv_glue_neg X n)
+  begin
+    change πg[2] (X (2 - succ n)) ≃g πg[2] (Ω (X (2 - n))),
+    apply homotopy_group_isomorphism_of_pequiv,
+    exact equiv_glue_neg X n
+  end
 
   definition πg_glue_homotopy_π_glue (X : spectrum) (n : ℤ) : πg_glue X n ~ π_glue X n :=
   by reflexivity
diff --git a/spectrum/trunc.hlean b/spectrum/trunc.hlean
index 4925e24..ced901b 100644
--- a/spectrum/trunc.hlean
+++ b/spectrum/trunc.hlean
@@ -52,7 +52,7 @@ begin
   induction p, induction k with k k,
   { refine pwhisker_right _ (ap1_phomotopy _) ⬝* @(ap1_ptrunc_elim k f) H,
     apply ptrunc_elim_phomotopy2, reflexivity },
-  { apply phomotopy_of_is_contr_cod, exact is_trunc_maxm2_loop H }
+  { apply phomotopy_of_is_contr_cod_pmap, exact is_trunc_maxm2_loop H }
 end
 
 definition loop_ptrunc_maxm2_pequiv_ptrunc_elim {k : ℤ} {l : ℕ₋₂} (p : maxm2 (k+1) = l)
@@ -70,7 +70,8 @@ definition loop_ptrunc_maxm2_pequiv_ptr {k : ℤ} {l : ℕ₋₂} (p : maxm2 (k+
 begin
   induction p, induction k with k k,
   { exact ap1_ptr k A },
-  { apply phomotopy_pinv_left_of_phomotopy, apply phomotopy_of_is_contr_cod, apply is_trunc_trunc }
+  { apply phomotopy_pinv_left_of_phomotopy, apply phomotopy_of_is_contr_cod_pmap,
+    apply is_trunc_trunc }
 end
 
 definition is_trunc_of_is_trunc_maxm2 (k : ℤ) (X : Type)