diff --git a/hott/algebra/category/constructions/comma.hlean b/hott/algebra/category/constructions/comma.hlean
index ea89813b8..e2473c61d 100644
--- a/hott/algebra/category/constructions/comma.hlean
+++ b/hott/algebra/category/constructions/comma.hlean
@@ -34,7 +34,7 @@ namespace category
 
   theorem is_trunc_comma_object (n : trunc_index) [HA : is_trunc n A]
     [HB : is_trunc n B] [H : Π(s d : C), is_trunc n (hom s d)] : is_trunc n (comma_object S T) :=
-  by apply is_trunc_equiv_closed;apply comma_object_sigma_char
+  is_trunc_equiv_closed n !comma_object_sigma_char _
 
   variables {S T}
   definition comma_object_eq' {x y : comma_object S T} (p : ob1 x = ob1 y) (q : ob2 x = ob2 y)
@@ -105,7 +105,7 @@ namespace category
   theorem is_trunc_comma_morphism (n : trunc_index) [H1 : is_trunc n (ob1 x ⟶ ob1 y)]
     [H2 : is_trunc n (ob2 x ⟶ ob2 y)] [Hp : Πm1 m2, is_trunc n (T m2 ∘ mor x = mor y ∘ S m1)]
     : is_trunc n (comma_morphism x y) :=
-  by apply is_trunc_equiv_closed; apply comma_morphism_sigma_char
+  is_trunc_equiv_closed n !comma_morphism_sigma_char _
 
   variables {x y z w}
   definition comma_morphism_eq {f f' : comma_morphism x y}
diff --git a/hott/algebra/category/constructions/pushout.hlean b/hott/algebra/category/constructions/pushout.hlean
index 7f7afc033..25cad0c22 100644
--- a/hott/algebra/category/constructions/pushout.hlean
+++ b/hott/algebra/category/constructions/pushout.hlean
@@ -418,7 +418,7 @@ namespace category
         { exact Cpushout_functor_inl η},
         { exact Cpushout_functor_inr η}},
         esimp, apply iso_pathover, apply hom_pathover,
-        rewrite [ap_compose' _ pr₁, ap_compose' _ pr₂, prod_eq_pr1, prod_eq_pr2],
+        rewrite [-ap_compose' _ pr₁, -ap_compose' _ pr₂, prod_eq_pr1, prod_eq_pr2],
         rewrite [-+respect_hom_of_eq (precomposition_functor _ _), +hom_of_eq_eq_of_iso],
         apply nat_trans_eq, intro c, esimp [category.to_precategory],
         rewrite [+id_left, +id_right, Cpushout_functor_list_singleton] end end},
diff --git a/hott/algebra/category/constructions/rezk.hlean b/hott/algebra/category/constructions/rezk.hlean
index 6efa22df6..554b536bf 100644
--- a/hott/algebra/category/constructions/rezk.hlean
+++ b/hott/algebra/category/constructions/rezk.hlean
@@ -114,7 +114,7 @@ namespace rezk
     transport (elim_set Pe Pp Pcomp) (pth f) = Pp f :=
   begin
     rewrite [tr_eq_cast_ap_fn, ↑elim_set, ▸*],
