diff --git a/colimit/seq_colim.hlean b/colimit/seq_colim.hlean
index 1ddf46e..60689fa 100644
--- a/colimit/seq_colim.hlean
+++ b/colimit/seq_colim.hlean
@@ -723,7 +723,7 @@ incl_kshift_diag f x
 definition seq_colim_eq_equiv0' (a₀ a₁ : A 0) :
   ι f a₀ = ι f a₁ ≃ seq_colim (id_seq_diagram f 0 a₀ a₁) :=
 begin
-  refine total_space_method2 (ι f a₀) (seq_colim_over (id0_seq_diagram_over f a₀))
+  refine total_space_method (ι f a₀) (seq_colim_over (id0_seq_diagram_over f a₀))
     _ _ (ι f a₁) ⬝e _,
   { apply @(is_trunc_equiv_closed_rev _ (sigma_seq_colim_over_equiv _ _)),
     apply is_contr_seq_colim },
diff --git a/colimit/sequence.hlean b/colimit/sequence.hlean
index f126496..a8606a0 100644
--- a/colimit/sequence.hlean
+++ b/colimit/sequence.hlean
@@ -92,7 +92,7 @@ namespace seq_colim
   /- lreplace le_of_succ_le with this -/
 
   definition lrep_f {n m : ℕ} (H : succ n ≤ m) (a : A n) :
-    lrep f H (f a) = lrep f (le_step_left H) a :=
+    lrep f H (f a) = lrep f (le_of_succ_le H) a :=
   begin
     induction H with m H p,
     { reflexivity },
