diff --git a/homotopy/EM.hlean b/homotopy/EM.hlean
index 87953ba..7080a30 100644
--- a/homotopy/EM.hlean
+++ b/homotopy/EM.hlean
@@ -97,7 +97,7 @@ namespace EM
 
   definition EM_equiv_EM [constructor] {G H : AbGroup} (φ : G ≃g H) (n : ℕ) : K G n ≃* K H n :=
   begin
-    fapply pequiv.MK,
+    fapply pequiv.MK',
     { exact EM_functor φ n },
     { exact EM_functor φ⁻¹ᵍ n },
     { intro x, refine (EM_functor_gcompose φ⁻¹ᵍ φ n)⁻¹* x ⬝ _,
diff --git a/homotopy/smash.hlean b/homotopy/smash.hlean
index 1f0723e..f2b3b4a 100644
--- a/homotopy/smash.hlean
+++ b/homotopy/smash.hlean
@@ -905,7 +905,7 @@ namespace smash
 
   definition smash_comm [constructor] : smash A B ≃* smash B A :=
   begin
-    apply pequiv.MK2, do 2 apply smash_flip_smash_flip
+    apply pequiv.MK, do 2 apply smash_flip_smash_flip
   end
 
   variables {A B}
diff --git a/homotopy/smash_adjoint.hlean b/homotopy/smash_adjoint.hlean
index 8d23779..4c6a01c 100644
--- a/homotopy/smash_adjoint.hlean
+++ b/homotopy/smash_adjoint.hlean
@@ -404,7 +404,7 @@ namespace smash
   definition smash_adjoint_pmap_natural_lm (C : Type*) (f : A →* A') (g : B →* B') :
     psquare (smash_adjoint_pmap A' B' C) (smash_adjoint_pmap A B C)
             (ppcompose_right (f ∧→ g)) (ppcompose_left (ppcompose_right f) ∘* ppcompose_right g) :=
-  (smash_pelim_natural_lm C g f)⁻¹ʰ*
+  proof (!smash_pelim_natural_lm)⁻¹ʰ* qed
 
   /- Corollary: associativity of smash -/
 
@@ -460,7 +460,7 @@ namespace smash
     refine !smash_functor_pid_pcompose⁻¹* ⬝* _,
     apply smash_functor_phomotopy phomotopy.rfl,
     refine !passoc⁻¹* ⬝* _,
-    refine pwhisker_right _ !smash_adjoint_pmap_natural_right ⬝* _,
+    refine pwhisker_right _ (smash_adjoint_pmap_natural_right f) ⬝* _,
     refine !passoc ⬝* _,
     apply pwhisker_left,
     apply smash_elim_inv_natural_right
@@ -468,7 +468,7 @@ namespace smash
 
   definition smash_assoc (A B C : Type*) : A ∧ (B ∧ C) ≃* (A ∧ B) ∧ C :=
   begin
-    fapply pequiv.MK2,
+    fapply pequiv.MK,
     { exact !smash_assoc_elim_equiv⁻¹ᵉ* !pid },
     { exact !smash_assoc_elim_equiv !pid },
     { refine !smash_assoc_elim_inv_natural_right_pt ⬝* _,
@@ -538,7 +538,7 @@ namespace smash
 
   definition smash_psusp (A B : Type*) : A ∧ ⅀ B ≃* ⅀(A ∧ B) :=
   begin
-    fapply pequiv.MK2,
+    fapply pequiv.MK,
     { exact !smash_psusp_elim_equiv⁻¹ᵉ* !pid },
     { exact !smash_psusp_elim_equiv !pid },
     { refine phomotopy_of_eq (!smash_psusp_elim_natural_right⁻¹ʰ* _) ⬝* _,
diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean
index af6b485..4df2fbd 100644
--- a/homotopy/spectrum.hlean
+++ b/homotopy/spectrum.hlean
@@ -189,8 +189,7 @@ namespace spectrum
                          (pwhisker_left (glue F n) (to_phomotopy n))
                          (pwhisker_right (glue E n) (ap1_phomotopy (to_phomotopy (S n))))
                          (glue_square f n)
-                         (glue_square g n)
-    )
+                         (glue_square g n))
 
   infix ` ~ₛ `:50 := shomotopy
 
@@ -344,7 +343,7 @@ namespace spectrum
     end
 
   definition scompose_spoint {N : succ_str} {X Y : gen_spectrum N} (f : X →ₛ Y)
-    : f ∘ₛ spoint f ~ₛ szero (sfiber f) Y :=
+    : f ∘ₛ spoint f ~ₛ !szero :=
   begin
     fapply shomotopy.mk,
     { intro n, exact pcompose_ppoint (f n) },
@@ -479,9 +478,7 @@ namespace spectrum
   definition spectrify_type_fun'_succ {N : succ_str} (X : gen_prespectrum N) (n : N) (k : ℕ) :
     spectrify_type_fun' X n (succ k) ~* Ω→ (spectrify_type_fun' X n k) :=
   begin