-    rewrite [ap_compose' trunctype.carrier, elim_pth], apply tcast_tua_fn
+    rewrite [-ap_compose' trunctype.carrier, elim_pth], apply tcast_tua_fn
   end
 
   end
diff --git a/hott/algebra/category/functor/basic.hlean b/hott/algebra/category/functor/basic.hlean
index 457b26020..f6dd09966 100644
--- a/hott/algebra/category/functor/basic.hlean
+++ b/hott/algebra/category/functor/basic.hlean
@@ -185,7 +185,7 @@ namespace functor
     local attribute trunctype.struct [instance] [priority 1] -- remove after #842 is closed
     protected theorem is_set_functor [instance]
       [HD : is_set D] : is_set (functor C D) :=
-    by apply is_trunc_equiv_closed; apply functor.sigma_char
+    is_trunc_equiv_closed 0 !functor.sigma_char _
   end
 
   /- higher equalities in the functor type -/
diff --git a/hott/algebra/category/functor/equivalence.hlean b/hott/algebra/category/functor/equivalence.hlean
index f0c02fe13..fb96487f4 100644
--- a/hott/algebra/category/functor/equivalence.hlean
+++ b/hott/algebra/category/functor/equivalence.hlean
@@ -283,7 +283,7 @@ namespace category
       { intro H, induction H with H1 H2, induction H1, induction H2, reflexivity},
       { intro H, induction H, reflexivity}
     end,
-    apply is_trunc_equiv_closed_rev, exact f,
+    exact is_trunc_equiv_closed_rev -1 f _
   end
 
   theorem is_prop_is_isomorphism [instance] (F : C ⇒ D) : is_prop (is_isomorphism F) :=
diff --git a/hott/algebra/group_theory.hlean b/hott/algebra/group_theory.hlean
index 778607a57..8f162fa1d 100644
--- a/hott/algebra/group_theory.hlean
+++ b/hott/algebra/group_theory.hlean
@@ -84,7 +84,7 @@ namespace group
       { intro v, induction v, reflexivity},
       { intro φ, induction φ, reflexivity}
     end,
-    apply is_trunc_equiv_closed_rev, exact H
+    exact is_trunc_equiv_closed_rev 0 H _
   end
 
   variables {G₁ G₂}
@@ -297,7 +297,7 @@ namespace group
       { intro v, induction v, reflexivity },
       { intro φ, induction φ, reflexivity }
     end,
-    apply is_trunc_equiv_closed_rev, exact H
+    exact is_trunc_equiv_closed_rev _ H _
   end
 
   definition trivial_homomorphism (A B : Group) : A →g B :=
@@ -345,7 +345,7 @@ namespace group
       mul_one      := group_equiv_mul_one,
       inv          := group_equiv_inv,
       mul_left_inv := group_equiv_mul_left_inv,
-    is_set_carrier := is_trunc_equiv_closed 0 f⦄
+    is_set_carrier := is_trunc_equiv_closed 0 f _ ⦄
 
   end
 
diff --git a/hott/choice.hlean b/hott/choice.hlean
index 7ccec2722..30310113a 100644
--- a/hott/choice.hlean
+++ b/hott/choice.hlean
@@ -56,7 +56,7 @@ namespace choice
   begin
     intro H, apply not_is_prop_bool_eq_bool,
     apply @is_trunc_equiv_closed (x0 = x0),
-    apply equiv.symm !equiv_subtype
+    apply equiv.symm !equiv_subtype, exact _
   end
 
   definition is_set_x1 (x : X) : is_set x.1 :=
diff --git a/hott/cubical/square.hlean b/hott/cubical/square.hlean
index 807e8f418..e800b87a3 100644
--- a/hott/cubical/square.hlean
+++ b/hott/cubical/square.hlean
@@ -529,7 +529,7 @@ namespace eq
 
   definition is_trunc_square [instance] (n : trunc_index) [H : is_trunc n .+2 A]
     : is_trunc n (square p₁₀ p₁₂ p₀₁ p₂₁) :=
-  is_trunc_equiv_closed_rev n !square_equiv_eq
+  is_trunc_equiv_closed_rev n !square_equiv_eq _
 
   -- definition square_of_con_inv_hsquare {p₁ p₂ p₃ p₄ : a₁ = a₂}
   --   {t : p₁ = p₂} {b : p₃ = p₄} {l : p₁ = p₃} {r : p₂ = p₄}
@@ -634,6 +634,12 @@ namespace eq
     induction q, esimp at r, induction r using idp_rec_on, exact hrfl
   end
 
+  definition natural_square2 {A B X : Type} {C : A → B → Type}
+    {a a₂ : A} {b b₂ : B} {c : C a b} {c₂ : C a₂ b₂} {f : A → X} {g : B → X}
+    (h : Πa b, C a b → f a = g b) (p : a = a₂) (q : b = b₂) (r : transport11 C p q c = c₂) :
+    square (h a b c) (h a₂ b₂ c₂) (ap f p) (ap g q) :=
+  by induction p; induction q; induction r; exact vrfl
+
   /- some higher coherence conditions -/
 
 
diff --git a/hott/hit/groupoid_quotient.hlean b/hott/hit/groupoid_quotient.hlean
index 8b421259b..dea68cfdc 100644
--- a/hott/hit/groupoid_quotient.hlean
+++ b/hott/hit/groupoid_quotient.hlean
@@ -145,7 +145,7 @@ section
     (Pcomp : Π⦃a b c⦄ (g : b ⟶ c) (f : a ⟶ b) (x : Pe a), Pp (g ∘ f) x = Pp g (Pp f x))
     {a b : G} (f : a ⟶ b) :
     transport (elim_set Pe Pp Pcomp) (pth f) = Pp f :=
-  by rewrite [tr_eq_cast_ap_fn, ↑elim_set, ▸*, ap_compose' trunctype.carrier, elim_pth];
+  by rewrite [tr_eq_cast_ap_fn, ↑elim_set, ▸*, -ap_compose' trunctype.carrier, elim_pth];
      apply tcast_tua_fn
 
 end
diff --git a/hott/hit/prop_trunc.hlean b/hott/hit/prop_trunc.hlean
index 717e9a5f7..9cae8937e 100644
--- a/hott/hit/prop_trunc.hlean
+++ b/hott/hit/prop_trunc.hlean
@@ -119,7 +119,7 @@ namespace one_step_tr
     { have q : trunc -1 ((tr_eq a a) = idp),
       begin
         refine to_fun !tr_eq_tr_equiv _,
-        refine @is_prop.elim _ _ _ _, apply is_trunc_equiv_closed, apply tr_eq_tr_equiv
+        refine @is_prop.elim _ _ _ _, exact is_trunc_equiv_closed -1 !tr_eq_tr_equiv _
       end,
       refine trunc.elim_on q _, clear q, intro p, exact !tr_eq_ne_idp p},
     { apply is_prop.elim}
diff --git a/hott/hit/pushout.hlean b/hott/hit/pushout.hlean
index 070fd7c46..ea8787614 100644
--- a/hott/hit/pushout.hlean
+++ b/hott/hit/pushout.hlean
@@ -184,7 +184,7 @@ namespace pushout
         { apply ap inl, reflexivity },
         { apply ap inr, reflexivity },
         { unfold F, unfold G, apply eq_pathover,
-          rewrite [ap_id,ap_compose' (quotient.elim _ _)],
+          rewrite [ap_id,-ap_compose' (quotient.elim _ _)],
           krewrite elim_glue, krewrite elim_eq_of_rel, apply hrefl } },
       { intro q, induction q with z z z' fr,
         { induction z with a p, induction a with x x,
@@ -192,7 +192,7 @@ namespace pushout
           { reflexivity } },
         { induction fr with a a' r p, induction r with x,
           esimp, apply eq_pathover,
-          rewrite [ap_id,ap_compose' (pushout.elim _ _ _)],
+          rewrite [ap_id,-ap_compose' (pushout.elim _ _ _)],
           krewrite elim_eq_of_rel, krewrite elim_glue, apply hrefl } }
     end
   end
@@ -276,7 +276,7 @@ namespace pushout
       { apply ap inl, apply right_inv },
       { apply ap inr, apply right_inv },
       { apply eq_pathover,
-        rewrite [ap_id,ap_compose' (pushout.functor tl bl tr fh gh)],
+        rewrite [ap_id,-ap_compose' (pushout.functor tl bl tr fh gh)],
         krewrite elim_glue,
         rewrite [ap_inv,ap_con,ap_inv],
         krewrite [pushout.ap_functor_inr], rewrite ap_con,
@@ -307,7 +307,7 @@ namespace pushout
       { apply ap inl, apply left_inv },
       { apply ap inr, apply left_inv },
       { apply eq_pathover,
-        rewrite [ap_id,ap_compose'
+        rewrite [ap_id,-ap_compose'
           (pushout.functor tl⁻¹ bl⁻¹ tr⁻¹ _ _)
           (pushout.functor tl bl tr _ _)],
         krewrite elim_glue,
diff --git a/hott/hit/quotient.hlean b/hott/hit/quotient.hlean
index 737c63f04..1b9de387e 100644
--- a/hott/hit/quotient.hlean
+++ b/hott/hit/quotient.hlean
@@ -212,96 +212,68 @@ namespace quotient
   end flattening
 
   section
-  open is_equiv equiv prod prod.ops
-  variables {A : Type} (R : A → A → Type)
-             {B : Type} (Q : B → B → Type)
-             (f : A → B) (k : Πa a' : A, R a a' → Q (f a) (f a'))
-  include f k
+  open is_equiv equiv prod function
+  variables {A : Type} {R : A → A → Type}
+            {B : Type} {Q : B → B → Type}
+            {C : Type} {S : C → C → Type}
+            (f : A → B) (k : Πa a' : A, R a a' → Q (f a) (f a'))
+            (g : B → C) (l : Πb b' : B, Q b b' → S (g b) (g b'))
 
-  protected definition functor [reducible] : quotient R → quotient Q :=
+  protected definition functor : quotient R → quotient Q :=
   quotient.elim (λa, class_of Q (f a)) (λa a' r, eq_of_rel Q (k a a' r))
 
+  definition functor_class_of (a : A) :
+    quotient.functor f k (class_of R a) = class_of Q (f a) :=
+  by reflexivity
+
+  definition functor_eq_of_rel {a a' : A} (r : R a a') :
+    ap (quotient.functor f k) (eq_of_rel R r) = eq_of_rel Q (k a a' r) :=
+  elim_eq_of_rel _ _ r
+
+  protected definition functor_compose :
+    quotient.functor (g ∘ f) (λa a' r, l (f a) (f a') (k a a' r)) ~
+    quotient.functor g l ∘ quotient.functor f k :=
+  begin
+    intro x, induction x,
+    { reflexivity },
+    { apply eq_pathover, refine hdeg_square _ ⬝hp (ap_compose (quotient.functor g l) _ _)⁻¹,
+      refine !functor_eq_of_rel ⬝ !functor_eq_of_rel⁻¹ ⬝ ap02 _ !functor_eq_of_rel⁻¹ }
+  end
+
+  protected definition functor_homotopy {f f' : A → B} {k : Πa a' : A, R a a' → Q (f a) (f a')}
+    {k' : Πa a' : A, R a a' → Q (f' a) (f' a')} (h : f ~ f')
+    (h2 : Π(a a' : A) (r : R a a'), transport11 Q (h a) (h a') (k a a' r) = k' a a' r) :
+    quotient.functor f k ~ quotient.functor f' k' :=
+  begin
+    intro x, induction x with a a a' r,
+    { exact ap (class_of Q) (h a) },
+    { apply eq_pathover, refine !functor_eq_of_rel ⬝ph _ ⬝hp !functor_eq_of_rel⁻¹,
+      apply transpose, apply natural_square2 (eq_of_rel Q), apply h2 }
+  end
+
+  protected definition functor_id (x : quotient R) :
+    quotient.functor id (λa a' r, r) x = x :=
+  begin
+    induction x,
+    { reflexivity },
+    { apply eq_pathover_id_right, apply hdeg_square, apply functor_eq_of_rel }
+  end
+
   variables [F : is_equiv f] [K : Πa a', is_equiv (k a a')]
   include F K
 
-  protected definition functor_inv [reducible] : quotient Q → quotient R :=
-  quotient.elim (λb, class_of R (f⁻¹ b))
-                (λb b' q, eq_of_rel R ((k (f⁻¹ b) (f⁻¹ b'))⁻¹
-                          ((right_inv f b)⁻¹ ▸ (right_inv f b')⁻¹ ▸ q)))
-
-  protected definition is_equiv [instance]
-    : is_equiv (quotient.functor R Q f k):=
+  protected definition is_equiv [instance] : is_equiv (quotient.functor f k) :=
   begin
-    fapply adjointify _ (quotient.functor_inv R Q f k),
-    { intro qb, induction qb with b b b' q,
-      { apply ap (class_of Q), apply right_inv },
-      { apply eq_pathover, rewrite [ap_id,ap_compose' (quotient.elim _ _)],
-        do 2 krewrite elim_eq_of_rel, rewrite (right_inv (k (f⁻¹ b) (f⁻¹ b'))),
-        have H1 : pathover (λz : B × B, Q z.1 z.2)
-          ((right_inv f b)⁻¹ ▸ (right_inv f b')⁻¹ ▸ q)
-          (prod_eq (right_inv f b) (right_inv f b')) q,
-        begin apply pathover_of_eq_tr, krewrite [prod_eq_inv,prod_eq_transport] end,
-        have H2 : square
-          (ap (λx : (Σz : B × B, Q z.1 z.2), class_of Q x.1.1)
-            (sigma_eq (prod_eq (right_inv f b) (right_inv f b')) H1))
-          (ap (λx : (Σz : B × B, Q z.1 z.2), class_of Q x.1.2)
-            (sigma_eq (prod_eq (right_inv f b) (right_inv f b')) H1))
-          (eq_of_rel Q ((right_inv f b)⁻¹ ▸ (right_inv f b')⁻¹ ▸ q))
-          (eq_of_rel Q q),
-        from
-          natural_square_tr (λw : (Σz : B × B, Q z.1 z.2), eq_of_rel Q w.2)
-          (sigma_eq (prod_eq (right_inv f b) (right_inv f b')) H1),
-        krewrite (ap_compose' (class_of Q)) at H2,
-        krewrite (ap_compose' (λz : B × B, z.1)) at H2,
-        rewrite sigma.ap_pr1 at H2, rewrite sigma_eq_pr1 at H2,
-        krewrite prod.ap_pr1 at H2, krewrite prod_eq_pr1 at H2,
-        krewrite (ap_compose' (class_of Q) (λx : (Σz : B × B, Q z.1 z.2), x.1.2)) at H2,
-        krewrite (ap_compose' (λz : B × B, z.2)) at H2,
-        rewrite sigma.ap_pr1 at H2, rewrite sigma_eq_pr1 at H2,
-        krewrite prod.ap_pr2 at H2, krewrite prod_eq_pr2 at H2,
-        apply H2 } },
-    { intro qa, induction qa with a a a' r,
-      { apply ap (class_of R), apply left_inv },
-      { apply eq_pathover, rewrite [ap_id,(ap_compose' (quotient.elim _ _))],
-        do 2 krewrite elim_eq_of_rel,
-        have H1 : pathover (λz : A × A, R z.1 z.2)
-          ((left_inv f a)⁻¹ ▸ (left_inv f a')⁻¹ ▸ r)
-          (prod_eq (left_inv f a) (left_inv f a')) r,
-        begin apply pathover_of_eq_tr, krewrite [prod_eq_inv,prod_eq_transport] end,
-        have H2 : square
-          (ap (λx : (Σz : A × A, R z.1 z.2), class_of R x.1.1)
-            (sigma_eq (prod_eq (left_inv f a) (left_inv f a')) H1))
-          (ap (λx : (Σz : A × A, R z.1 z.2), class_of R x.1.2)
-            (sigma_eq (prod_eq (left_inv f a) (left_inv f a')) H1))
-          (eq_of_rel R ((left_inv f a)⁻¹ ▸ (left_inv f a')⁻¹ ▸ r))
-          (eq_of_rel R r),
-        begin
-          exact
-          natural_square_tr (λw : (Σz : A × A, R z.1 z.2), eq_of_rel R w.2)
-          (sigma_eq (prod_eq (left_inv f a) (left_inv f a')) H1)
-        end,
-        krewrite (ap_compose' (class_of R)) at H2,
-        krewrite (ap_compose' (λz : A × A, z.1)) at H2,
-        rewrite sigma.ap_pr1 at H2, rewrite sigma_eq_pr1 at H2,
-        krewrite prod.ap_pr1 at H2, krewrite prod_eq_pr1 at H2,
-        krewrite (ap_compose' (class_of R) (λx : (Σz : A × A, R z.1 z.2), x.1.2)) at H2,
-        krewrite (ap_compose' (λz : A × A, z.2)) at H2,
-        rewrite sigma.ap_pr1 at H2, rewrite sigma_eq_pr1 at H2,
-        krewrite prod.ap_pr2 at H2, krewrite prod_eq_pr2 at H2,
-        have H3 :
-          (k (f⁻¹ (f a)) (f⁻¹ (f a')))⁻¹
-          ((right_inv f (f a))⁻¹ ▸ (right_inv f (f a'))⁻¹ ▸ k a a' r)
-          = (left_inv f a)⁻¹ ▸ (left_inv f a')⁻¹ ▸ r,
-        begin
-          rewrite [adj f a,adj f a',ap_inv',ap_inv'],
-          rewrite [-(tr_compose _ f (left_inv f a')⁻¹ (k a a' r)),
-                   -(tr_compose _ f (left_inv f a)⁻¹)],
-          rewrite [-(fn_tr_eq_tr_fn (left_inv f a')⁻¹ (λx, k a x) r),
-                   -(fn_tr_eq_tr_fn (left_inv f a)⁻¹
-                     (λx, k x (f⁻¹ (f a')))),
-                   left_inv (k _ _)]
-        end,
-        rewrite H3, apply H2 } }
+    apply adjointify _ (quotient.functor f⁻¹ᶠ
+      (λb b' q, (k (f⁻¹ᶠ b) (f⁻¹ᶠ b'))⁻¹ᶠ (transport11 Q (right_inv f b)⁻¹ (right_inv f b')⁻¹ q))),
+    exact abstract begin intro x, refine (quotient.functor_compose _ _ _ _ x)⁻¹ ⬝ _ ⬝ quotient.functor_id x,
+      apply quotient.functor_homotopy (right_inv f), intros a a' r,
+      rewrite [right_inv (k _ _), -transport11_con, con.left_inv, con.left_inv] end end,
+    exact abstract begin intro x, refine (quotient.functor_compose _ _ _ _ x)⁻¹ ⬝ _ ⬝ quotient.functor_id x,
+      apply quotient.functor_homotopy (left_inv f), intros a a' r,
+      rewrite [adj f, adj f, -ap_inv, -ap_inv, transport11_ap,
+           -fn_transport11_eq_transport11_fn _ _ _ _ k, left_inv (k _ _), -transport11_con,
+           con.left_inv, con.left_inv] end end
   end
 end
 
@@ -313,7 +285,7 @@ section
 
   /- This could also be proved using ua, but then it wouldn't compute -/
   protected definition equiv : quotient R ≃ quotient Q :=
-  equiv.mk (quotient.functor R Q f k) _
+  equiv.mk (quotient.functor f k) _
 end
 
 
diff --git a/hott/homotopy/circle.hlean b/hott/homotopy/circle.hlean
index c36f7cc97..eda87b4eb 100644
--- a/hott/homotopy/circle.hlean
+++ b/hott/homotopy/circle.hlean
@@ -309,7 +309,7 @@ namespace circle
   definition homotopy_group_of_circle (n : ℕ) : πg[n+2] S¹* ≃g G0 :=
   begin
     refine @trivial_homotopy_add_of_is_set_loopn S¹* 1 n _,
-    apply is_trunc_equiv_closed_rev, apply base_eq_base_equiv
+    exact is_trunc_equiv_closed_rev _ base_eq_base_equiv _
   end
 
   definition eq_equiv_Z (x : S¹) : x = x ≃ ℤ :=
@@ -326,8 +326,8 @@ namespace circle
   proposition is_trunc_circle [instance] : is_trunc 1 S¹ :=
   begin
     apply is_trunc_succ_of_is_trunc_loop,
-    { apply trunc_index.minus_one_le_succ},
-    { intro x, apply is_trunc_equiv_closed_rev, apply eq_equiv_Z}
+    { apply trunc_index.minus_one_le_succ },
+    { intro x, exact is_trunc_equiv_closed_rev 0 !eq_equiv_Z _ }
   end
 
   proposition is_conn_circle [instance] : is_conn 0 S¹ :=
diff --git a/hott/homotopy/connectedness.hlean b/hott/homotopy/connectedness.hlean
index cb6c9ac78..1c0456a88 100644
--- a/hott/homotopy/connectedness.hlean
+++ b/hott/homotopy/connectedness.hlean
@@ -24,16 +24,11 @@ namespace is_conn
     : A ≃ B → is_conn n A → is_conn n B :=
   begin
     intros H C,
-    fapply @is_contr_equiv_closed (trunc n A) _,
-    apply trunc_equiv_trunc,
-    assumption
+    exact is_contr_equiv_closed (trunc_equiv_trunc n H) C,
   end
 
   theorem is_conn_of_le (A : Type) {n k : ℕ₋₂} (H : n ≤ k) [is_conn k A] : is_conn n A :=
-  begin
-    apply is_contr_equiv_closed,
-    apply trunc_trunc_equiv_left _ H
-  end
+  is_contr_equiv_closed (trunc_trunc_equiv_left _ H) _
 
   theorem is_conn_fun_of_le {A B : Type} (f : A → B) {n k : ℕ₋₂} (H : n ≤ k)
     [is_conn_fun k f] : is_conn_fun n f :=
@@ -175,7 +170,7 @@ namespace is_conn
     begin
       intro a,
       apply is_conn_equiv_closed n (equiv.symm (fiber_const_equiv A a₀ a)),
-      apply @is_contr_equiv_closed _ _ (tr_eq_tr_equiv n a₀ a),
+      apply is_contr_equiv_closed (tr_eq_tr_equiv n a₀ a) _,
     end
 
   end
@@ -274,15 +269,11 @@ namespace is_conn
 
   definition is_conn_trunc [instance] (A : Type) (n k : ℕ₋₂) [H : is_conn n A]
     : is_conn n (trunc k A) :=
-  begin
-    apply is_trunc_equiv_closed, apply trunc_trunc_equiv_trunc_trunc
-  end
+  is_contr_equiv_closed !trunc_trunc_equiv_trunc_trunc _
 
   definition is_conn_eq [instance] (n : ℕ₋₂) {A : Type} (a a' : A) [is_conn (n.+1) A] :
     is_conn n (a = a') :=
-  begin
-    apply is_trunc_equiv_closed, apply tr_eq_tr_equiv,
-  end
+  is_contr_equiv_closed !tr_eq_tr_equiv _
 
   definition is_conn_loop [instance] (n : ℕ₋₂) (A : Type*) [is_conn (n.+1) A] : is_conn n (Ω A) :=
   !is_conn_eq
@@ -346,8 +337,8 @@ namespace is_conn
   definition is_conn_fun_lift_functor (n : ℕ₋₂) {A B : Type} (f : A → B) [is_conn_fun n f] :
     is_conn_fun n (lift_functor f) :=
   begin
-    intro b, cases b with b, apply is_trunc_equiv_closed_rev,
-    { apply trunc_equiv_trunc, apply fiber_lift_functor}
+    intro b, cases b with b,
+    exact is_contr_equiv_closed_rev (trunc_equiv_trunc _ !fiber_lift_functor) _
   end
 
   open trunc_index
@@ -378,7 +369,7 @@ namespace is_conn
     apply @is_contr_of_inhabited_prop,
     { apply is_trunc_succ_intro,
       refine trunc.rec _, intro a, refine trunc.rec _, intro a',
-      apply is_contr_equiv_closed !tr_eq_tr_equiv⁻¹ᵉ },
+      exact is_contr_equiv_closed !tr_eq_tr_equiv⁻¹ᵉ _ },
     exact a
   end
 
@@ -460,7 +451,7 @@ namespace is_conn
 
   definition is_contr_of_is_conn_of_is_trunc {n : ℕ₋₂} {A : Type} (H : is_trunc n A)
     (K : is_conn n A) : is_contr A :=
-  is_contr_equiv_closed (trunc_equiv n A)
+  is_contr_equiv_closed (trunc_equiv n A) _
 
   definition is_trunc_succ_succ_of_is_trunc_loop (n : ℕ₋₂) (A : Type*) (H : is_trunc (n.+1) (Ω A))
     (H2 : is_conn 0 A) : is_trunc (n.+2) A :=
@@ -477,7 +468,7 @@ namespace is_conn
     rewrite [succ_add],
     apply is_trunc_succ_succ_of_is_trunc_loop,
     { apply IH,
-      { apply is_trunc_equiv_closed _ !loopn_succ_in },
+      { exact is_trunc_equiv_closed _ !loopn_succ_in _ },
       apply is_conn_loop },
     exact is_conn_of_le _ (zero_le_of_nat m)
   end
diff --git a/hott/homotopy/homotopy_group.hlean b/hott/homotopy/homotopy_group.hlean
index 4a9ae23f9..87cb5491b 100644
--- a/hott/homotopy/homotopy_group.hlean
+++ b/hott/homotopy/homotopy_group.hlean
@@ -31,10 +31,9 @@ namespace is_trunc
   theorem trivial_homotopy_group_of_is_conn (A : Type*) {k n : ℕ} (H : k ≤ n) [is_conn n A]
     : is_contr (π[k] A) :=
   begin
-      have H3 : is_contr (ptrunc k A), from is_conn_of_le A (of_nat_le_of_nat H),
-      have H4 : is_contr (Ω[k](ptrunc k A)), from !is_trunc_loopn_of_is_trunc,
-      apply is_trunc_equiv_closed_rev,
-      { apply equiv_of_pequiv (homotopy_group_pequiv_loop_ptrunc k A)}
+    have H3 : is_contr (ptrunc k A), from is_conn_of_le A (of_nat_le_of_nat H),
+    have H4 : is_contr (Ω[k](ptrunc k A)), from !is_trunc_loopn_of_is_trunc,
+    exact is_trunc_equiv_closed_rev _ (equiv_of_pequiv (homotopy_group_pequiv_loop_ptrunc k A)) _
   end
 
   -- Corollary 8.3.3
diff --git a/hott/homotopy/imaginaroid.hlean b/hott/homotopy/imaginaroid.hlean
index 9f545e921..cf15db00c 100644
--- a/hott/homotopy/imaginaroid.hlean
+++ b/hott/homotopy/imaginaroid.hlean
@@ -70,7 +70,7 @@ section
     { reflexivity },
     { reflexivity },
     { apply eq_pathover, rewrite ap_id,
-      rewrite (ap_compose' (λy, -y)),
+      rewrite [-(ap_compose' (λy, -y))],
       krewrite susp.elim_merid, rewrite ap_inv,
       krewrite susp.elim_merid, rewrite neg_neg,
       rewrite inv_inv, apply hrefl }
@@ -85,7 +85,7 @@ section
     { reflexivity },
     { reflexivity },
     { apply eq_pathover, rewrite ap_id,
-      krewrite (ap_compose' (λy, y*)),
+      krewrite [-(ap_compose' (λy, y*))],
       do 2 krewrite susp.elim_merid, rewrite neg_neg,
       apply hrefl }
   end
@@ -96,7 +96,7 @@ section
     { reflexivity },
     { reflexivity },
     { apply eq_pathover,
-      krewrite [ap_compose' (λy, y*),ap_compose' (λy, -y) (λy, y*)],
+      krewrite [-ap_compose' (λy, y*),-ap_compose' (λy, -y) (λy, y*)],
       do 3 krewrite susp.elim_merid, rewrite ap_inv, krewrite susp.elim_merid,
       apply hrefl }
   end
diff --git a/hott/homotopy/join.hlean b/hott/homotopy/join.hlean
index f95a3a992..3d5386748 100644
--- a/hott/homotopy/join.hlean
+++ b/hott/homotopy/join.hlean
@@ -152,13 +152,13 @@ namespace join
       { apply ap inl, apply to_right_inv },
       { apply ap inr, apply to_right_inv },
       { apply eq_pathover, rewrite ap_id,
-        rewrite (ap_compose' (join.elim _ _ _)),
+        rewrite [-(ap_compose' (join.elim _ _ _))],
         do 2 krewrite join.elim_glue, apply join.hsquare } },
     { intro x, induction x with a b a b,
       { apply ap inl, apply to_left_inv },
       { apply ap inr, apply to_left_inv },
       { apply eq_pathover, rewrite ap_id,
-        rewrite (ap_compose' (join.elim _ _ _)),
+        rewrite [-(ap_compose' (join.elim _ _ _))],
         do 2 krewrite join.elim_glue, apply join.hsquare } }
   end
 
@@ -202,7 +202,7 @@ namespace join
       { reflexivity },
       { reflexivity },
       { esimp, apply eq_pathover, rewrite ap_id,
-        rewrite (ap_compose' (join.elim _ _ _)),
+        rewrite [-(ap_compose' (join.elim _ _ _))],
         rewrite [susp.elim_merid,ap_con,ap_inv],
         krewrite [join.elim_glue,join.elim_glue],
         esimp, rewrite [inv_inv,idp_con],
@@ -212,13 +212,13 @@ namespace join
       { apply glue },
       { induction b,
         { esimp, apply eq_pathover, rewrite ap_id,
-          rewrite (ap_compose' (susp.elim _ _ _)),
+          rewrite [-(ap_compose' (susp.elim _ _ _))],
           krewrite join.elim_glue, rewrite ap_inv,
           krewrite susp.elim_merid,
           apply square_of_eq_top, apply inverse,
           rewrite con.assoc, apply con.left_inv },
         { esimp, apply eq_pathover, rewrite ap_id,
-          rewrite (ap_compose' (susp.elim _ _ _)),
+          rewrite [-(ap_compose' (susp.elim _ _ _))],
           krewrite join.elim_glue, esimp,
           apply square_of_eq_top,
           rewrite [idp_con,con.right_inv] } } }
@@ -251,7 +251,7 @@ namespace join
     induction x with a b a b, do 2 reflexivity,
     apply eq_pathover, rewrite ap_id,
     apply hdeg_square,
-    apply concat, apply ap_compose' (join.elim _ _ _),
+    apply concat, apply ap_compose (join.elim _ _ _),
     krewrite [join.elim_glue, ap_inv, join.elim_glue], apply inv_inv,
   end
 
diff --git a/hott/homotopy/quaternionic_hopf.hlean b/hott/homotopy/quaternionic_hopf.hlean
index 3f3172024..5fa538bf3 100644
--- a/hott/homotopy/quaternionic_hopf.hlean
+++ b/hott/homotopy/quaternionic_hopf.hlean
@@ -62,9 +62,9 @@ namespace hopf
     rewrite circle_star_eq, induction x,
     { reflexivity },
     { apply eq_pathover, rewrite ap_constant,
-      krewrite [ap_compose' (λz : S¹ × S¹, circle_mul z.1 z.2)
+      krewrite [-ap_compose' (λz : S¹ × S¹, circle_mul z.1 z.2)
                             (λa : S¹, (a, circle_star a))],
-      rewrite [ap_compose' (prod_functor (λa : S¹, a) circle_star)
+      rewrite [-ap_compose' (prod_functor (λa : S¹, a) circle_star)
                            (λa : S¹, (a, a))],
       rewrite ap_diagonal,
       krewrite [ap_prod_functor (λa : S¹, a) circle_star loop loop],
diff --git a/hott/homotopy/sphere2.hlean b/hott/homotopy/sphere2.hlean
index 7ed5442b3..6f6401972 100644
--- a/hott/homotopy/sphere2.hlean
+++ b/hott/homotopy/sphere2.hlean
@@ -43,7 +43,7 @@ namespace sphere
     { fapply equiv.mk,
       { exact cc_to_fn (LES_of_homotopy_groups complex_hopf) (n+3, 0)},
       { have H : is_trunc 1 (pfiber complex_hopf),
-        from @(is_trunc_equiv_closed_rev _ pfiber_complex_hopf) is_trunc_circle,
+        from is_trunc_equiv_closed_rev _ pfiber_complex_hopf is_trunc_circle,
         refine LES_is_equiv_of_trivial complex_hopf (n+3) 0 _ _,
         { have H2 : 1 ≤[ℕ] n + 1, from !one_le_succ,
           exact @trivial_ghomotopy_group_of_is_trunc _ _ _ H H2 },
@@ -78,7 +78,7 @@ namespace sphere
   begin
     intro H,
     note H2 := trivial_ghomotopy_group_of_is_trunc (S (n+1)) n n !le.refl,
-    have H3 : is_contr ℤ, from is_trunc_equiv_closed _ (equiv_of_isomorphism (πnSn (n+1))),
+    have H3 : is_contr ℤ, from is_trunc_equiv_closed _ (equiv_of_isomorphism (πnSn (n+1))) _,
     have H4 : (0 : ℤ) ≠ (1 : ℤ), from dec_star,
     apply H4,
     apply is_prop.elim,
diff --git a/hott/homotopy/susp.hlean b/hott/homotopy/susp.hlean
index 6e3af5421..2e551bf13 100644
--- a/hott/homotopy/susp.hlean
+++ b/hott/homotopy/susp.hlean
@@ -180,14 +180,14 @@ namespace susp
   abstract begin
     intro sb, induction sb with b, do 2 reflexivity,
     apply eq_pathover,
-    rewrite [ap_id,ap_compose' (susp_functor' f) (susp_functor' f⁻¹)],
+    rewrite [ap_id,-ap_compose' (susp_functor' f) (susp_functor' f⁻¹)],
     krewrite [susp.elim_merid,susp.elim_merid], apply transpose,
     apply susp.merid_square (right_inv f b)
   end end
   abstract begin
     intro sa, induction sa with a, do 2 reflexivity,
     apply eq_pathover,
-    rewrite [ap_id,ap_compose' (susp_functor' f⁻¹) (susp_functor' f)],
+    rewrite [ap_id,-ap_compose' (susp_functor' f⁻¹) (susp_functor' f)],
     krewrite [susp.elim_merid,susp.elim_merid], apply transpose,
     apply susp.merid_square (left_inv f a)
   end end
@@ -302,7 +302,7 @@ namespace susp
        { reflexivity },
       { reflexivity },
       { esimp, apply eq_pathover, apply hdeg_square,
-        xrewrite [ap_compose' f, ap_compose' (susp.elim (f x) (f x) (λ (a : f x = f x), a)),▸*],
+        xrewrite [-ap_compose' f, -ap_compose' (susp.elim (f x) (f x) (λ (a : f x = f x), a)),▸*],
         xrewrite [+elim_merid, ap1_gen_idp_left] }},
     { reflexivity }
   end
@@ -330,7 +330,7 @@ namespace susp
       { reflexivity },
       { exact merid pt },
       { apply eq_pathover,
-        xrewrite [▸*, ap_id, ap_compose' (susp.elim north north (λa, a)), +elim_merid,▸*],
+        xrewrite [▸*, ap_id, -ap_compose' (susp.elim north north (λa, a)), +elim_merid,▸*],
         apply square_of_eq, exact !idp_con ⬝ !inv_con_cancel_right⁻¹ }},
     { reflexivity }
   end
diff --git a/hott/homotopy/vankampen.hlean b/hott/homotopy/vankampen.hlean
index 71dd38508..f390feff1 100644
--- a/hott/homotopy/vankampen.hlean
+++ b/hott/homotopy/vankampen.hlean
@@ -172,9 +172,9 @@ namespace pushout
     { rewrite [decode_list_pair, decode_list_nil], exact ap tr !con.left_inv},
     { apply decode_list_singleton},
     { apply decode_list_singleton},
-    { rewrite [+decode_list_pair], induction h with p, apply ap tr, rewrite [-+ap_compose'],
+    { rewrite [+decode_list_pair], induction h with p, apply ap tr, rewrite [+ap_compose'],
       exact !ap_con_eq_con_ap⁻¹},
-    { rewrite [+decode_list_pair], induction h with p, apply ap tr, rewrite [-+ap_compose'],
+    { rewrite [+decode_list_pair], induction h with p, apply ap tr, rewrite [+ap_compose'],
       apply ap_con_eq_con_ap}
   end
 
diff --git a/hott/init/funext.hlean b/hott/init/funext.hlean
index 8ee8bc10a..472876277 100644
--- a/hott/init/funext.hlean
+++ b/hott/init/funext.hlean
@@ -243,7 +243,7 @@ namespace eq
   equiv.mk apd10 _
 
   definition eq_of_homotopy [reducible] : f ~ g → f = g :=
-  (@apd10 A P f g)⁻¹
+  (@apd10 A P f g)⁻¹ᶠ
 
   definition apd10_eq_of_homotopy_fn (p : f ~ g) : apd10 (eq_of_homotopy p) = p :=
   right_inv apd10 p
diff --git a/hott/init/path.hlean b/hott/init/path.hlean
index 39f9650d2..ba71d51d5 100644
--- a/hott/init/path.hlean
+++ b/hott/init/path.hlean
@@ -14,7 +14,7 @@ open function eq
 /- Path equality -/
 
 namespace eq
-  variables {A B C : Type} {P : A → Type} {a a' x y z t : A} {b b' : B}
+  variables {A A' B B' C : Type} {P : A → Type} {a a' a'' x y z t : A} {b b' b'' : B}
 
   --notation a = b := eq a b
   notation x = y `:>`:50 A:49 := @eq A x y
@@ -364,7 +364,7 @@ namespace eq
 
   -- Sometimes we don't have the actual function [compose].
   definition ap_compose' [unfold 8] (g : B → C) (f : A → B) {x y : A} (p : x = y) :
-    ap (λa, g (f a)) p = ap g (ap f p) :=
+    ap g (ap f p) = ap (λa, g (f a)) p :=
   by induction p; reflexivity
 
   -- The action of constant maps.
@@ -403,7 +403,6 @@ namespace eq
     (r ⬝ ap f q) ⬝ p y = (r ⬝ p x) ⬝ ap g q :=
   by induction q; reflexivity
 
-  -- TODO: try this using the simplifier, and compare proofs
   definition ap_con_con_eq_con_ap_con {f g : A → B} (p : f ~ g) {x y : A} (q : x = y)
       {z : B} (s : g y = z) :
     ap f q ⬝ (p y ⬝ s) = p x ⬝ (ap g q ⬝ s) :=
@@ -560,6 +559,28 @@ namespace eq
     (p : a = a') (q : b = b') (z : P a b) : P a' b' :=
   transport (P a') q (p ▸ z)
 
+  definition transport11_con (P : A → B → Type) (p : a = a') (p' : a' = a'') (q : b = b')
+    (q' : b' = b'') (z : P a b) :
+    transport11 P (p ⬝ p') (q ⬝ q') z = transport11 P p' q' (transport11 P p q z) :=
+  begin induction p', induction q', reflexivity end
+
+  definition transport11_compose (P : A' → B' → Type) (f : A → A') (g : B → B')
+    (p : a = a') (q : b = b') (z : P (f a) (g b)) :
+    transport11 (λa b, P (f a) (g b)) p q z = transport11 P (ap f p) (ap g q) z :=
+  by induction p; induction q; reflexivity
+
+  definition transport11_ap (P : A' → B' → Type) (f : A → A') (g : B → B')
+    (p : a = a') (q : b = b') (z : P (f a) (g b)) :
+     transport11 P (ap f p) (ap g q) z =
+     transport11 (λ(a : A) (b : B), P (f a) (g b)) p q z :=
+  (transport11_compose P f g p q z)⁻¹
+
+  definition fn_transport11_eq_transport11_fn (P : A → B → Type)
+    (Q : A → B → Type) (p : a = a') (q : b = b')
+    (f : Πa b, P a b → Q a b) (z : P a b) :
+    f a' b' (transport11 P p q z) = transport11 Q p q (f a b z) :=
+  by induction p; induction q; reflexivity
+
   -- Transporting along higher-dimensional paths
   definition transport2 [unfold 7] (P : A → Type) {x y : A} {p q : x = y} (r : p = q) (z : P x) :
     p ▸ z = q ▸ z :=
diff --git a/hott/init/pathover.hlean b/hott/init/pathover.hlean
index c389bc86b..55de1168f 100644
--- a/hott/init/pathover.hlean
+++ b/hott/init/pathover.hlean
@@ -21,6 +21,7 @@ namespace eq
   idpatho : pathover B b (refl a) b
 
   notation b ` =[`:50 p:0 `] `:0 b₂:50 := pathover _ b p b₂
+  notation b ` =[`:50 p:0 `; `:0 B `] `:0 b₂:50 := pathover B b p b₂
 
   definition idpo [reducible] [constructor] : b =[refl a] b :=
   pathover.idpatho b
diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean
index bf504c0bb..3410d41b1 100644
--- a/hott/init/trunc.hlean
+++ b/hott/init/trunc.hlean
@@ -271,9 +271,12 @@ namespace is_trunc
     : (is_contr B) :=
   is_contr.mk (f (center A)) (λp, eq_of_eq_inv !center_eq)
 
-  definition is_contr_equiv_closed (H : A ≃ B) [HA: is_contr A] : is_contr B :=
+  definition is_contr_equiv_closed (H : A ≃ B) (HA : is_contr A) : is_contr B :=
   is_contr_is_equiv_closed (to_fun H)
 
+  definition is_contr_equiv_closed_rev (H : A ≃ B) (HB : is_contr B) : is_contr A :=
+  is_contr_equiv_closed H⁻¹ᵉ HB
+
   definition equiv_of_is_contr_of_is_contr [HA : is_contr A] [HB : is_contr B] : A ≃ B :=
   equiv.mk
     (λa, center B)
@@ -292,12 +295,10 @@ namespace is_trunc
     [HA : is_trunc n B] : is_trunc n A :=
   is_trunc_is_equiv_closed n f⁻¹
 
-  definition is_trunc_equiv_closed (n : ℕ₋₂) (f : A ≃ B) [HA : is_trunc n A]
-    : is_trunc n B :=
+  definition is_trunc_equiv_closed (n : ℕ₋₂) (f : A ≃ B) (HA : is_trunc n A) : is_trunc n B :=
   is_trunc_is_equiv_closed n (to_fun f)
 
-  definition is_trunc_equiv_closed_rev (n : ℕ₋₂) (f : A ≃ B) [HA : is_trunc n B]
-    : is_trunc n A :=
+  definition is_trunc_equiv_closed_rev (n : ℕ₋₂) (f : A ≃ B) (HA : is_trunc n B) : is_trunc n A :=
   is_trunc_is_equiv_closed n (to_inv f)
 
   definition is_equiv_of_is_prop [constructor] [HA : is_prop A] [HB : is_prop B]
@@ -318,7 +319,7 @@ namespace is_trunc
   /- truncatedness of lift -/
   definition is_trunc_lift [instance] [priority 1450] (A : Type) (n : ℕ₋₂)
     [H : is_trunc n A] : is_trunc n (lift A) :=
-  is_trunc_equiv_closed _ !equiv_lift
+  is_trunc_equiv_closed _ !equiv_lift _
 
   end
 
@@ -341,7 +342,7 @@ namespace is_trunc
 
   definition is_trunc_pathover [instance]
     (n : ℕ₋₂) [H : is_trunc (n.+1) (C a)] : is_trunc n (c =[p] c₂) :=
-  is_trunc_equiv_closed_rev n !pathover_equiv_eq_tr
+  is_trunc_equiv_closed_rev n !pathover_equiv_eq_tr _
 
   definition is_prop.elimo [H : is_prop (C a)] : c =[p] c₂ :=
   pathover_of_eq_tr !is_prop.elim
diff --git a/hott/types/W.hlean b/hott/types/W.hlean
index 7ea30fdb7..46baa61bc 100644
--- a/hott/types/W.hlean
+++ b/hott/types/W.hlean
@@ -124,8 +124,9 @@ namespace Wtype
   fapply is_trunc_equiv_closed,
   { apply equiv_path_W},
   { apply is_trunc_sigma,
-    intro p, cases p, esimp, apply is_trunc_equiv_closed_rev,
-      apply pathover_idp}
+    intro p, cases p,
+    apply is_trunc_equiv_closed_rev n !pathover_idp,
+    apply is_trunc_pi_eq, intro b, apply IH }
   end
 
 end Wtype
diff --git a/hott/types/equiv.hlean b/hott/types/equiv.hlean
index 10a584987..32b5035a2 100644
--- a/hott/types/equiv.hlean
+++ b/hott/types/equiv.hlean
@@ -42,11 +42,11 @@ namespace is_equiv
   definition is_contr_right_coherence (u : Σ(g : B → A), f ∘ g ~ id)
     : is_contr (Σ(η : u.1 ∘ f ~ id), Π(a : A), u.2 (f a) = ap f (η a)) :=
   begin
-    fapply is_trunc_equiv_closed,
-      {apply equiv.symm, apply sigma_pi_equiv_pi_sigma},
-    fapply is_trunc_equiv_closed,
-      {apply pi_equiv_pi_right, intro a,
-        apply (fiber_eq_equiv (fiber.mk (u.1 (f a)) (u.2 (f a))) (fiber.mk a idp))},
+    apply is_contr_equiv_closed_rev !sigma_pi_equiv_pi_sigma,
+    apply is_contr_equiv_closed,
+    { apply pi_equiv_pi_right, intro a,
+      apply (fiber_eq_equiv (fiber.mk (u.1 (f a)) (u.2 (f a))) (fiber.mk a idp)) },
+    exact _
   end
 
   omit H
@@ -77,7 +77,7 @@ namespace is_equiv
 
   theorem is_prop_is_equiv [instance] : is_prop (is_equiv f) :=
   is_prop_of_imp_is_contr
-    (λ(H : is_equiv f), is_trunc_equiv_closed -2 (equiv.symm !is_equiv.sigma_char'))
+    (λ(H : is_equiv f), is_contr_equiv_closed (equiv.symm !is_equiv.sigma_char') _)
 
   definition inv_eq_inv {A B : Type} {f f' : A → B} {Hf : is_equiv f} {Hf' : is_equiv f'}
     (p : f = f') : f⁻¹ = f'⁻¹ :=
@@ -209,7 +209,7 @@ namespace is_equiv
   begin
     intro a,
     apply is_equiv_of_is_contr_fun, intro q,
-    apply @is_contr_equiv_closed _ _ (fiber_total_equiv f q)
+    exact is_contr_equiv_closed (fiber_total_equiv f q) _
   end
 
 end is_equiv
diff --git a/hott/types/fiber.hlean b/hott/types/fiber.hlean
index 65a2e07e2..32735d08f 100644
--- a/hott/types/fiber.hlean
+++ b/hott/types/fiber.hlean
@@ -170,7 +170,7 @@ namespace fiber
     fapply pequiv_of_equiv, esimp,
     refine transport_fiber_equiv (g ∘* f) (respect_pt g)⁻¹ ⬝e fiber.equiv_postcompose f g (Point B),
     esimp, apply (ap (fiber.mk (Point A))), refine !con.assoc ⬝ _, apply inv_con_eq_of_eq_con,
-    rewrite [▸*, con.assoc, con.right_inv, con_idp, -ap_compose'],
+    rewrite [▸*, con.assoc, con.right_inv, con_idp, ap_compose'],
     exact ap_con_eq_con (λ x, ap g⁻¹ᵉ* (ap g (pleft_inv' g x)⁻¹) ⬝ ap g⁻¹ᵉ* (pright_inv g (g x)) ⬝
       pleft_inv' g x) (respect_pt f)
   end
@@ -291,7 +291,7 @@ namespace fiber
   -- this breaks certain proofs if it is an instance
   definition is_trunc_fiber (n : ℕ₋₂) {A B : Type} (f : A → B) (b : B)
     [is_trunc n A] [is_trunc (n.+1) B] : is_trunc n (fiber f b) :=
-  is_trunc_equiv_closed_rev n !fiber.sigma_char
+  is_trunc_equiv_closed_rev n !fiber.sigma_char _
 
   definition is_trunc_pfiber (n : ℕ₋₂) {A B : Type*} (f : A →* B)
     [is_trunc n A] [is_trunc (n.+1) B] : is_trunc n (pfiber f) :=
diff --git a/hott/types/fin.hlean b/hott/types/fin.hlean
index 011827035..a29c5b884 100644
--- a/hott/types/fin.hlean
+++ b/hott/types/fin.hlean
@@ -30,8 +30,8 @@ end
 
 definition is_set_fin [instance] : is_set (fin n) :=
 begin
-  assert H : Πa, is_set (a < n), exact _, -- I don't know why this is necessary
-  apply is_trunc_equiv_closed_rev, apply fin.sigma_char,
+  assert H : Πa, is_set (a < n), exact _,
+  apply is_trunc_equiv_closed_rev 0 !fin.sigma_char _,
 end
 
 definition eq_of_veq : Π {i j : fin n}, (val i) = j → i = j :=
diff --git a/hott/types/pi.hlean b/hott/types/pi.hlean
index 4bb6d0cf4..cae70f3d6 100644
--- a/hott/types/pi.hlean
+++ b/hott/types/pi.hlean
@@ -269,28 +269,22 @@ namespace pi
       [H : ∀a, is_trunc n (B a)] : is_trunc n (Πa, B a) :=
   begin
     revert B H,
-    eapply (trunc_index.rec_on n),
-      {intro B H,
-        fapply is_contr.mk,
-          intro a, apply center,
-          intro f, apply eq_of_homotopy,
-            intro x, apply (center_eq (f x))},
-      {intro n IH B H,
-        fapply is_trunc_succ_intro, intro f g,
-          fapply is_trunc_equiv_closed,
-            apply equiv.symm, apply eq_equiv_homotopy,
-            apply IH,
-              intro a,
-              show is_trunc n (f a = g a), from
-              is_trunc_eq n (f a) (g a)}
+    induction n with n IH,
+    { intros B H, apply is_contr.mk (λa, !center),
+      intro f, apply eq_of_homotopy,
+      intro x, apply (center_eq (f x)) },
+    { intros B H, fapply is_trunc_succ_intro, intro f g,
+      fapply is_trunc_equiv_closed,
+      apply equiv.symm, apply eq_equiv_homotopy,
+      apply IH,
+      intro a,
+      show is_trunc n (f a = g a), from
+      is_trunc_eq n (f a) (g a) }
   end
   local attribute is_trunc_pi [instance]
-  theorem is_trunc_pi_eq [instance] [priority 500] (n : trunc_index) (f g : Πa, B a)
+  theorem is_trunc_pi_eq (n : trunc_index) (f g : Πa, B a)
       [H : ∀a, is_trunc n (f a = g a)] : is_trunc n (f = g) :=
-  begin
-    apply is_trunc_equiv_closed_rev,
-    apply eq_equiv_homotopy
-  end
+  is_trunc_equiv_closed_rev n !eq_equiv_homotopy _
 
   theorem is_trunc_not [instance] (n : trunc_index) (A : Type) : is_trunc (n.+1) ¬A :=
   by unfold not;exact _
diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean
index a650955c8..14902f57f 100644
--- a/hott/types/pointed.hlean
+++ b/hott/types/pointed.hlean
@@ -134,7 +134,7 @@ namespace pointed
 
   definition passoc [constructor] (h : C →* D) (g : B →* C) (f : A →* B) : (h ∘* g) ∘* f ~* h ∘* (g ∘* f) :=
   phomotopy.mk (λa, idp)
-    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 pid_pcompose [constructor] (f : A →* B) : pid B ∘* f ~* f :=
   begin
@@ -368,7 +368,7 @@ namespace pointed
 
   definition is_trunc_ppi [instance] (n : ℕ₋₂) {A : Type*} (B : A → Type) (b₀ : B pt) [Πa, is_trunc n (B a)] :
     is_trunc n (ppi B b₀) :=
-  is_trunc_equiv_closed_rev _ !ppi.sigma_char
+  is_trunc_equiv_closed_rev _ !ppi.sigma_char _
 
   definition is_trunc_pmap [instance] (n : ℕ₋₂) (A B : Type*) [is_trunc n B] :
     is_trunc n (A →* B) :=
diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean
index 452093ce7..2aba40ae8 100644
--- a/hott/types/sigma.hlean
+++ b/hott/types/sigma.hlean
@@ -526,11 +526,9 @@ namespace sigma
   begin
   revert A B HA HB,
   induction n with n IH,
-  { intro A B HA HB, fapply is_trunc_equiv_closed_rev, apply sigma_equiv_of_is_contr_left},
+  { intro A B HA HB, exact is_contr_equiv_closed_rev !sigma_equiv_of_is_contr_left _ },
   { intro A B HA HB, apply is_trunc_succ_intro, intro u v,
-    apply is_trunc_equiv_closed_rev,
-      apply sigma_eq_equiv,
-      exact IH _ _ _ _}
+    exact is_trunc_equiv_closed_rev n !sigma_eq_equiv (IH _ _ _ _) }
   end
 
   theorem is_trunc_subtype (B : A → Prop) (n : trunc_index)
diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean
index c69d96308..9a51c1e9b 100644
--- a/hott/types/trunc.hlean
+++ b/hott/types/trunc.hlean
@@ -270,7 +270,7 @@ namespace trunc_index
   equiv.MK add_two sub_two add_two_sub_two sub_two_add_two
 
   definition is_set_trunc_index [instance] : is_set ℕ₋₂ :=
-  is_trunc_equiv_closed_rev 0 trunc_index_equiv_nat
+  is_trunc_equiv_closed_rev 0 trunc_index_equiv_nat _
 
 end trunc_index open trunc_index
 
@@ -333,8 +333,8 @@ namespace is_trunc
   theorem is_trunc_trunctype [instance] (n : ℕ₋₂) : is_trunc n.+1 (n-Type) :=
   begin
     apply is_trunc_succ_intro, intro X Y,
-    fapply is_trunc_equiv_closed_rev, { apply trunctype_eq_equiv},
-    fapply is_trunc_equiv_closed_rev, { apply eq_equiv_equiv},
+    apply is_trunc_equiv_closed_rev _ !trunctype_eq_equiv,
+    apply is_trunc_equiv_closed_rev _ !eq_equiv_equiv,
     induction n,
     { apply @is_contr_of_inhabited_prop,
       { apply is_trunc_equiv },
@@ -649,16 +649,14 @@ namespace trunc
     (n m : ℕ₋₂) [H : is_trunc n A] : is_trunc n (trunc m A) :=
   begin
     revert A m H, eapply (trunc_index.rec_on n),
-    { clear n, intro A m H, apply is_contr_equiv_closed,
-      { apply equiv.symm, apply trunc_equiv, apply (@is_trunc_of_le _ -2), apply minus_two_le} },
+    { clear n, intro A m H, refine is_contr_equiv_closed_rev _ H,
+      { apply trunc_equiv, apply (@is_trunc_of_le _ -2), apply minus_two_le} },
     { clear n, intro n IH A m H, induction m with m,
       { apply (@is_trunc_of_le _ -2), apply minus_two_le},
       { apply is_trunc_succ_intro, intro aa aa',
         apply (@trunc.rec_on _ _ _ aa  (λy, !is_trunc_succ_of_is_prop)),
         eapply (@trunc.rec_on _ _ _ aa' (λy, !is_trunc_succ_of_is_prop)),
-        intro a a', apply (is_trunc_equiv_closed_rev),
-        { apply tr_eq_tr_equiv},
-        { exact (IH _ _ _)}}}
+        intro a a', apply is_trunc_equiv_closed_rev _ !tr_eq_tr_equiv (IH _ _ _) }}
   end
 
   /- equivalences between truncated types (see also hit.trunc) -/
@@ -696,10 +694,7 @@ namespace trunc
 
   theorem is_trunc_trunc_of_le (A : Type)
     (n : ℕ₋₂) {m k : ℕ₋₂} (H : m ≤ k) [is_trunc n (trunc k A)] : is_trunc n (trunc m A) :=
-  begin
-    apply is_trunc_equiv_closed,
-    { apply trunc_trunc_equiv_left, exact H},
-  end
+  is_trunc_equiv_closed _ (trunc_trunc_equiv_left _ H) _
 
   definition trunc_functor_homotopy [unfold 7] {X Y : Type} (n : ℕ₋₂) {f g : X → Y}
     (p : f ~ g) (x : trunc n X) : trunc_functor n f x = trunc_functor n g x :=
@@ -855,8 +850,8 @@ namespace trunc
   begin
     fapply phomotopy.mk,
     { apply trunc_functor_compose},
-    { esimp, refine !idp_con ⬝ _, refine whisker_right _ !ap_compose'⁻¹ᵖ ⬝ _,
-      esimp, refine whisker_right _ (ap_compose' tr g _) ⬝ _, exact !ap_con⁻¹},
+    { esimp, refine !idp_con ⬝ _, refine whisker_right _ !ap_compose' ⬝ _,
+      esimp, refine whisker_right _ (ap_compose tr g _) ⬝ _, exact !ap_con⁻¹},
   end
 
   definition ptrunc_functor_pid [constructor] (X : Type*) (n : ℕ₋₂) :
@@ -872,7 +867,7 @@ namespace trunc
   begin
     fapply phomotopy.mk,
     { intro x, esimp, refine !trunc_functor_cast ⬝ _, refine ap010 cast _ x,
-      refine !ap_compose'⁻¹ ⬝ !ap_compose'},
+      refine !ap_compose' ⬝ !ap_compose },
     { induction p, reflexivity},
   end
 
@@ -950,7 +945,7 @@ namespace trunc
   begin
     fapply phomotopy.mk,
     { intro a, induction a with a, reflexivity },
-    { refine !idp_con ⬝ _ ⬝ !idp_con⁻¹, refine !ap_compose'⁻¹ ⬝ _, apply ap_id }
+    { refine !idp_con ⬝ _ ⬝ !idp_con⁻¹, refine !ap_compose' ⬝ _, apply ap_id }
   end
 
   definition ptr_natural [constructor] (n : ℕ₋₂) {A B : Type*} (f : A →* B) :