diff --git a/algebra/arrow_group.hlean b/algebra/arrow_group.hlean
index 3b3a9ed..33e1833 100644
--- a/algebra/arrow_group.hlean
+++ b/algebra/arrow_group.hlean
@@ -197,7 +197,7 @@ namespace group
   begin
     apply isomorphism.mk (Group_trunc_pmap_homomorphism f),
     apply @is_equiv_trunc_functor,
-    exact to_is_equiv (pequiv_ppcompose_right f),
+    exact to_is_equiv (ppmap_pequiv_ppmap_left f),
   end
 
   definition Group_trunc_pmap_isomorphism_refl (A B : Type*) (x : Group_trunc_pmap A B) :
diff --git a/algebra/cogroup.hlean b/algebra/cogroup.hlean
index dc9eaed..5cd60fd 100644
--- a/algebra/cogroup.hlean
+++ b/algebra/cogroup.hlean
@@ -186,7 +186,7 @@ section
       { reflexivity },
       { exact glue pt },
       { apply eq_pathover,
-        krewrite [ap_id,ap_compose' (wpr1 (⅀ A) (⅀ A)) (pinch A)],
+        krewrite [ap_id,-ap_compose' (wpr1 (⅀ A) (⅀ A)) (pinch A)],
         krewrite elim_merid, rewrite ap_con,
         krewrite [pushout.elim_inr,ap_constant],
         rewrite ap_con, krewrite [pushout.elim_inl,pushout.elim_glue,ap_id],
@@ -201,7 +201,7 @@ section
       { reflexivity },
       { reflexivity },
       { apply eq_pathover,
-        krewrite [ap_id,ap_compose' (wpr2 (⅀ A) (⅀ A)) (pinch A)],
+        krewrite [ap_id,-ap_compose' (wpr2 (⅀ A) (⅀ A)) (pinch A)],
         krewrite elim_merid, rewrite ap_con,
         krewrite [pushout.elim_inr,ap_id],
         rewrite ap_con, krewrite [pushout.elim_inl,pushout.elim_glue,ap_constant],
diff --git a/algebra/exactness.hlean b/algebra/exactness.hlean
index 9fdec90..8e78fca 100644
--- a/algebra/exactness.hlean
+++ b/algebra/exactness.hlean
@@ -205,7 +205,7 @@ begin
   { intro b p, note q := eq_of_inv_eq ((homotopy_top_of_hsquare' h₂ b)⁻¹ ⬝ p) ⬝ respect_pt eC,
     induction is_short_exact.ker_in_im H (eB b) q with a' r,
     apply image.mk (eA⁻¹ a'),
-    exact eq_of_fn_eq_fn eB ((homotopy_top_of_hsquare h₁⁻¹ʰᵗʸᵛ a')⁻¹ ⬝ r) },
+    exact inj eB ((homotopy_top_of_hsquare h₁⁻¹ʰᵗʸᵛ a')⁻¹ ⬝ r) },
   { apply is_surjective_homotopy_closed_rev (homotopy_top_of_hsquare' h₂),
     apply is_surjective_compose, apply is_surjective_of_is_equiv,
     apply is_surjective_compose, apply is_short_exact.is_surj H, apply is_surjective_of_is_equiv }
diff --git a/algebra/graded.hlean b/algebra/graded.hlean
index d4f3f85..261dcf0 100644
--- a/algebra/graded.hlean
+++ b/algebra/graded.hlean
@@ -151,7 +151,7 @@ definition graded_hom_change_image {f : M₁ →gm M₂} {i j k : I} {m : M₂ k
   (q : deg f j = k) (h : image (f ↘ p) m) : image (f ↘ q) m :=
 begin
   have Σ(r : i = j), ap (deg f) r = p ⬝ q⁻¹,
-  from ⟨eq_of_fn_eq_fn (deg f) (p ⬝ q⁻¹), !ap_eq_of_fn_eq_fn'⟩,
+  from ⟨inj (deg f) (p ⬝ q⁻¹), !ap_inj'⟩,
   induction this with r s, induction r, induction q, esimp at s, induction s, exact h
 end
 
@@ -159,7 +159,7 @@ definition graded_hom_codom_rec {f : M₁ →gm M₂} {j : I} {P : Π⦃i⦄, de
   {i i' : I} (p : deg f i = j) (h : P p) (q : deg f i' = j) : P q :=
 begin
   have Σ(r : i = i'), ap (deg f) r = p ⬝ q⁻¹,
-  from ⟨eq_of_fn_eq_fn (deg f) (p ⬝ q⁻¹), !ap_eq_of_fn_eq_fn'⟩,
+  from ⟨inj (deg f) (p ⬝ q⁻¹), !ap_inj'⟩,
   induction this with r s, induction r, induction q, esimp at s, induction s, exact h
 end
 
diff --git a/algebra/left_module.hlean b/algebra/left_module.hlean
index cdc293f..e9b49d4 100644
--- a/algebra/left_module.hlean
+++ b/algebra/left_module.hlean
@@ -259,7 +259,7 @@ section
       end,
     have ∀ f : LeftModule.carrier M₁ → LeftModule.carrier M₂,
       is_set (is_module_hom (Ring.carrier R) f), from _,
-    apply is_trunc_equiv_closed_rev, exact H
+    exact is_trunc_equiv_closed_rev _ H _
   end
 
   variables {M₁ M₂}
@@ -350,9 +350,9 @@ end
   homomorphism.mk φ⁻¹
     abstract begin
     split,
-      intro g₁ g₂, apply eq_of_fn_eq_fn' φ,
+      intro g₁ g₂, apply inj' φ,
       rewrite [respect_add φ, +right_inv φ],
-      intro r x, apply eq_of_fn_eq_fn' φ,
+      intro r x, apply inj' φ,
       rewrite [to_respect_smul φ, +right_inv φ],
     end end
 
diff --git a/algebra/ses.hlean b/algebra/ses.hlean
index 89f0eea..f437987 100644
--- a/algebra/ses.hlean
+++ b/algebra/ses.hlean
@@ -89,7 +89,7 @@ definition SES_of_isomorphism_right {B C : AbGroup} (g : B ≃g C) : SES trivial
     intro b p,
     have q : g b = g 1,
     from p ⬝ (respect_one g)⁻¹,
-    note r := eq_of_fn_eq_fn (equiv_of_isomorphism g) q,
+    note r := inj (equiv_of_isomorphism g) q,
     fapply tr, fapply fiber.mk, exact unit.star, rewrite r,
   end
 
@@ -133,7 +133,7 @@ begin
   exact g,
   fapply is_embedding_of_is_injective,
   intro x y p,
-  fapply eq_of_fn_eq_fn (equiv_of_isomorphism α),
+  fapply inj (equiv_of_isomorphism α),
   fapply @is_injective_of_is_embedding _ _ f (SES.Hf ses) (α x) (α y),
   rewrite [H x], rewrite [H y], exact p,
   exact SES.Hg ses,
diff --git a/algebra/spectral_sequence.hlean b/algebra/spectral_sequence.hlean
index 6132e96..c2cb563 100644
--- a/algebra/spectral_sequence.hlean
+++ b/algebra/spectral_sequence.hlean
@@ -40,7 +40,7 @@ namespace left_module
     is_contr (part H n) :=
   begin
     induction n with n IH,
-    { exact is_trunc_equiv_closed_rev -2 (equiv_of_isomorphism (e0 H)) },
+    { exact is_trunc_equiv_closed_rev -2 (equiv_of_isomorphism (e0 H)) _ },
     { exact is_contr_right_of_short_exact_mod (ses H n) IH }
   end
 
@@ -55,7 +55,7 @@ namespace left_module
   have is_contr (part H 0), from
   nat.rec_down (λn, is_contr (part H n)) _ (HD' H _ !le.refl)
     (λn H2, is_contr_middle_of_short_exact_mod (ses H n) (HE n) H2),
-  is_contr_equiv_closed (equiv_of_isomorphism (e0 H))
+  is_contr_equiv_closed (equiv_of_isomorphism (e0 H)) _
 
   definition is_built_from_isomorphism (e : D ≃lm D') (f : Πn, E n ≃lm E' n)
     (H : is_built_from D E) : is_built_from D' E' :=
@@ -661,7 +661,7 @@ namespace left_module
   begin
     assert H2 : Π(l : ℕ), is_contr (Einfdiag n l),
     { intro l, apply is_contr_E,
-      refine @(is_trunc_equiv_closed_rev -2 (equiv_of_isomorphism (e c _))) (H n l) },
+      refine is_trunc_equiv_closed_rev -2 (equiv_of_isomorphism (e c _)) (H n l) },
     assert H3 : is_contr (Dinfdiag n 0),
     { fapply nat.rec_down (λk, is_contr (Dinfdiag n k)),
       { exact is_bounded.B HH (deg (k X) (n, s₀ n)) },
@@ -669,7 +669,7 @@ namespace left_module
       { intro l H,
         exact is_contr_middle_of_short_exact_mod (short_exact_mod_infpage HH (n, s₀ n) l)
                 (H2 l) H }},
-    refine @is_trunc_equiv_closed _ _ _ _ H3,
+    refine is_trunc_equiv_closed _ _ H3,
     exact equiv_of_isomorphism (Dinfdiag0 HH (n, s₀ n) (HB c n) ⬝lm f c n)
   end
 
diff --git a/algebra/subgroup.hlean b/algebra/subgroup.hlean
index 9af352d..e58ccb1 100644
--- a/algebra/subgroup.hlean
+++ b/algebra/subgroup.hlean
@@ -32,7 +32,7 @@ namespace group
     { intro b, cases b, reflexivity },
     { intro a, cases a with a1 a2, cases a2, reflexivity }
   end,
-  is_trunc_equiv_closed _ this
+  is_trunc_equiv_closed _ this _
   qed
 
   /-- Every group G has at least two subgroups, the trivial subgroup containing only one, and the full subgroup. --/
diff --git a/cohomology/basic.hlean b/cohomology/basic.hlean
index ec6bdbd..69eb5c9 100644
--- a/cohomology/basic.hlean
+++ b/cohomology/basic.hlean
@@ -136,7 +136,7 @@ definition cohomology_isomorphism_refl (X : Type*) (Y : spectrum) (n : ℤ) (x :
 definition cohomology_isomorphism_right (X : Type*) {Y Y' : spectrum} (e : Πn, Y n ≃* Y' n)
   (n : ℤ) : H^n[X, Y] ≃g H^n[X, Y'] :=
 cohomology_isomorphism_shomotopy_group_sp_cotensor X Y !neg_neg ⬝g
-shomotopy_group_isomorphism_of_pequiv (-n) (λk, pequiv_ppcompose_left (e k)) ⬝g
+shomotopy_group_isomorphism_of_pequiv (-n) (λk, ppmap_pequiv_ppmap_right (e k)) ⬝g
 (cohomology_isomorphism_shomotopy_group_sp_cotensor X Y' !neg_neg)⁻¹ᵍ
 
 definition unreduced_cohomology_isomorphism {X X' : Type} (f : X' ≃ X) (Y : spectrum) (n : ℤ) :
@@ -231,7 +231,7 @@ definition cohomology_susp_1 (X : Type*) (Y : spectrum) (n : ℤ) :
   susp X →* Ω (Ω (Y (n + 1 + 2))) ≃ X →* Ω (Ω (Y (n+2))) :=
 calc
   susp X →* Ω[2] (Y (n + 1 + 2)) ≃ X →* Ω (Ω[2] (Y (n + 1 + 2))) : susp_adjoint_loop_unpointed
-    ... ≃ X →* Ω[2] (Y (n+2)) : equiv_of_pequiv (pequiv_ppcompose_left
+    ... ≃ X →* Ω[2] (Y (n+2)) : equiv_of_pequiv (ppmap_pequiv_ppmap_right
                                                   (cohomology_susp_2 Y n))
 
 definition cohomology_susp_1_pmap_mul {X : Type*} {Y : spectrum} {n : ℤ}
@@ -302,8 +302,8 @@ end
 
 theorem EM_dimension (G : AbGroup) (n : ℤ) (H : n ≠ 0) :
   is_contr (ordinary_cohomology (plift pbool) G n) :=
-@(is_trunc_equiv_closed_rev -2
-  (equiv_of_isomorphism (cohomology_isomorphism (pequiv_plift pbool) _ _)))
+is_trunc_equiv_closed_rev -2
+  (equiv_of_isomorphism (cohomology_isomorphism (pequiv_plift pbool) _ _))
   (EM_dimension' G n H)
 
 open group algebra
@@ -316,7 +316,7 @@ theorem is_contr_cohomology_of_is_contr_spectrum (n : ℤ) (X : Type*) (Y : spec
 begin
   apply is_trunc_trunc_of_is_trunc,
   apply is_trunc_pmap,
-  apply is_trunc_equiv_closed_rev,
+  refine is_contr_equiv_closed_rev _ H,
   exact loop_pequiv_loop (loop_pequiv_loop (pequiv_ap Y (add.assoc n 1 1)⁻¹) ⬝e* (equiv_glue Y (n+1))⁻¹ᵉ*) ⬝e
     (equiv_glue Y n)⁻¹ᵉ*
 end
diff --git a/colimit/omega_compact.hlean b/colimit/omega_compact.hlean
index 3f98581..daa9a6f 100644
--- a/colimit/omega_compact.hlean
+++ b/colimit/omega_compact.hlean
@@ -75,7 +75,7 @@ namespace seq_colim
     { intro h, induction h with n h n h,
       { esimp, apply ap (ι' _ n), apply unit_arrow_eq},
       { esimp, apply eq_pathover_id_right,
-        refine ap_compose' (seq_colim.elim _ _ _) _ _ ⬝ph _,
+        refine ap_compose (seq_colim.elim _ _ _) _ _ ⬝ph _,
         refine ap02 _ !elim_glue ⬝ph _,
         refine !elim_glue ⬝ph _,
         refine _ ⬝pv natural_square_tr (@glue _ (seq_diagram_arrow_left f unit) n) (unit_arrow_eq h),
diff --git a/colimit/omega_compact_sum.hlean b/colimit/omega_compact_sum.hlean
index 0f993a4..faa0db7 100644
--- a/colimit/omega_compact_sum.hlean
+++ b/colimit/omega_compact_sum.hlean
@@ -107,9 +107,9 @@ begin
     refine ap02 _ (!elim_glue ⬝ !idp_con) ⬝ _,
     refine !ap_compose ⬝ _, refine ap02 _ !elim_glue ⬝ _,
     refine !ap_compose ⬝ _, esimp, refine ap02 _ !ap_sigma_functor_id_sigma_eq ⬝ _,
-    apply eq_of_fn_eq_fn (prod_eq_equiv _ _), apply pair_eq,
-    { exact !ap_compose'⁻¹ ⬝ !sigma_eq_pr1 ⬝ !prod_eq_pr1⁻¹ },
-    { refine !ap_compose'⁻¹ ⬝ _ ⬝ !prod_eq_pr2⁻¹, esimp,
+    apply inj (prod_eq_equiv _ _), apply pair_eq,
+    { exact !ap_compose' ⬝ !sigma_eq_pr1 ⬝ !prod_eq_pr1⁻¹ },
+    { refine !ap_compose' ⬝ _ ⬝ !prod_eq_pr2⁻¹, esimp,
       refine !sigma_eq_pr2_constant ⬝ _,
       refine !eq_of_pathover_apo ⬝ _, exact sorry }}
 end
diff --git a/colimit/pointed.hlean b/colimit/pointed.hlean
index 36c1c85..9b4a3ea 100644
--- a/colimit/pointed.hlean
+++ b/colimit/pointed.hlean
@@ -45,7 +45,7 @@ namespace seq_colim
       refine _ ⬝ whisker_right _ !con.assoc,
       refine _ ⬝ (con.assoc (_ ⬝ _) _ _)⁻¹,
       xrewrite [-IH],
-      esimp[shift_up], rewrite [elim_glue,  ap_inv, -ap_compose'], esimp,
+      esimp[shift_up], rewrite [elim_glue,  ap_inv, ap_compose'], esimp,
       rewrite [-+con.assoc], apply whisker_right,
       rewrite con.assoc, apply !eq_inv_con_of_con_eq,
       symmetry, exact eq_of_square !natural_square
@@ -89,15 +89,15 @@ namespace seq_colim
     { esimp[inclusion_pt], exact !idp_con⁻¹ },
     { esimp[inclusion_pt], rewrite [+ap_con, -+ap_inv, +con.assoc, +seq_colim_functor_glue],
       xrewrite[-IH],
-      rewrite[-+ap_compose', -+con.assoc],
+      rewrite[+ap_compose', -+con.assoc],
       apply whisker_right, esimp,
       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, ap_con, ap_compose', +ap_inv],
       rewrite[-+con.assoc],
       refine _ ⬝ whisker_right _ (whisker_right _ (whisker_right _ (whisker_right _ !con.left_inv⁻¹))),
       rewrite[idp_con, +con.assoc], apply whisker_left,
-      rewrite[ap_con, -ap_compose', con_inv, +con.assoc], apply whisker_left,
+      rewrite[ap_con, ap_compose', con_inv, +con.assoc], apply whisker_left,
       refine eq_inv_con_of_con_eq _,
       symmetry, exact eq_of_square !natural_square
     }
@@ -139,7 +139,7 @@ namespace seq_colim
       rewrite ap_con, rewrite ap_con,
       rewrite elim_glue,
       rewrite [-ap_inv],
-      rewrite [-ap_compose'], esimp,
+      rewrite [ap_compose'], esimp,
       rewrite [(eq_con_inv_of_con_eq (!to_homotopy_pt))],
       rewrite [IH],
       rewrite [con_inv],
diff --git a/colimit/seq_colim.hlean b/colimit/seq_colim.hlean
index 60689fa..98f2355 100644
--- a/colimit/seq_colim.hlean
+++ b/colimit/seq_colim.hlean
@@ -65,7 +65,7 @@ begin
                                                  (left_inv (@f _) a))) _,
     apply move_top_of_left, apply move_left_of_bot,
     refine ap02 _ (whisker_left _ (adj (@f _) a)) ⬝pv _,
-    rewrite [-+ap_con, -ap_compose', ap_id],
+    rewrite [-+ap_con, ap_compose', ap_id],
     apply natural_square_tr },
   { intro a, reflexivity }
 end
@@ -109,7 +109,7 @@ begin
   apply eq_pathover, apply hdeg_square,
   refine !seq_colim_functor_glue ⬝ _ ⬝ (ap_compose (seq_colim_functor _ _) _ _)⁻¹,
   refine _ ⬝ (ap02 _ proof !seq_colim_functor_glue qed ⬝ !ap_con)⁻¹,
-  refine _ ⬝ (proof !ap_compose'⁻¹ ⬝ ap_compose (ι f'') _ _ qed ◾ proof !seq_colim_functor_glue qed)⁻¹,
+  refine _ ⬝ (proof !ap_compose' ⬝ ap_compose (ι f'') _ _ qed ◾ proof !seq_colim_functor_glue qed)⁻¹,
   exact whisker_right _ !ap_con ⬝ !con.assoc
 end
 
@@ -355,7 +355,7 @@ definition seq_colim_over_equiv_glue {k : ℕ} (x : P (rep f k (f a))) :
   glue (seq_diagram_of_over g a) (rep_f f k a ▸o x) :=
 begin
   refine ap_compose (shift_down (seq_diagram_of_over g a)) _ _ ⬝ _,
-  exact ap02 _ !elim_glue ⬝ !ap_con ⬝ !ap_compose'⁻¹ ◾ !elim_glue
+  exact ap02 _ !elim_glue ⬝ !ap_con ⬝ !ap_compose' ◾ !elim_glue
 end
 
 variable {a}
@@ -578,7 +578,7 @@ begin
   induction v with x y,
   induction x with n a n a,
   { exact sigma_colim_rec_point g e w y },
-  { apply pi_pathover_left', intro x,
+  { apply pi_pathover_left, intro x,
     refine change_path (whisker_left _ !ap_inv ⬝ !con_inv_cancel_right)
       (_ ⬝o pathover_ap E (dpair _) (apd (sigma_colim_rec_point g e w) !seq_colim_over_glue⁻¹)),
     /- we can simplify the squareover we need to fill a bit if we apply this rule here -/
@@ -630,10 +630,10 @@ square (colim_sigma_of_sigma_colim_path1 g (g p)) (colim_sigma_of_sigma_colim_pa
     (glue (seq_diagram_of_over g (f a)) p)) :=
 begin
   refine !elim_glue ⬝ph _,
-  refine _ ⬝hp (ap_compose' (colim_sigma_of_sigma_colim_constructor g) _ _)⁻¹,
+  refine _ ⬝hp (ap_compose' (colim_sigma_of_sigma_colim_constructor g) _ _),
   refine _ ⬝hp ap02 _ !seq_colim_over_equiv_glue⁻¹,
   refine _ ⬝hp !ap_con⁻¹,
-  refine _ ⬝hp !ap_compose' ◾ !elim_glue⁻¹,
+  refine _ ⬝hp !ap_compose ◾ !elim_glue⁻¹,
   refine _ ⬝pv whisker_rt _ (natural_square0111 P (pathover_tro (rep_f f k a) p) g
                                                   (λn a p, glue (seq_diagram_sigma g) ⟨a, p⟩)),
   refine _ ⬝ whisker_left _ (ap02 _ !inv_inv⁻¹ ⬝ !ap_inv),
@@ -755,7 +755,7 @@ seq_colim_eq_equiv0' f a₀ a₁ ⬝e seq_colim_id_equiv_seq_colim_id0 f a₀ a
 
 definition seq_colim_eq_equiv {n : ℕ} (a₀ a₁ : A n) :
   ι f a₀ = ι f a₁ ≃ seq_colim (id_seq_diagram f n a₀ a₁) :=
-eq_equiv_fn_eq_of_equiv (kshift_equiv f n) (ι f a₀) (ι f a₁) ⬝e
+eq_equiv_fn_eq (kshift_equiv f n) (ι f a₀) (ι f a₁) ⬝e
 eq_equiv_eq_closed (incl_kshift_diag0 f a₀)⁻¹ (incl_kshift_diag0 f a₁)⁻¹ ⬝e
 seq_colim_eq_equiv0' (kshift_diag f n) a₀ a₁ ⬝e
 @seq_colim_equiv _ _ _ (λk, ap (@f _))
@@ -805,19 +805,19 @@ equiv.MK (seq_colim_trunc_of_trunc_seq_colim f k) (trunc_seq_colim_of_seq_colim_
     { induction x with a, reflexivity },
     { induction x with a, apply eq_pathover_id_right, apply hdeg_square,
       refine ap_compose (seq_colim_trunc_of_trunc_seq_colim f k) _ _ ⬝ ap02 _ !elim_glue ⬝ _,
-      refine !ap_compose'⁻¹ ⬝ !elim_glue ⬝ _, exact !idp_con }
+      refine !ap_compose' ⬝ !elim_glue ⬝ _, exact !idp_con }
   end end
   abstract begin
     intro x, induction x with x, induction x with n a n a,
     { reflexivity },
     { apply eq_pathover, apply hdeg_square,
       refine ap_compose (trunc_seq_colim_of_seq_colim_trunc f k) _ _ ⬝ ap02 _ !elim_glue ⬝ _,
-      refine !ap_compose'⁻¹ ⬝ !elim_glue }
+      refine !ap_compose' ⬝ !elim_glue }
   end end
 
 theorem is_conn_seq_colim [instance] (k : ℕ₋₂) [H : Πn, is_conn k (A n)] :
   is_conn k (seq_colim f) :=
-is_trunc_equiv_closed_rev -2 (trunc_seq_colim_equiv f k)
+is_trunc_equiv_closed_rev -2 (trunc_seq_colim_equiv f k) _
 
 /- the colimit of a sequence of fibers is the fiber of the functorial action of the colimit -/
 definition domain_seq_colim_functor {A A' : ℕ → Type} {f : seq_diagram A}
@@ -866,7 +866,7 @@ theorem is_trunc_fun_seq_colim_functor (k : ℕ₋₂) (H : Πn, is_trunc_fun k
   is_trunc_fun k (seq_colim_functor τ p) :=
 begin
   intro x, induction x using seq_colim.rec_prop,
-  exact is_trunc_equiv_closed_rev k (fiber_seq_colim_functor τ p a),
+  exact is_trunc_equiv_closed_rev k (fiber_seq_colim_functor τ p a) _
 end
 
 open is_conn
diff --git a/higher_groups.hlean b/higher_groups.hlean
index 1c959b6..afd5f22 100644
--- a/higher_groups.hlean
+++ b/higher_groups.hlean
@@ -64,7 +64,7 @@ open ωGType (renaming B→oB e→oe)
 lemma is_trunc_B' (G : [n;k]GType) : is_trunc (k+n) (B G) :=
 begin
   apply is_trunc_of_is_trunc_loopn,
-  exact is_trunc_equiv_closed _ (e G),
+  exact is_trunc_equiv_closed _ (e G) _,
   exact _
 end
 
@@ -96,7 +96,8 @@ sigma_equiv_of_is_embedding_left_contr
       assert lem : Π(A : n-Type*) (B : Type*) (H : is_trunc n B),
         (A ≃* B) ≃ (A ≃* (ptrunctype.mk B H pt)),
       { intro A B'' H, induction B'', reflexivity },
-      apply lem }
+      apply lem },
+    exact _
   end
   begin
     intro B' H, apply fiber.mk (ptruncconntype.mk B' (is_trunc_B (GType.mk H.1 B' H.2)) pt _),
@@ -107,7 +108,7 @@ definition GType_equiv_pequiv {n k : ℕ} (G : [n;k]GType) : GType_equiv n k G 
 by reflexivity
 
 definition GType_eq_equiv {n k : ℕ} (G H : [n;k]GType) : (G = H :> [n;k]GType) ≃ (B G ≃* B H) :=
-eq_equiv_fn_eq_of_equiv (GType_equiv n k) _ _ ⬝e !ptruncconntype_eq_equiv
+eq_equiv_fn_eq (GType_equiv n k) _ _ ⬝e !ptruncconntype_eq_equiv
 
 definition GType_eq {n k : ℕ} {G H : [n;k]GType} (e : B G ≃* B H) : G = H :=
 (GType_eq_equiv G H)⁻¹ᵉ e
@@ -127,13 +128,13 @@ end
 definition InfGType_equiv (k : ℕ) : [∞;k]GType ≃ Type*[k.-1] :=
 InfGType.sigma_char k ⬝e
 @sigma_equiv_of_is_contr_right _ _
-  (λX, is_trunc_equiv_closed_rev -2 (sigma_equiv_sigma_right (λB', !pType_eq_equiv⁻¹ᵉ)))
+  (λX, is_trunc_equiv_closed_rev -2 (sigma_equiv_sigma_right (λB', !pType_eq_equiv⁻¹ᵉ)) _)
 
 definition InfGType_equiv_pequiv {k : ℕ} (G : [∞;k]GType) : InfGType_equiv k G ≃* iB G :=
 by reflexivity
 
 definition InfGType_eq_equiv {k : ℕ} (G H : [∞;k]GType) : (G = H :> [∞;k]GType) ≃ (iB G ≃* iB H) :=
-eq_equiv_fn_eq_of_equiv (InfGType_equiv k) _ _ ⬝e !pconntype_eq_equiv
+eq_equiv_fn_eq (InfGType_equiv k) _ _ ⬝e !pconntype_eq_equiv
 
 definition InfGType_eq {k : ℕ} {G H : [∞;k]GType} (e : iB G ≃* iB H) : G = H :=
 (InfGType_eq_equiv G H)⁻¹ᵉ e
@@ -293,7 +294,7 @@ begin
   { have k ≥ succ n, from le_of_succ_le_succ H,
     assert this : n + succ k ≤ 2 * k,
     { rewrite [two_mul, add_succ, -succ_add], exact nat.add_le_add_right this k },
-    exact freudenthal_pequiv (B G) this }
+    exact freudenthal_pequiv this (B G) }
 end⁻¹ᵉ* ⬝e*
 ptrunc_pequiv (n + k) _
 
@@ -434,6 +435,7 @@ equivalence.trans !pb_Precategory_equivalence_of_equiv
                   (equivalence.trans (equivalence.symm (AbGrp_equivalence_cptruncconntype' k))
                     proof equivalence.refl _ qed)
 
+/-
 print axioms GType_equiv
 print axioms InfGType_equiv
 print axioms Decat_adjoint_Disc
@@ -448,5 +450,6 @@ print axioms stabilization
 print axioms is_trunc_GType
 print axioms cGType_equivalence_Grp
 print axioms cGType_equivalence_AbGrp
+-/
 
 end higher_group
diff --git a/homotopy/EM.hlean b/homotopy/EM.hlean
index 9b3cec4..ca703d0 100644
--- a/homotopy/EM.hlean
+++ b/homotopy/EM.hlean
@@ -169,7 +169,7 @@ namespace EM
   end
 
   definition loopn_EMadd1_pequiv_EM1_succ (G : AbGroup) (n : ℕ) :
-    loopn_EMadd1_pequiv_EM1 G (succ n) ~* (loopn_succ_in (EMadd1 G (succ n)) n)⁻¹ᵉ* ∘*
+    loopn_EMadd1_pequiv_EM1 G (succ n) ~* (loopn_succ_in n (EMadd1 G (succ n)))⁻¹ᵉ* ∘*
       Ω→[n] (loop_EMadd1 G n) ∘* loopn_EMadd1_pequiv_EM1 G n :=
   by reflexivity
 
@@ -178,7 +178,7 @@ namespace EM
 
   definition loop_EMadd1_succ (G : AbGroup) (n : ℕ) :
     loop_EMadd1 G (n+1) ~* (loop_ptrunc_pequiv (n+1+1) (susp (EMadd1 G (n+1))))⁻¹ᵉ* ∘*
-    freudenthal_pequiv (EMadd1 G (n+1)) (add_mul_le_mul_add n 1 1) ∘*
+    freudenthal_pequiv (add_mul_le_mul_add n 1 1) (EMadd1 G (n+1)) ∘*
     (ptrunc_pequiv (n+1+1) (EMadd1 G (n+1)))⁻¹ᵉ* :=
   by reflexivity
 
@@ -333,7 +333,7 @@ namespace EM
     { exact π→g[n+2] },
     { exact λφ, (EMadd1_pequiv_type Y n ∘* EMadd1_functor φ (n+1)) ∘* (EMadd1_pequiv_type X n)⁻¹ᵉ* },
     { intro φ, apply homomorphism_eq,
-      refine homotopy_group_functor_compose (n+2) _ _ ⬝hty _, exact sorry }, -- easy but tedious
+      refine homotopy_group_functor_pcompose (n+2) _ _ ⬝hty _, exact sorry }, -- easy but tedious
     { intro f, apply eq_of_phomotopy, refine (phomotopy_pinv_right_of_phomotopy _)⁻¹*,
       apply EMadd1_pequiv_type_natural }
   end
@@ -504,14 +504,14 @@ namespace EM
     (λX, πg[1] X)
     (λX Y f, π→g[1] f)
     begin intro, apply homomorphism_eq, exact to_homotopy !homotopy_group_functor_pid end
-    begin intros, apply homomorphism_eq, exact to_homotopy !homotopy_group_functor_compose end
+    begin intros, apply homomorphism_eq, exact to_homotopy !homotopy_group_functor_pcompose end
 
   definition ab_homotopy_group_cfunctor (n : ℕ) : cType*[n.+1] ⇒ AbGrp :=
   functor.mk
     (λX, πag[n+2] X)
     (λX Y f, π→g[n+2] f)
     begin intro, apply homomorphism_eq, exact to_homotopy !homotopy_group_functor_pid end
-    begin intros, apply homomorphism_eq, exact to_homotopy !homotopy_group_functor_compose end
+    begin intros, apply homomorphism_eq, exact to_homotopy !homotopy_group_functor_pcompose end
 
   definition is_equivalence_EM1_cfunctor : is_equivalence EM1_cfunctor.{u} :=
   begin
@@ -576,7 +576,7 @@ namespace EM
       !fundamental_group_EM1,
     exact homotopy_group_isomorphism_of_pequiv 0 e,
     refine is_trunc_of_is_trunc_loopn n 1 X _ (@is_conn_of_is_conn_succ _ _ H1),
-    apply is_trunc_equiv_closed_rev 1 e
+    exact is_trunc_equiv_closed_rev 1 e _
   end
 
   definition EM1_pequiv_EM1 {G H : Group} (φ : G ≃g H) : EM1 G ≃* EM1 H :=
@@ -588,7 +588,7 @@ namespace EM
 
   definition is_contr_EM1 {G : Group} (H : is_contr G) : is_contr (EM1 G) :=
   is_contr_of_is_conn_of_is_trunc
-    (is_trunc_succ_succ_of_is_trunc_loop _ _ (is_trunc_equiv_closed _ !loop_EM1) _) !is_conn_EM1
+    (is_trunc_succ_succ_of_is_trunc_loop _ _ (is_trunc_equiv_closed _ !loop_EM1 _) _) !is_conn_EM1
 
   definition is_contr_EMadd1 (n : ℕ) {G : AbGroup} (H : is_contr G) : is_contr (EMadd1 G n) :=
   begin
@@ -675,7 +675,7 @@ namespace EM
     induction H with n,
     have H2 : is_exact (π→g[n+1] (ppoint f)) (π→g[n+1] f),
     from is_exact_of_is_exact_at (is_exact_LES_of_homotopy_groups f (n+1, 0)),
-    have H3 : is_exact (π→g[n+1] (boundary_map f) ∘g ghomotopy_group_succ_in Y n)
+    have H3 : is_exact (π→g[n+1] (boundary_map f) ∘g ghomotopy_group_succ_in n Y)
       (π→g[n+1] (ppoint f)),
     from is_exact_of_is_exact_at (is_exact_LES_of_homotopy_groups f (n+1, 1)),
     exact isomorphism_kernel_of_is_exact H3 H2 H1
diff --git a/homotopy/degree.hlean b/homotopy/degree.hlean
index 9f4ece2..5883237 100644
--- a/homotopy/degree.hlean
+++ b/homotopy/degree.hlean
@@ -123,7 +123,7 @@ namespace sphere
     deg (g ∘* f) = deg g *[ℤ] deg f :=
   begin
     induction H with n,
-    refine ap (πnSn (n+1)) (homotopy_group_functor_compose (succ n) g f (tr surf)) ⬝ _,
+    refine ap (πnSn (n+1)) (homotopy_group_functor_pcompose (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 c249aa2..416e387 100644
--- a/homotopy/fwedge.hlean
+++ b/homotopy/fwedge.hlean
@@ -151,7 +151,7 @@ namespace fwedge
 
   definition wedge_pmap_equiv  [constructor] (A B X : Type*) :
     ((A ∨ B) →* X) ≃ ((A →* X) × (B →* X)) :=
-    calc (A ∨ B) →* X ≃ ⋁(bool.rec A B) →* X : by exact pequiv_ppcompose_right (wedge_pequiv_fwedge A B)⁻¹ᵉ*
+    calc (A ∨ B) →* X ≃ ⋁(bool.rec A B) →* X : by exact ppmap_pequiv_ppmap_left (wedge_pequiv_fwedge A B)⁻¹ᵉ*
             ...       ≃ Πi, (bool.rec A B) i →* X : by exact fwedge_pmap_equiv (bool.rec A B) X
             ...       ≃  (A →* X) × (B →* X) : by exact pi_bool_left (λ i, bool.rec A B i →* X)
 
@@ -212,7 +212,7 @@ namespace fwedge
 
 -- hsquare 3:
   definition fwedge_to_wedge_nat_square {A B X Y : Type*} (f : X →* Y) :
-        hsquare (pequiv_ppcompose_right (wedge_pequiv_fwedge A B)) (pequiv_ppcompose_right (wedge_pequiv_fwedge A B)) (pcompose f) (pcompose f) :=
+        hsquare (ppmap_pequiv_ppmap_left (wedge_pequiv_fwedge A B)) (ppmap_pequiv_ppmap_left (wedge_pequiv_fwedge A B)) (pcompose f) (pcompose f) :=
   begin
     exact sorry
   end
diff --git a/homotopy/join_theorem.hlean b/homotopy/join_theorem.hlean
index 6185190..fdbc4b7 100644
--- a/homotopy/join_theorem.hlean
+++ b/homotopy/join_theorem.hlean
@@ -74,7 +74,7 @@ begin
   apply is_retraction_of_is_equiv,
   apply is_equiv_of_is_contr_fun,
   intro f,
-  refine is_contr_equiv_closed _,
+  refine is_contr_equiv_closed _ _,
   {exact unit},
   symmetry,
   exact sorry
diff --git a/homotopy/pushout.hlean b/homotopy/pushout.hlean
index 2d4759f..40182b3 100644
--- a/homotopy/pushout.hlean
+++ b/homotopy/pushout.hlean
@@ -98,7 +98,7 @@ namespace pushout
 
 },
     { apply ap10,
-      apply eq_of_fn_eq_fn (equiv.mk _ (H D)),
+      apply inj (equiv.mk _ (H D)),
       fapply sigma_eq,
       { esimp, fapply prod_eq,
           apply eq_of_homotopy, intro b,
@@ -128,9 +128,9 @@ namespace pushout
 --     { intro x, exact sorry
 
 -- },
---     { intro d, apply eq_of_fn_eq_fn (equiv_lift D), esimp, revert d,
+--     { intro d, apply inj (equiv_lift D), esimp, revert d,
 --       apply ap10,
---       apply eq_of_fn_eq_fn (equiv.mk _ (H (lift.{_ (max u₁ u₂ u₃)} D))),
+--       apply inj (equiv.mk _ (H (lift.{_ (max u₁ u₂ u₃)} D))),
 --       fapply sigma_eq,
 --       { esimp, fapply prod_eq,
 --           apply eq_of_homotopy, intro b, apply ap up, esimp,
@@ -183,7 +183,7 @@ namespace pushout
       { reflexivity },
       { apply eq_pathover_id_right, apply hdeg_square,
         refine ap_compose pushout_vcompose_to _ _ ⬝ ap02 _ !elim_glue ⬝ _,
-        refine !ap_con ⬝ !elim_glue ◾ !ap_compose'⁻¹ ⬝ !idp_con ⬝ _, esimp, apply elim_glue }},
+        refine !ap_con ⬝ !elim_glue ◾ !ap_compose' ⬝ !idp_con ⬝ _, esimp, apply elim_glue }},
     { intro x, induction x with d y b,
       { reflexivity },
       { induction y with b c a,
@@ -281,10 +281,10 @@ namespace pushout
     { reflexivity },
     { reflexivity },
     { apply eq_pathover, apply hdeg_square, esimp,
-      refine !elim_glue ⬝ whisker_right _ (!ap_con ⬝ !ap_compose'⁻¹ ◾ idp) ◾
-        (ap02 _ !con_inv ⬝ !ap_con ⬝ whisker_left _ (ap02 _ !ap_inv⁻¹ ⬝ !ap_compose'⁻¹)) ⬝ _ ⬝
+      refine !elim_glue ⬝ whisker_right _ (!ap_con ⬝ !ap_compose' ◾ idp) ◾
+        (ap02 _ !con_inv ⬝ !ap_con ⬝ whisker_left _ (ap02 _ !ap_inv⁻¹ ⬝ !ap_compose')) ⬝ _ ⬝
         (ap_compose (pushout.functor h₂ i₂ j₂ p₂ q₂) _ _ ⬝ ap02 _ !elim_glue)⁻¹,
-      refine _ ⬝ (!ap_con ⬝ (!ap_con ⬝ !ap_compose'⁻¹ ◾ !elim_glue) ◾ !ap_compose'⁻¹)⁻¹ᵖ,
+      refine _ ⬝ (!ap_con ⬝ (!ap_con ⬝ !ap_compose' ◾ !elim_glue) ◾ !ap_compose')⁻¹ᵖ,
       refine !con.assoc⁻¹ ⬝ whisker_right _ _,
       exact whisker_right _ !con.assoc ⬝ !con.assoc }
   end
@@ -512,7 +512,7 @@ equiv.MK sum_pushout_of_pushout_sum pushout_sum_of_sum_pushout
     { apply eq_pathover_id_right,
       refine ap_compose pushout_sum_of_sum_pushout _ _ ⬝ ap02 _ !elim_glue ⬝ph _,
       induction a with a a':
-        (apply hdeg_square; refine !ap_compose'⁻¹ ⬝ !elim_glue ⬝ !con_idp ⬝ !idp_con) }
+        (apply hdeg_square; refine !ap_compose' ⬝ !elim_glue ⬝ !con_idp ⬝ !idp_con) }
   end end
 
 variables {f g f' g'}
@@ -534,7 +534,7 @@ begin
   { induction c with c c': reflexivity },
   { exact abstract begin apply eq_pathover,
     refine !ap_compose ⬝ ap02 _ !elim_glue ⬝ph _,
-    induction a with a a': exact hdeg_square (!ap_compose'⁻¹ ⬝ !elim_glue ⬝ !elim_glue⁻¹)
+    induction a with a a': exact hdeg_square (!ap_compose' ⬝ !elim_glue ⬝ !elim_glue⁻¹)
     end end }
 end
 
@@ -551,13 +551,13 @@ begin
   { induction c with c c': reflexivity },
   { exact abstract begin apply eq_pathover,
     refine !ap_compose ⬝ ap02 _ !elim_glue ⬝ph _ ⬝hp (!ap_compose ⬝ ap02 _ !elim_glue)⁻¹,
-    refine !ap_con ⬝ (!ap_con ⬝ !ap_compose'⁻¹ ◾ !elim_glue) ◾ (!ap_compose'⁻¹ ⬝ !ap_inv) ⬝ph _,
+    refine !ap_con ⬝ (!ap_con ⬝ !ap_compose' ◾ !elim_glue) ◾ (!ap_compose' ⬝ !ap_inv) ⬝ph _,
     induction a with a a',
-    { apply hdeg_square, refine !ap_compose'⁻¹ ◾ idp ◾ !ap_compose'⁻¹⁻² ⬝ _ ⬝ !ap_compose',
+    { apply hdeg_square, refine !ap_compose' ◾ idp ◾ !ap_compose'⁻² ⬝ _ ⬝ !ap_compose'⁻¹,
       refine _ ⬝ (ap_compose sum.inl _ _ ⬝ ap02 _ !elim_glue)⁻¹,
       exact (ap_compose sum.inl _ _ ◾ idp ⬝ !ap_con⁻¹) ◾ (!ap_inv⁻¹ ⬝ ap_compose sum.inl _ _) ⬝
         !ap_con⁻¹ },
-    { apply hdeg_square, refine !ap_compose'⁻¹ ◾ idp ◾ !ap_compose'⁻¹⁻² ⬝ _ ⬝ !ap_compose',
+    { apply hdeg_square, refine !ap_compose' ◾ idp ◾ !ap_compose'⁻² ⬝ _ ⬝ !ap_compose'⁻¹,
       refine _ ⬝ (ap_compose sum.inr _ _ ⬝ ap02 _ !elim_glue)⁻¹,
       exact (ap_compose sum.inr _ _ ◾ idp ⬝ !ap_con⁻¹) ◾ (!ap_inv⁻¹ ⬝ ap_compose sum.inr _ _) ⬝
         !ap_con⁻¹ } end end }
@@ -600,7 +600,7 @@ equiv.MK sigma_pushout_of_pushout_sigma pushout_sigma_of_sigma_pushout
     { apply eq_pathover_id_right,
       refine ap_compose pushout_sigma_of_sigma_pushout _ _ ⬝ ap02 _ !elim_glue ⬝ph _,
       induction a with a a',
-        apply hdeg_square, refine !ap_compose'⁻¹ ⬝ !elim_glue ⬝ !con_idp ⬝ !idp_con }
+        apply hdeg_square, refine !ap_compose' ⬝ !elim_glue ⬝ !con_idp ⬝ !idp_con }
   end end
 
 variables {f g}
@@ -621,12 +621,14 @@ begin
   { reflexivity },
   { exact abstract begin apply eq_pathover, apply hdeg_square,
     refine !ap_compose ⬝ ap02 _ !elim_glue ⬝ !ap_con ⬝
-      (!ap_con ⬝ (!ap_compose'⁻¹ ⬝ !ap_compose'⁻¹) ◾ !elim_glue) ◾
-      (!ap_compose'⁻¹ ⬝ ap02 _ !ap_inv⁻¹ ⬝ !ap_compose'⁻¹) ⬝ _,
-    exact
-      (ap_compose (sigma_functor s (λ x, pushout.functor (h₁ x) (h₂ x) (h₃ x) (p x) (q x))) _ _ ⬝
-      ap02 _ !elim_glue ⬝ !ap_compose'⁻¹ ⬝ ap_compose (dpair _) _ _ ⬝ ap02 _ !elim_glue ⬝
-      !ap_con ⬝ (!ap_con ⬝ !ap_compose'⁻¹ ◾ idp) ◾ !ap_compose'⁻¹)⁻¹ end end }
+      (!ap_con ⬝ (!ap_compose' ⬝ !ap_compose') ◾ !elim_glue) ◾
+      (!ap_compose' ⬝ ap02 _ !ap_inv⁻¹ ⬝ !ap_compose') ⬝ _,
+    symmetry,
+    refine
+      ap_compose (sigma_functor s (λ x, pushout.functor (h₁ x) (h₂ x) (h₃ x) (p x) (q x))) _ _ ⬝
+      ap02 _ !elim_glue ⬝ !ap_compose' ⬝ ap_compose (dpair _) _ _ ⬝ _,
+    exact ap02 _ !elim_glue ⬝ !ap_con ⬝ (!ap_con ⬝ !ap_compose' ◾ idp) ◾ !ap_compose'
+end end }
 end
 
 
@@ -696,7 +698,7 @@ end
     fapply phomotopy.mk,
     { intro y, reflexivity },
     { esimp, refine !idp_con ⬝ _,
-      refine _ ⬝ (!ap_con ⬝ (!ap_compose'⁻¹ ⬝ !ap_inv) ◾ !elim_glue)⁻¹,
+      refine _ ⬝ (!ap_con ⬝ (!ap_compose' ⬝ !ap_inv) ◾ !elim_glue)⁻¹,
       apply eq_inv_con_of_con_eq, exact (to_homotopy_pt p)⁻¹ }
   end
 
@@ -807,7 +809,7 @@ namespace pushout
     begin intro x, induction x: reflexivity end begin intro x, induction x: reflexivity end
 
   definition quotient_equiv_pushout_natural :
-    hsquare (quotient.functor _ _ f k) (pushout_quotient_functor f k)
+    hsquare (quotient.functor f k) (pushout_quotient_functor f k)
       (quotient_equiv_pushout R) (quotient_equiv_pushout Q) :=
   begin
     intro x, induction x with a a a' r,
diff --git a/homotopy/realprojective.hlean b/homotopy/realprojective.hlean
index d8f1688..8f1c29e 100644
--- a/homotopy/realprojective.hlean
+++ b/homotopy/realprojective.hlean
@@ -56,7 +56,7 @@ calc (⟨e, p⟩ = ⟨f, q⟩)
     ≃ Σ (h : e = f), h ▸ p = q   : sigma_eq_equiv'
 ... ≃ Σ (h : e ~ f), p = h a ⬝ q :
 begin
-  apply sigma_equiv_sigma ((equiv_eq_char e f) ⬝e eq_equiv_homotopy),
+  apply sigma_equiv_sigma ((equiv_eq_char e f) ⬝e !eq_equiv_homotopy),
   intro h, induction h, esimp, change (p = q) ≃ (p = idp ⬝ q),
   rewrite idp_con
 end
@@ -84,7 +84,7 @@ definition BoolType.eq_equiv_equiv (A B : BoolType)
   : (A = B) ≃ (A ≃ B) :=
 calc (A = B)
     ≃ (BoolType.sigma_char A = BoolType.sigma_char B)
-    : eq_equiv_fn_eq_of_equiv
+    : eq_equiv_fn_eq
 ... ≃ (BoolType.carrier A = BoolType.carrier B)
     : begin
         induction A with A p, induction B with B q,
@@ -109,7 +109,7 @@ definition theorem_II_2_lemma_1 (e : bool ≃ bool)
 sum.elim (dichotomy (e ff)) (λ q, q)
 begin
   intro q, apply empty.elim, apply ff_ne_tt,
-  apply to_inv (eq_equiv_fn_eq_of_equiv e ff tt),
+  apply to_inv (eq_equiv_fn_eq e ff tt),
   exact q ⬝ p⁻¹,
 end
 
@@ -118,7 +118,7 @@ definition theorem_II_2_lemma_2 (e : bool ≃ bool)
 sum.elim (dichotomy (e ff))
 begin
   intro q, apply empty.elim, apply ff_ne_tt,
-  apply to_inv (eq_equiv_fn_eq_of_equiv e ff tt),
+  apply to_inv (eq_equiv_fn_eq e ff tt),
   exact q ⬝ p⁻¹
 end
 begin
diff --git a/homotopy/smash.hlean b/homotopy/smash.hlean
index bd03efc..c04d57e 100644
--- a/homotopy/smash.hlean
+++ b/homotopy/smash.hlean
@@ -1107,10 +1107,10 @@ namespace smash
     { reflexivity },
     { reflexivity },
     { apply eq_pathover_id_right,
-      refine ap_compose' smash_flip' _ _ ⬝ ap02 _ !elim_gluel ⬝ !elim_gluer ⬝ph _,
+      refine ap_compose smash_flip' _ _ ⬝ ap02 _ !elim_gluel ⬝ !elim_gluer ⬝ph _,
       apply hrfl },
     { apply eq_pathover_id_right,
-      refine ap_compose' smash_flip' _ _ ⬝ ap02 _ !elim_gluer ⬝ !elim_gluel ⬝ph _,
+      refine ap_compose smash_flip' _ _ ⬝ ap02 _ !elim_gluer ⬝ !elim_gluel ⬝ph _,
       apply hrfl }
   end
 
@@ -1137,13 +1137,13 @@ namespace smash
     { reflexivity },
     { reflexivity },
     { apply eq_pathover,
-      refine ap_compose' (smash_functor' _ _)  _ _ ⬝ ap02 _ !elim_gluel ⬝ !functor_gluer ⬝ph _
-        ⬝hp (ap_compose' smash_flip' _ _ ⬝ ap02 _ !functor_gluel)⁻¹ᵖ,
-      refine _ ⬝hp (!ap_con ⬝ !ap_compose'⁻¹ ◾ !elim_gluel)⁻¹, exact hrfl },
+      refine ap_compose (smash_functor' _ _)  _ _ ⬝ ap02 _ !elim_gluel ⬝ !functor_gluer ⬝ph _
+        ⬝hp (ap_compose smash_flip' _ _ ⬝ ap02 _ !functor_gluel)⁻¹ᵖ,
+      refine _ ⬝hp (!ap_con ⬝ !ap_compose' ◾ !elim_gluel)⁻¹, exact hrfl },
     { apply eq_pathover,
-      refine ap_compose' (smash_functor' _ _)  _ _ ⬝ ap02 _ !elim_gluer ⬝ !functor_gluel ⬝ph _
-        ⬝hp (ap_compose' smash_flip' _ _ ⬝ ap02 _ !functor_gluer)⁻¹ᵖ,
-      refine _ ⬝hp (!ap_con ⬝ !ap_compose'⁻¹ ◾ !elim_gluer)⁻¹, exact hrfl },
+      refine ap_compose (smash_functor' _ _)  _ _ ⬝ ap02 _ !elim_gluer ⬝ !functor_gluel ⬝ph _
+        ⬝hp (ap_compose smash_flip' _ _ ⬝ ap02 _ !functor_gluer)⁻¹ᵖ,
+      refine _ ⬝hp (!ap_con ⬝ !ap_compose' ◾ !elim_gluer)⁻¹, exact hrfl },
   end
 
   definition smash_flip_smash_functor (f : A →* C) (g : B →* D) :
diff --git a/homotopy/smash_adjoint.hlean b/homotopy/smash_adjoint.hlean
index 1a47c44..a82cbb2 100644
--- a/homotopy/smash_adjoint.hlean
+++ b/homotopy/smash_adjoint.hlean
@@ -135,17 +135,17 @@ namespace smash
       { apply eq_pathover,
         refine ap_compose (smash_pmap_counit B C') _ _ ⬝ph _ ⬝hp (ap_compose g _ _)⁻¹,
         refine ap02 _ !functor_gluel ⬝ph _ ⬝hp ap02 _ !elim_gluel⁻¹,
-        refine !ap_con ⬝ !ap_compose'⁻¹ ◾ !elim_gluel ⬝ph _,
+        refine !ap_con ⬝ !ap_compose' ◾ !elim_gluel ⬝ph _,
         refine !idp_con ⬝ph _, apply square_of_eq,
         refine !idp_con ⬝ !con_inv_cancel_right⁻¹ },
       { apply eq_pathover,
         refine ap_compose (smash_pmap_counit B C') _ _ ⬝ph _ ⬝hp (ap_compose g _ _)⁻¹,
         refine ap02 _ !functor_gluer ⬝ph _ ⬝hp ap02 _ !elim_gluer⁻¹,
-        refine !ap_con ⬝ !ap_compose'⁻¹ ◾ !elim_gluer ⬝ph _⁻¹ʰ,
+        refine !ap_con ⬝ !ap_compose' ◾ !elim_gluer ⬝ph _⁻¹ʰ,
         apply square_of_eq_bot, refine !idp_con ⬝ _,
         induction C' with C' c₀', induction g with g g₀, esimp at *,
         induction g₀, refine ap02 _ !eq_of_phomotopy_refl }},
-    { refine !idp_con ⬝ !idp_con ⬝ _, refine _ ⬝ !ap_compose',
+    { refine !idp_con ⬝ !idp_con ⬝ _, refine _ ⬝ !ap_compose,
       refine _ ⬝ (ap_is_constant respect_pt _)⁻¹, refine !idp_con⁻¹ }
   end
 
@@ -160,16 +160,16 @@ namespace smash
       { reflexivity },
       { apply eq_pathover, apply hdeg_square,
         refine ap_compose !smash_pmap_counit _ _ ⬝ ap02 _ !elim_gluel ⬝ !ap_con ⬝
-          !ap_compose'⁻¹ ◾ !elim_gluel ⬝ _,
+          !ap_compose' ◾ !elim_gluel ⬝ _,
         refine (ap_compose !smash_pmap_counit _ _ ⬝ ap02 _ !elim_gluel ⬝ !ap_con ⬝
-          !ap_compose'⁻¹ ◾ !elim_gluel ⬝ !idp_con)⁻¹ },
+          !ap_compose' ◾ !elim_gluel ⬝ !idp_con)⁻¹ },
       { apply eq_pathover, apply hdeg_square,
         refine ap_compose !smash_pmap_counit _ _ ⬝ ap02 _ (!elim_gluer ⬝ !idp_con) ⬝
           !elim_gluer ⬝ _,
         refine (ap_compose !smash_pmap_counit _ _ ⬝ ap02 _ !elim_gluer ⬝ !ap_con ⬝
-          !ap_compose'⁻¹ ◾ !elim_gluer ⬝ !con_idp ⬝ _)⁻¹,
+          !ap_compose' ◾ !elim_gluer ⬝ !con_idp ⬝ _)⁻¹,
         refine !to_fun_eq_of_phomotopy ⬝ _, reflexivity }},
-    { refine !idp_con ⬝ _, refine !ap_compose'⁻¹ ⬝ _ ⬝ !ap_ap011⁻¹, esimp,
+    { refine !idp_con ⬝ _, refine !ap_compose' ⬝ _ ⬝ !ap_ap011⁻¹, esimp,
       refine !to_fun_eq_of_phomotopy ⬝ _, exact !ap_constant⁻¹ }
   end
 
@@ -185,15 +185,15 @@ namespace smash
       { exact gluer pt },
       { apply eq_pathover_id_right,
         refine ap_compose smash_pmap_counit_map _ _ ⬝ ap02 _ !functor_gluel ⬝ph _,
-        refine !ap_con ⬝ !ap_compose'⁻¹ ◾ !elim_gluel ⬝ph _,
+        refine !ap_con ⬝ !ap_compose' ◾ !elim_gluel ⬝ph _,
         refine !idp_con ⬝ph _,
         apply square_of_eq, refine !idp_con ⬝ !inv_con_cancel_right⁻¹ },
       { apply eq_pathover_id_right,
         refine ap_compose smash_pmap_counit_map _ _ ⬝ ap02 _ !functor_gluer ⬝ph _,
-        refine !ap_con ⬝ !ap_compose'⁻¹ ◾ !elim_gluer ⬝ph _,
+        refine !ap_con ⬝ !ap_compose' ◾ !elim_gluer ⬝ph _,
         refine !ap_eq_of_phomotopy ⬝ph _,
         apply square_of_eq, refine !idp_con ⬝ !inv_con_cancel_right⁻¹ }},
-    { refine _ ⬝ !ap_compose', refine _ ⬝ (ap_is_constant respect_pt _)⁻¹,
+    { refine _ ⬝ !ap_compose, refine _ ⬝ (ap_is_constant respect_pt _)⁻¹,
          rexact (con.right_inv (gluel pt))⁻¹ }
   end
 
@@ -431,7 +431,7 @@ namespace smash
   calc
     ppmap (A ∧ (B ∧ C)) X
         ≃* ppmap A (ppmap (B ∧ C) X)     : smash_adjoint_pmap A (B ∧ C) X
-    ... ≃* ppmap A (ppmap B (ppmap C X)) : pequiv_ppcompose_left (smash_adjoint_pmap B C X)
+    ... ≃* ppmap A (ppmap B (ppmap C X)) : ppmap_pequiv_ppmap_right (smash_adjoint_pmap B C X)
     ... ≃* ppmap (A ∧ B) (ppmap C X)     : smash_adjoint_pmap_inv A B (ppmap C X)
     ... ≃* ppmap ((A ∧ B) ∧ C) X         : smash_adjoint_pmap_inv (A ∧ B) C X
 
@@ -517,7 +517,7 @@ namespace smash
     ppmap (D ∧ (A ∧ (B ∧ C))) X ≃* ppmap (D ∧ ((A ∧ B) ∧ C)) X :=
   calc     ppmap (D ∧ (A ∧ (B ∧ C))) X
         ≃* ppmap D (ppmap (A ∧ (B ∧ C)) X) : smash_adjoint_pmap D (A ∧ (B ∧ C)) X
-    ... ≃* ppmap D (ppmap ((A ∧ B) ∧ C) X) : pequiv_ppcompose_left (smash_assoc_elim_pequiv A B C X)
+    ... ≃* ppmap D (ppmap ((A ∧ B) ∧ C) X) : ppmap_pequiv_ppmap_right (smash_assoc_elim_pequiv A B C X)
     ... ≃* ppmap (D ∧ ((A ∧ B) ∧ C)) X     : smash_adjoint_pmap_inv D ((A ∧ B) ∧ C) X
 
   definition smash_assoc_elim_right_pequiv (A B C D X : Type*) :
@@ -595,7 +595,7 @@ namespace smash
   calc
     ppmap (⅀ A ∧ B) X ≃* ppmap (⅀ A) (ppmap B X) : smash_adjoint_pmap (⅀ A) B X
     ... ≃* ppmap A (Ω (ppmap B X)) : susp_adjoint_loop A (ppmap B X)
-    ... ≃* ppmap A (ppmap B (Ω X)) : pequiv_ppcompose_left (loop_ppmap_commute B X)
+    ... ≃* ppmap A (ppmap B (Ω X)) : ppmap_pequiv_ppmap_right (loop_ppmap_commute B X)
     ... ≃* ppmap (A ∧ B) (Ω X) : smash_adjoint_pmap A B (Ω X)
     ... ≃* ppmap (⅀ (A ∧ B)) X : susp_adjoint_loop (A ∧ B) X
 
diff --git a/homotopy/susp.hlean b/homotopy/susp.hlean
index 285653a..248799d 100644
--- a/homotopy/susp.hlean
+++ b/homotopy/susp.hlean
@@ -159,7 +159,7 @@ sorry
         esimp, induction q, esimp, krewrite prod_transport, fapply sigma_eq,
         { exact idp },
         { esimp, rewrite eq_transport_Fl, rewrite eq_transport_Fl,
-          krewrite elim_glue, krewrite (ap_compose' pr1 prod_of_wedge (glue star)),
+          krewrite elim_glue, krewrite [-ap_compose' pr1 prod_of_wedge (glue star)],
           krewrite elim_glue, esimp, apply eq_pathover, rewrite idp_con, esimp,
           apply square_of_eq, rewrite [idp_con,idp_con,inv_inv] } }
     end
diff --git a/homotopy/wedge.hlean b/homotopy/wedge.hlean
index 9933f3c..046d60a 100644
--- a/homotopy/wedge.hlean
+++ b/homotopy/wedge.hlean
@@ -140,7 +140,7 @@ begin
   { induction v with p x, exact fiber.mk (inl x) p },
   { exact fiber.mk (inr pt) idp },
   { esimp, apply fiber_eq (wedge.glue ⬝ ap inr p), symmetry,
-      refine !ap_con ⬝ !wedge.elim_glue ◾ (!ap_compose'⁻¹ ⬝ !ap_id) ⬝ !idp_con }
+      refine !ap_con ⬝ !wedge.elim_glue ◾ (!ap_compose' ⬝ !ap_id) ⬝ !idp_con }
 end
 
 variables (X Y)
@@ -164,7 +164,7 @@ pmap.mk pfiber_wedge_pr2_of_pcofiber_pprod_incl1'
 --   begin
 --     fapply phomotopy.mk,
 --     { intro p, apply fiber_eq (wedge.glue ⬝ ap inr p ⬝ wedge.glue⁻¹), symmetry,
---       refine !ap_con ⬝ (!ap_con ⬝ !wedge.elim_glue ◾ (!ap_compose'⁻¹ ⬝ !ap_id)) ◾
+--       refine !ap_con ⬝ (!ap_con ⬝ !wedge.elim_glue ◾ (!ap_compose' ⬝ !ap_id)) ◾
 --         (!ap_inv ⬝ !wedge.elim_glue⁻²) ⬝ _, exact idp_con p },
 --     { esimp, refine fiber_eq2 (con.right_inv wedge.glue) _ ⬝ !fiber_eq_eta⁻¹,
 --       rewrite [idp_con, ↑fiber_eq_pr2, con2_idp, whisker_right_idp, whisker_right_idp],
@@ -186,8 +186,8 @@ pequiv.MK (pcofiber_pprod_incl1_of_pfiber_wedge_pr2 _ _)
     fapply phomotopy.mk,
     { intro x, esimp, induction x with x p,  induction x with x y,
       { reflexivity },
-      { refine (fiber_eq (ap inr p) _)⁻¹, refine !ap_id⁻¹ ⬝ !ap_compose' },
-      { apply @pi_pathover_right' _ _ _ _ (λ(xp : Σ(x : X ∨ Y), pppi.to_fun (wedge_pr2 X Y) x = pt),
+      { refine (fiber_eq (ap inr p) _)⁻¹, refine !ap_id⁻¹ ⬝ !ap_compose },
+      { apply @pi_pathover_right _ _ _ _ (λ(xp : Σ(x : X ∨ Y), pppi.to_fun (wedge_pr2 X Y) x = pt),
           pfiber_wedge_pr2_of_pcofiber_pprod_incl1'
           (pcofiber_pprod_incl1_of_pfiber_wedge_pr2' (mk xp.1 xp.2)) = mk xp.1 xp.2),
         intro p, apply eq_pathover, exact sorry }},
diff --git a/move_to_lib.hlean b/move_to_lib.hlean
index 37ead01..55eb11f 100644
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@@ -329,7 +329,7 @@ end
   definition trunc_isomorphism_of_equiv {A B : Type} [inf_group A] [inf_group B] (f : A ≃ B)
     (h : is_mul_hom f) : Group.mk (trunc 0 A) (trunc_group A) ≃g Group.mk (trunc 0 B) (trunc_group B) :=
   begin
-    apply isomorphism_of_equiv (equiv.mk (trunc_functor 0 f) (is_equiv_trunc_functor 0 f)), intros x x',
+    apply isomorphism_of_equiv (trunc_equiv_trunc 0 f), intros x x',
     induction x with a, induction x' with a', apply ap tr, exact h a a'
   end
 
@@ -425,7 +425,7 @@ end
   definition to_ginv_inf [constructor] (φ : G₁ ≃∞g G₂) : G₂ →∞g G₁ :=
   inf_homomorphism.mk φ⁻¹
     abstract begin
-    intro g₁ g₂, apply eq_of_fn_eq_fn' φ,
+    intro g₁ g₂, apply inj' φ,
     rewrite [respect_mul φ, +right_inv φ]
     end end
 
@@ -616,7 +616,7 @@ definition fiber_eq2_equiv {A B : Type} {f : A → B} {b : B} {x y : fiber f b}
   (q₂ : point_eq x = ap f p₂ ⬝ point_eq y) : (fiber_eq p₁ q₁ = fiber_eq p₂ q₂) ≃
   (Σ(r : p₁ = p₂), q₁ ⬝ whisker_right (point_eq y) (ap02 f r) = q₂) :=
 begin
-  refine (eq_equiv_fn_eq_of_equiv (fiber_eq_equiv' x y)⁻¹ᵉ _ _)⁻¹ᵉ ⬝e sigma_eq_equiv _ _ ⬝e _,
+  refine (eq_equiv_fn_eq (fiber_eq_equiv' x y)⁻¹ᵉ _ _)⁻¹ᵉ ⬝e sigma_eq_equiv _ _ ⬝e _,
   apply sigma_equiv_sigma_right, esimp, intro r,
   refine !eq_pathover_equiv_square ⬝e _,
   refine eq_hconcat_equiv !ap_constant ⬝e hconcat_eq_equiv (ap_compose (λx, x ⬝ _) _ _) ⬝e _,
@@ -713,7 +713,7 @@ end
 
 definition is_trunc_fun_compose (k : ℕ₋₂) {A B C : Type} {g : B → C} {f : A → B}
   (Hg : is_trunc_fun k g) (Hf : is_trunc_fun k f) : is_trunc_fun k (g ∘ f) :=
-λc, is_trunc_equiv_closed_rev k (fiber_compose g f c)
+λc, is_trunc_equiv_closed_rev k (fiber_compose g f c) _
 
 definition is_conn_fun_compose (k : ℕ₋₂) {A B C : Type} {g : B → C} {f : A → B}
   (Hg : is_conn_fun k g) (Hf : is_conn_fun k f) : is_conn_fun k (g ∘ f) :=
@@ -1093,7 +1093,7 @@ namespace sphere
   --   assert H : is_contr (Ω[n] (S m)),
   --   { apply homotopy_group_sphere_le, },
   --   apply phomotopy_of_eq,
-  --   apply eq_of_fn_eq_fn !sphere_pmap_pequiv,
+  --   apply inj !sphere_pmap_pequiv,
   --   apply @is_prop.elim
   -- end
 
@@ -1370,7 +1370,7 @@ begin
   assert H : is_trunc (n.+2) (Σ(k : ℕ), iterated_prod X k),
   { apply is_trunc_sigma, apply is_trunc_succ_succ_of_is_set,
     intro, exact is_trunc_iterated_prod H },
-  apply is_trunc_equiv_closed_rev _ (list.sigma_char X),
+  apply is_trunc_equiv_closed_rev _ (list.sigma_char X) _,
 end
 
 end list
@@ -1394,11 +1394,11 @@ definition freudenthal_pequiv_trunc_index' (A : Type*) (n : ℕ) (k : ℕ₋₂)
   (H : k ≤ of_nat (2 * n)) : ptrunc k A ≃* ptrunc k (Ω (susp A)) :=
 begin
   assert lem : Π(l : ℕ₋₂), l ≤ 0 → ptrunc l A ≃* ptrunc l (Ω (susp A)),
-  { intro l H', exact ptrunc_pequiv_ptrunc_of_le H' (freudenthal_pequiv A (zero_le (2 * n))) },
+  { intro l H', exact ptrunc_pequiv_ptrunc_of_le H' (freudenthal_pequiv (zero_le (2 * n)) A) },
   cases k with k, { exact lem -2 (minus_two_le 0) },
   cases k with k, { exact lem -1 (succ_le_succ (minus_two_le -1)) },
   rewrite [-of_nat_add_two at *, add_two_sub_two at HA],
-  exact freudenthal_pequiv A (le_of_of_nat_le_of_nat H)
+  exact freudenthal_pequiv (le_of_of_nat_le_of_nat H) A
 end
 
 end susp
diff --git a/pointed_pi.hlean b/pointed_pi.hlean
index ca97908..21dec0b 100644
--- a/pointed_pi.hlean
+++ b/pointed_pi.hlean
@@ -44,7 +44,7 @@ namespace pointed
     (q : p pt ⬝hty apd10 (respect_pt g) ~ apd10 (respect_pt f)) : f ~* g :=
   begin
     apply phomotopy.mk (λa, eq_of_homotopy (p a)),
-    apply eq_of_fn_eq_fn eq_equiv_homotopy,
+    apply inj !eq_equiv_homotopy,
     apply eq_of_homotopy, intro b,
     refine !apd10_con ⬝ _,
     refine whisker_right _ !apd10_eq_of_homotopy ⬝ q b
@@ -113,7 +113,7 @@ namespace pointed
   pupi_pequiv erfl f
 
   definition loop_pupi [constructor] {A : Type} (B : A → Type*) : Ω (Πᵘ*a, B a) ≃* Πᵘ*a, Ω (B a) :=
-  pequiv_of_equiv eq_equiv_homotopy idp
+  pequiv_of_equiv !eq_equiv_homotopy idp
 
   -- definition loop_pupi_natural [constructor] {A : Type} {B B' : A → Type*} (f : Πa, B a →* B' a) :
   --   psquare (Ω→ (pupi_functor_right f)) (pupi_functor_right (λa, Ω→ (f a)))
@@ -357,7 +357,7 @@ namespace pointed
     (q : p pt ⬝* phomotopy_of_eq (respect_pt g) = phomotopy_of_eq (respect_pt f)) : f ~* g :=
   begin
     apply phomotopy.mk (λa, eq_of_phomotopy (p a)),
-    apply eq_of_fn_eq_fn !ppi_eq_equiv,
+    apply inj !ppi_eq_equiv,
     refine !phomotopy_of_eq_con ⬝ _, esimp,
     refine ap (λx, x ⬝* _) !phomotopy_of_eq_of_phomotopy ⬝ q
   end
@@ -370,7 +370,7 @@ namespace pointed
 --     : f ~* g :=
 --   begin
 --     apply phomotopy.mk (λa, eq_of_phomotopy (p a)),
---     apply eq_of_fn_eq_fn (ppi_eq_equiv _ _),
+--     apply inj (ppi_eq_equiv _ _),
 --     refine !phomotopy_of_eq_con ⬝ _,
 -- --    refine !phomotopy_of_eq_of_phomotopy ◾** idp ⬝ q,
 --   end
@@ -501,7 +501,7 @@ namespace pointed
     (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)  :=
   phomotopy.mk homotopy.rfl
-    abstract !idp_con ⬝ whisker_right _ (!ap_con ⬝ whisker_right _ !ap_compose'⁻¹) ⬝ !con.assoc end
+    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) :
@@ -608,7 +608,7 @@ namespace pointed
 
   definition ppmap.sigma_char [constructor] (A B : Type*) :
     ppmap A B ≃* @psigma_gen (A →ᵘ* B) (λf, f pt = pt) idp :=
-  pequiv_of_equiv pmap.sigma_char idp
+  pequiv_of_equiv !pmap.sigma_char idp
 
   definition pppi.sigma_char [constructor] (B : A → Type*) :
     (Π*(a : A), B a) ≃* @psigma_gen (Πᵘ*a, B a) (λf, f pt = pt) idp :=
@@ -633,7 +633,7 @@ namespace pointed
     { refine !idp_con ⬝ !idp_con ⬝ _,
       fapply sigma_eq2,
       { refine !sigma_eq_pr1 ⬝ _ ⬝ !ap_sigma_pr1⁻¹,
-        apply eq_of_fn_eq_fn eq_equiv_homotopy,
+        apply inj !eq_equiv_homotopy,
         refine !apd10_eq_of_homotopy_fn ⬝ _ ⬝ !apd10_to_fun_eq_of_phomotopy⁻¹,
         apply eq_of_homotopy, intro a, reflexivity },
       { exact sorry } }
@@ -745,7 +745,7 @@ namespace pointed
              end
       ... ≃* ppmap A (psigma_gen (λb, f b = pt) (respect_pt f)) :
              by exact (ppmap_psigma _ _)⁻¹ᵉ*
-      ... ≃* ppmap A (pfiber f) : by exact pequiv_ppcompose_left !pfiber.sigma_char'⁻¹ᵉ*
+      ... ≃* ppmap A (pfiber f) : by exact ppmap_pequiv_ppmap_right !pfiber.sigma_char'⁻¹ᵉ*
 
   -- definition pppi_ppmap {A C : Type*} {B : A → Type*} :
   --   ppmap (/- dependent smash of B -/) C ≃* Π*(a : A), ppmap (B a) C :=
diff --git a/spectrum/basic.hlean b/spectrum/basic.hlean
index da21edb..75e2905 100644
--- a/spectrum/basic.hlean
+++ b/spectrum/basic.hlean
@@ -332,13 +332,13 @@ namespace spectrum
   /-
   definition eq_of_shomotopy_pfun {N : succ_str} {X Y : gen_prespectrum N} {f g : X →ₛ Y} (H : f ~ₛ g) (n : N) : f n = g n :=
   begin
-    fapply eq_of_fn_eq_fn (smap_sigma_equiv X Y),
+    fapply inj (smap_sigma_equiv X Y),
     repeat exact sorry
   end-/
 
   definition fam_phomotopy_of_eq
     {N : Type} {X Y: N → Type*} (f g : Π n, X n →* Y n) : (f = g) ≃ (Π n, f n ~* g n) :=
-    (eq.eq_equiv_homotopy) ⬝e pi_equiv_pi_right (λ n, pmap_eq_equiv (f n) (g n))
+    !eq_equiv_homotopy ⬝e pi_equiv_pi_right (λ n, pmap_eq_equiv (f n) (g n))
 
 /-
   definition phomotopy_rec_on_eq [recursor]
@@ -385,7 +385,7 @@ namespace spectrum
 
   definition eq_of_shomotopy {N : succ_str} {X Y : gen_prespectrum N} {f g : X →ₛ Y} (H : f ~ₛ g) : f = g :=
   begin
-    fapply eq_of_fn_eq_fn (smap_sigma_equiv X Y)⁻¹ᵉ,
+    fapply inj (smap_sigma_equiv X Y)⁻¹ᵉ,
     induction f with f fsq,
     induction g with g gsq,
     induction H with H Hsq,
@@ -728,7 +728,7 @@ namespace spectrum
     : πag[k + 2] (E (-n + 2 + k)) →g πag[k + 3] (E (-n + 2 + (k + 1))) :=
   begin
     refine _ ∘g π→g[k+2] (glue E _),
-    refine (ghomotopy_group_succ_in _ (k+1))⁻¹ᵍ ∘g _,
+    refine (ghomotopy_group_succ_in (k+1) _)⁻¹ᵍ ∘g _,
     refine homotopy_group_isomorphism_of_pequiv (k+1)
       (loop_pequiv_loop (pequiv_of_eq (ap E (add.assoc (-n + 2) k 1))))
   end
@@ -796,7 +796,7 @@ namespace spectrum
   definition sp_cotensor [constructor] {N : succ_str} (A : Type*) (B : gen_spectrum N) :
     gen_spectrum N :=
     spectrum.MK (λn, ppmap A (B n))
-      (λn, (loop_ppmap_commute A (B (S n)))⁻¹ᵉ* ∘*ᵉ (pequiv_ppcompose_left (equiv_glue B n)))
+      (λn, (loop_ppmap_commute A (B (S n)))⁻¹ᵉ* ∘*ᵉ ppmap_pequiv_ppmap_right (equiv_glue B n))
 
   /- unpointed cotensor -/
   definition sp_ucotensor [constructor] {N : succ_str} (A : Type) (B : gen_spectrum N) :
diff --git a/spectrum/trunc.hlean b/spectrum/trunc.hlean
index c81043a..3ef4582 100644
--- a/spectrum/trunc.hlean
+++ b/spectrum/trunc.hlean
@@ -113,7 +113,7 @@ end
 
 definition is_strunc_pequiv_closed {k : ℤ} {E F : spectrum} (H : Πn, E n ≃* F n)
   (H2 : is_strunc k E) : is_strunc k F :=
-λn, is_trunc_equiv_closed (maxm2 (k + n)) (H n)
+λn, is_trunc_equiv_closed (maxm2 (k + n)) (H n) _
 
 definition is_strunc_sunit (n : ℤ) : is_strunc n sunit :=
 begin
diff --git a/univalent_subcategory.hlean b/univalent_subcategory.hlean
index a70b128..3add859 100644
--- a/univalent_subcategory.hlean
+++ b/univalent_subcategory.hlean
@@ -254,7 +254,7 @@ induction p,
 
   definition Group_eq_equiv (G H : Group) : G = H ≃ (G ≃g H) :=
   begin
-    refine (eq_equiv_fn_eq_of_equiv sigma_char2 G H) ⬝e _,
+    refine (eq_equiv_fn_eq sigma_char2 G H) ⬝e _,
     refine !sigma_eq_equiv ⬝e _,
     refine sigma_equiv_sigma_right Group_eq_equiv_lemma ⬝e _,
     transitivity (Σ(e : (sigma_char2 G).1 ≃ (sigma_char2 H).1),
@@ -269,7 +269,7 @@ induction p,
   definition Group_eq2 {G H : Group} {p q : G = H}
     (r : isomorphism_of_eq p ~ isomorphism_of_eq q) : p = q :=
   begin
-    apply eq_of_fn_eq_fn (Group_eq_equiv G H),
+    apply inj (Group_eq_equiv G H),
     apply isomorphism_eq,
     intro g, refine to_fun_Group_eq_equiv p g ⬝ r g ⬝ (to_fun_Group_eq_equiv q g)⁻¹,
   end
@@ -293,8 +293,7 @@ definition AbGroup_to_Group [constructor] : functor (Precategory.mk AbGroup _)
 definition is_set_group (X : Type) : is_set (group X) :=
 begin
 apply is_trunc_of_imp_is_trunc, intros, assert H : is_set X, exact @group.is_set_carrier X a, clear a,
-apply is_trunc_equiv_closed, apply equiv.symm,
-apply group.sigma_char
+exact is_trunc_equiv_closed_rev _ !group.sigma_char _
 end
 
 definition ab_group_to_group (A  : Type) (g : ab_group A) : group A := _
@@ -330,7 +329,7 @@ assert H : (fiber (total f) ⟨a, c⟩)≃ fiber (f a) c,
 apply fiber_total_equiv,
 assert H2 : is_prop (fiber (f a) c),
 apply is_prop_fiber_of_is_embedding,
-apply is_trunc_equiv_closed -1 (H⁻¹ᵉ),
+exact is_trunc_equiv_closed -1 (H⁻¹ᵉ) _
 end
 
 definition AbGroup_to_Group_homot : AbGroup_to_Group ~ Group_sigma⁻¹ ∘ total ab_group_to_group ∘ AbGroup_sigma :=