-    refine _ ⬝* !ap1_pcompose⁻¹*,
-    apply !pwhisker_right,
-    refine !to_pinv_pequiv_MK2
+    refine !ap1_pcompose⁻¹*
   end
 
   definition spectrify_pequiv {N : succ_str} (X : gen_prespectrum N) (n : N) :
@@ -517,7 +514,7 @@ namespace spectrum
     (equiv_gluen X n (k+1))⁻¹ᵉ* ~*
     (equiv_gluen X n k)⁻¹ᵉ* ∘* Ω→[k] (equiv_glue X (n +' k))⁻¹ᵉ* ∘* !loopn_succ_in :=
   begin
-    refine !trans_pinv ⬝* pwhisker_left _ _, refine !trans_pinv ⬝* _, refine !to_pinv_pequiv_MK2 ◾* !pinv_pinv
+    refine !trans_pinv ⬝* pwhisker_left _ _, refine !trans_pinv ⬝* _, refine pwhisker_left _ !pinv_pinv
   end
 
   definition spectrify_map {N : succ_str} {X : gen_prespectrum N} : X →ₛ spectrify X :=
@@ -550,11 +547,8 @@ namespace spectrum
       refine pwhisker_left _ (pwhisker_right _ (phomotopy_pinv_right_of_phomotopy (!loopn_succ_in_natural)⁻¹*)⁻¹*) ⬝* _,
       refine pwhisker_right _ !apn_pinv ⬝* _,
       refine (phomotopy_pinv_left_of_phomotopy _)⁻¹*,
-      refine pwhisker_right _ !pmap_eta⁻¹* ⬝* _,
       refine apn_psquare k _,
-      refine pwhisker_right _ _  ⬝* psquare_of_phomotopy !smap.glue_square,
-      exact !pmap_eta⁻¹*
-    }
+      refine psquare_of_phomotopy !smap.glue_square }
   end
 
   definition spectrify.elim {N : succ_str} {X : gen_prespectrum N} {Y : gen_spectrum N}
diff --git a/homotopy/wedge.hlean b/homotopy/wedge.hlean
index f3f82fe..10ab20e 100644
--- a/homotopy/wedge.hlean
+++ b/homotopy/wedge.hlean
@@ -29,7 +29,7 @@ namespace wedge
 
   definition pwedge_comm [constructor] (A B : Type*) : A ∨ B ≃* B ∨ A :=
   begin
-    fapply pequiv.MK,
+    fapply pequiv.MK',
     { exact pwedge_flip A B },
     { exact wedge_flip },
     { exact wedge_flip_wedge_flip },
diff --git a/move_to_lib.hlean b/move_to_lib.hlean
index 2192a53..5e0fe4b 100644
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@@ -309,7 +309,7 @@ namespace misc
   definition ptrunc_component' (n : ℕ₋₂) (A : Type*) :
     ptrunc (n.+2) (component A) ≃* component (ptrunc (n.+2) A) :=
   begin
-    fapply pequiv.MK,
+    fapply pequiv.MK',
     { exact ptrunc.elim (n.+2) (component_functor !ptr) },
     { intro x, cases x with x p, induction x with a,
       refine tr ⟨a, _⟩,