diff --git a/homology/basic.hlean b/homology/basic.hlean
index 0ead27e..851aa8e 100644
--- a/homology/basic.hlean
+++ b/homology/basic.hlean
@@ -54,7 +54,7 @@ namespace homology
 
     theorem Hh_homotopy (n : ℤ) {A B : Type*} (f g : A →* B) (h : f ~ g) : Hh theory n f ~ Hh theory n g := λ x,
     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 (respect_pt f)) x : by exact ap (λ f, Hh theory n f x) (pmap_eta_eq 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 :
                begin
diff --git a/homotopy/pushout.hlean b/homotopy/pushout.hlean
index c8f1a05..2d4759f 100644
--- a/homotopy/pushout.hlean
+++ b/homotopy/pushout.hlean
@@ -111,7 +111,7 @@ namespace pushout
         refine ap (λx, apd10 x _) (ap_compose (λx, x ∘ f) pr1 _ ⬝ ap02 _ !prod_eq_pr1) ⬝ph _
                ⬝hp ap (λx, apd10 x _) (ap_compose (λx, x ∘ g) pr2 _ ⬝ ap02 _ !prod_eq_pr2)⁻¹,
         refine apd10 !apd10_ap_precompose_dependent a ⬝ph _ ⬝hp apd10 !apd10_ap_precompose_dependent⁻¹ a,
-        refine apd10 !apd10_eq_of_homotopy (f a) ⬝ph _ ⬝hp apd10 !apd10_eq_of_homotopy⁻¹ (g a),
+        refine !apd10_eq_of_homotopy ⬝ph _ ⬝hp !apd10_eq_of_homotopy⁻¹,
         refine ap_compose (pushout.elim h k p) _ _ ⬝pv _,
         refine aps (pushout.elim h k p) _ ⬝vp (!elim_glue ⬝ !ap_id⁻¹),
         esimp,   exact sorry
@@ -981,7 +981,7 @@ namespace pushout
     assert H : Π w, P w ≃ pushout.elim_type (P ∘ inl) (P ∘ inr) Pglue w,
     { intro w, induction w with x x x,
       { exact erfl }, { exact erfl },
-      { apply equiv_pathover, intro pfx pgx q,
+      { apply equiv_pathover2, intro pfx pgx q,
         apply pathover_of_tr_eq,
         apply eq.trans (ap10 (elim_type_glue.{u₁ u₂ u₃ u₄}
           (P ∘ inl) (P ∘ inr) Pglue x) pfx), -- why do we need explicit universes here?
diff --git a/homotopy/realprojective.hlean b/homotopy/realprojective.hlean
index e2b8377..d8f1688 100644
--- a/homotopy/realprojective.hlean
+++ b/homotopy/realprojective.hlean
@@ -151,7 +151,7 @@ begin
 end
 
 definition corollary_II_6 : Π A : BoolType, (pt = A) ≃ A :=
-@total_space_method BoolType pt BoolType.carrier theorem_II_2 idp
+@total_space_method BoolType pt BoolType.carrier theorem_II_2 pt
 
 definition is_conn_BoolType [instance] : is_conn 0 BoolType :=
 begin
diff --git a/homotopy/wedge.hlean b/homotopy/wedge.hlean
index 939a415..9933f3c 100644
--- a/homotopy/wedge.hlean
+++ b/homotopy/wedge.hlean
@@ -258,9 +258,9 @@ pequiv.MK (nar_of_noo f g h) (noo_of_nar f g h)
 -- apply eq_pathover_id_right, refine ap_compose nar_of_noo _ _ ⬝ ap02 _ !elim_glue ⬝ph _
 -- apply eq_pathover_id_right, refine ap_compose noo_of_nar _ _ ⬝ ap02 _ !elim_glue ⬝ph _
 
-  definition loop_pequiv_of_cross_section {A B : Type*} (f : A →* B) (g : B →* A)
-    (h : f ∘* g ~* pid B) : Ω A ≃* Ω (pfiber f) ×* Ω B :=
-
+  -- definition loop_pequiv_of_cross_section {A B : Type*} (f : A →* B) (g : B →* A)
+  --   (h : f ∘* g ~* pid B) : Ω A ≃* Ω (pfiber f) ×* Ω B :=
+  -- sorry
 
 
 
diff --git a/move_to_lib.hlean b/move_to_lib.hlean
index 6c65c6c..b06fc71 100644
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@@ -23,6 +23,7 @@ is_trunc_loop_of_is_trunc > is_trunc_loopn_of_is_trunc
 
 
 first two arguments reordered in is_trunc_loopn_nat
+reorder pathover arguments of constructions with squareovers (mostly implicit)
 -/
 
 namespace eq
diff --git a/pointed.hlean b/pointed.hlean
index a0b9d2b..6677ea8 100644
--- a/pointed.hlean
+++ b/pointed.hlean
@@ -213,13 +213,6 @@ namespace pointed
 
 /- Homotopy between a function and its eta expansion -/
 
-  definition pmap_eta [constructor] {X Y : Type*} (f : X →* Y) : f ~* pmap.mk f (respect_pt f) :=
-  begin
-    fapply phomotopy.mk,
-    reflexivity,
-    esimp, exact !idp_con
-  end
-
   definition papply_point [constructor] (A B : Type*) : papply B pt ~* pconst (ppmap A B) B :=
   phomotopy.mk (λf, respect_pt f) idp
 
diff --git a/pointed_cubes.hlean b/pointed_cubes.hlean
index 79392cc..6735771 100644
--- a/pointed_cubes.hlean
+++ b/pointed_cubes.hlean
@@ -91,13 +91,22 @@ begin
   exact (pconst_pcompose fleft)⁻¹*,
 end
 
-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 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 :=
+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
 
-definition ptube_h {A B C D : Type*} {ftop : A →* B} {fbot : C →* D} {fleft fleft' : A →* C} (phtpy_left : fleft ~* fleft') {fright fright' : B →* D} (phtpy_right : fright ~* fright') (psq_back : psquare ftop fbot fleft fright) (psq_front : psquare ftop fbot fleft' fright') : Type :=
+definition ptube_h {A B C D : Type*} {ftop : A →* B} {fbot : C →* D} {fleft fleft' : A →* C}
+  (phtpy_left : fleft ~* fleft') {fright fright' : B →* D} (phtpy_right : fright ~* fright')
+  (psq_back : psquare ftop fbot fleft fright) (psq_front : psquare ftop fbot fleft' fright') :
+  Type :=
 phsquare (pwhisker_right ftop phtpy_right) (pwhisker_left fbot phtpy_left) psq_back psq_front
 
 --print pinv_right_phomotopy_of_phomotopy
diff --git a/pointed_pi.hlean b/pointed_pi.hlean
index 446f324..eb3cfdd 100644
--- a/pointed_pi.hlean
+++ b/pointed_pi.hlean
@@ -47,7 +47,7 @@ namespace pointed
     apply eq_of_fn_eq_fn eq_equiv_homotopy,
     apply eq_of_homotopy, intro b,
     refine !apd10_con ⬝ _,
-    refine whisker_right _ !pi.apd10_eq_of_homotopy ⬝ q b
+    refine whisker_right _ !apd10_eq_of_homotopy ⬝ q b
   end
 
   definition pupi_functor [constructor] {A A' : Type} {B : A → Type*} {B' : A' → Type*}
@@ -65,9 +65,9 @@ namespace pointed
   begin
     fapply phomotopy_mk_pupi,
     { intro h a, reflexivity },
-    { intro a, refine !idp_con ⬝ _, refine !apd10_con ⬝ _ ⬝ !pi.apd10_eq_of_homotopy⁻¹, esimp,
-      refine (!apd10_prepostcompose ⬝ ap02 (g' a) !pi.apd10_eq_of_homotopy) ◾
-             !pi.apd10_eq_of_homotopy }
+    { intro a, refine !idp_con ⬝ _, refine !apd10_con ⬝ _ ⬝ !apd10_eq_of_homotopy⁻¹, esimp,
+      refine (!apd10_prepostcompose ⬝ ap02 (g' a) !apd10_eq_of_homotopy) ◾
+             !apd10_eq_of_homotopy }
   end
 
   definition pupi_functor_pid (A : Type) (B : A → Type*) :
@@ -75,7 +75,7 @@ namespace pointed
   begin
     fapply phomotopy_mk_pupi,
     { intro h a, reflexivity },
-    { intro a, refine !idp_con ⬝ !pi.apd10_eq_of_homotopy⁻¹ }
+    { intro a, refine !idp_con ⬝ !apd10_eq_of_homotopy⁻¹ }
   end
 
   definition pupi_functor_phomotopy {A A' : Type} {B : A → Type*} {B' : A' → Type*}
@@ -86,8 +86,8 @@ namespace pointed
     fapply phomotopy_mk_pupi,
     { intro h a, exact q a (h (f a)) ⬝ ap (g' a) (apdt h (p a)) },
     { intro a, esimp,
-     exact whisker_left _ !pi.apd10_eq_of_homotopy ⬝ !con.assoc ⬝
-           to_homotopy_pt (q a) ⬝ !pi.apd10_eq_of_homotopy⁻¹ }
+     exact whisker_left _ !apd10_eq_of_homotopy ⬝ !con.assoc ⬝
+           to_homotopy_pt (q a) ⬝ !apd10_eq_of_homotopy⁻¹ }
   end
 
   definition pupi_pequiv [constructor] {A A' : Type} {B : A → Type*} {B' : A' → Type*}
@@ -634,7 +634,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_eq_of_phomotopy⁻¹,
+        refine !apd10_eq_of_homotopy_fn ⬝ _ ⬝ !apd10_to_fun_eq_of_phomotopy⁻¹,
         apply eq_of_homotopy, intro a, reflexivity },
       { exact sorry } }
   end
diff --git a/spectrum/basic.hlean b/spectrum/basic.hlean
index defccbe..54815fb 100644
--- a/spectrum/basic.hlean
+++ b/spectrum/basic.hlean
@@ -8,8 +8,8 @@ Authors: Michael Shulman, Floris van Doorn, Egbert Rijke, Stefano Piceghello, Yu
 import homotopy.LES_of_homotopy_groups ..algebra.splice ..algebra.seq_colim ..homotopy.EM ..homotopy.fwedge
        ..pointed_cubes
 
-open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group
-     succ_str EM EM.ops function unit lift is_trunc
+open eq nat int susp pointed sigma is_equiv equiv fiber algebra trunc trunc_index pi group
+     succ_str EM EM.ops function unit lift is_trunc sigma.ops
 
 /---------------------
   Basic definitions
@@ -19,7 +19,7 @@ open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc
 
 structure gen_prespectrum (N : succ_str) :=
   (deloop : N → Type*)
-  (glue : Π(n:N), (deloop n) →* (Ω (deloop (S n))))
+  (glue : Π(n:N), deloop n →* Ω (deloop (S n)))
 
 attribute gen_prespectrum.deloop [coercion]
 
@@ -182,14 +182,12 @@ namespace spectrum
 
   definition smap_to_sigma [unfold 4] {N : succ_str} {X Y : gen_prespectrum N} (f : X →ₛ Y) : smap_sigma X Y :=
   begin
-    induction f with f fsq,
-    exact sigma.mk f fsq,
+    exact sigma.mk (smap.to_fun f) (glue_square f),
   end
 
   definition smap_to_struc [unfold 4] {N : succ_str} {X Y : gen_prespectrum N} (f : smap_sigma X Y) : X →ₛ Y :=
   begin
-    induction f with f fsq,
-    exact smap.mk f fsq,
+    exact smap.mk f.1 f.2,
   end
 
   definition smap_to_sigma_isretr {N : succ_str} {X Y : gen_prespectrum N} (f : smap_sigma X Y) :
@@ -220,43 +218,25 @@ namespace spectrum
   glue_square f n
 
   definition sid [constructor] [refl] {N : succ_str} (E : gen_prespectrum N) : E →ₛ E :=
-  smap.mk (λ n, pid (E n)) (λ n, psquare_of_phtpy_bot (ap1_pid) (psquare_of_pid_top_bot (phomotopy.rfl)))
-
-  --print sid
- --   smap.mk (λn, pid (E n))
- --   (λn, calc glue E n ∘* pid (E n) ~* glue E n                   : pcompose_pid
- --                             ...   ~* pid (Ω(E (S n))) ∘* glue E n : pid_pcompose
- --                             ...   ~* Ω→(pid (E (S n))) ∘* glue E n : pwhisker_right (glue E n) ap1_pid⁻¹*)
+  begin
+    apply smap.mk (λ n, pid (E n)),
+    intro n, exact phrfl ⬝vp* !ap1_pid
+  end
 
   definition scompose [trans] {N : succ_str} {X Y Z : gen_prespectrum N}
     (g : Y →ₛ Z) (f : X →ₛ Y) : X →ₛ Z :=
-    smap.mk (λn, g n ∘* f n)
-            (λ n, psquare_of_phtpy_bot
-                    (ap1_pcompose (g (S n)) (f (S n)))
-                    (psquare_hcompose (glue_square f n) (glue_square g n)))
-
-/-
-      (λn, calc glue Z n ∘* to_fun g n ∘* to_fun f n
-             ~* (glue Z n ∘* to_fun g n) ∘* to_fun f n                 : passoc
-         ... ~* (Ω→(to_fun g (S n)) ∘* glue Y n) ∘* to_fun f n      : pwhisker_right (to_fun f n) (glue_square g n)
-         ... ~* Ω→(to_fun g (S n)) ∘* (glue Y n ∘* to_fun f n)      : passoc
-         ... ~* Ω→(to_fun g (S n)) ∘* (Ω→ (f (S n)) ∘* glue X n) : pwhisker_left (Ω→(to_fun g (S n))) (glue_square f n)
-         ... ~* (Ω→(to_fun g (S n)) ∘* Ω→(f (S n))) ∘* glue X n  : passoc
-         ... ~* Ω→(to_fun g (S n) ∘* to_fun f (S n)) ∘* glue X n : pwhisker_right (glue X n) (ap1_pcompose _ _))
--/
+  begin
+    apply smap.mk (λn, g n ∘* f n),
+    intro n, exact (glue_square f n ⬝h* glue_square g n) ⬝vp* !ap1_pcompose
+  end
 
   infixr ` ∘ₛ `:60 := scompose
 
   definition szero [constructor] {N : succ_str} (E F : gen_prespectrum N) : E →ₛ F :=
-    smap.mk (λn, pconst (E n) (F n))
-            (λn, psquare_of_phtpy_bot (ap1_pconst (E (S n)) (F (S n)))
-                   (psquare_of_pconst_top_bot (glue E n) (glue F n)))
-
-/-
-      (λn, calc glue F n ∘* pconst (E n) (F n) ~* pconst (E n) (Ω(F (S n)))                    : pcompose_pconst
-                                         ...   ~* pconst (Ω(E (S n))) (Ω(F (S n))) ∘* glue E n : pconst_pcompose
-                                         ...   ~* Ω→(pconst (E (S n)) (F (S n))) ∘* glue E n   : pwhisker_right (glue E n) (ap1_pconst _ _))
--/
+  begin
+    apply smap.mk (λn, pconst (E n) (F n)),
+    intro n, exact !hpconst_square ⬝vp* !ap1_pconst
+  end
 
   definition stransport [constructor] {N : succ_str} {A : Type} {a a' : A} (p : a = a')
   (E : A → gen_prespectrum N) : E a →ₛ E a' :=
@@ -270,7 +250,7 @@ namespace spectrum
     (to_phomotopy : Πn, f n ~* g n)
     (glue_homotopy : Πn, ptube_v
                            (to_phomotopy n)
-                           (ap1_phomotopy (to_phomotopy (S n)))
+                           (Ω⇒ (to_phomotopy (S n)))
                            (glue_square f n)
                            (glue_square g n))
 
@@ -282,6 +262,7 @@ namespace spectrum
 -/
 
   infix ` ~ₛ `:50 := shomotopy
+  attribute [coercion] shomotopy.to_phomotopy
 
   definition shomotopy_compose {N : succ_str} {E F : gen_prespectrum N} {f g h : E →ₛ F} (p : g ~ₛ h) (q : f ~ₛ g) : f ~ₛ h :=
   shomotopy.mk
@@ -314,10 +295,7 @@ namespace spectrum
       (glue_square g n)
 
   definition shomotopy_to_sigma [unfold 6] {N : succ_str} {X Y : gen_prespectrum N} {f g : X →ₛ Y} (H : f ~ₛ g) : shomotopy_sigma f g :=
-  begin
-    induction H with H Hsq,
-    exact sigma.mk H Hsq,
-  end
+  ⟨H, shomotopy.glue_homotopy H⟩
 
   definition shomotopy_to_struct [unfold 6] {N : succ_str} {X Y : gen_prespectrum N} {f g : X →ₛ Y} (H : shomotopy_sigma f g) : f ~ₛ g :=
   begin
@@ -423,7 +401,7 @@ namespace spectrum
     refine change_path _ _,
 --    have p : eq_of_homotopy (λ n, eq_of_phomotopy phomotopy.rfl) = refl f,
     reflexivity,
-    refine (eq_of_homotopy_eta rfl)⁻¹ ⬝ _,
+    refine (eq_of_homotopy_apd10 rfl)⁻¹ ⬝ _,
     fapply ap (eq_of_homotopy), fapply eq_of_homotopy, intro n, refine (eq_of_phomotopy_refl _)⁻¹,
 --    fapply eq_of_phomotopy,
     fapply pathover_idp_of_eq,
@@ -552,6 +530,7 @@ namespace spectrum
   smap.mk (λn, ppoint (f n))
     begin
       intro n,
+--      refine _ ⬝vp* !ppoint_loop_pfiber_inv,
       refine _ ⬝* !passoc,
       refine _ ⬝* pwhisker_right _ !ppoint_loop_pfiber_inv⁻¹*,
       rexact (pfiber_pequiv_of_square_ppoint (equiv_glue X n) (equiv_glue Y n) (sglue_square f n))⁻¹*
@@ -562,7 +541,7 @@ namespace spectrum
   begin
     fapply shomotopy.mk,
     { intro n, exact pcompose_ppoint (f n) },
-    { intro n, exact sorry }
+    { intro n, esimp, exact sorry }
   end
 
   /---------------------
@@ -750,9 +729,9 @@ namespace spectrum
       intro k,
       note sq1 := homotopy_group_homomorphism_psquare (k+2) (ptranspose (smap.glue_square f (-n + 2 +[ℤ] k))),
       note sq2 := homotopy_group_functor_psquare (k+2) (ap1_psquare (ptransport_natural E F f (add.assoc (-n + 2) k 1))),
-      note sq3 := (homotopy_group_succ_in_natural (k+2) (f (-n + 2 +[ℤ] (k+1))))⁻¹ʰᵗʸʰ,
-      note sq4 := hsquare_of_psquare sq2,
-      note rect := sq1 ⬝htyh sq4 ⬝htyh sq3,
+      -- note sq3 := (homotopy_group_succ_in_natural (k+2) (f (-n + 2 +[ℤ] (k +[ℕ] 1))))⁻¹ʰᵗʸʰ,
+      -- note sq4 := hsquare_of_psquare sq2,
+      -- note rect := sq1 ⬝htyh sq4 ⬝htyh sq3,
       exact sorry --sq1 ⬝htyh sq4 ⬝htyh sq3,
     end
   qed
diff --git a/spectrum/trunc.hlean b/spectrum/trunc.hlean
index ced901b..c81043a 100644
--- a/spectrum/trunc.hlean
+++ b/spectrum/trunc.hlean
@@ -7,7 +7,7 @@ Truncatedness and truncation of spectra
 -/
 
 import .basic
-open int trunc eq is_trunc lift unit pointed equiv is_equiv algebra EM
+open int trunc eq is_trunc lift unit pointed equiv is_equiv algebra EM trunc_index
 
 namespace spectrum