diff --git a/library/hott/axioms/funext.lean b/library/hott/axioms/funext.lean
index 1ad2df7fa..e74672a32 100644
--- a/library/hott/axioms/funext.lean
+++ b/library/hott/axioms/funext.lean
@@ -3,7 +3,6 @@
 -- Author: Jeremy Avigad, Jakob von Raumer
 -- Ported from Coq HoTT
 
--- TODO: take a look at the Coq tricks
 import hott.path hott.equiv
 open path
 
@@ -12,7 +11,7 @@ open path
 
 -- Define function extensionality as a type class
 inductive funext [class] : Type  :=
-  mk : (Π (A : Type) (P : A → Type ) (f g : Π x, P x), IsEquiv (@apD10 A P f g))
+  mk : (Π (A : Type) (P : A → Type ) (f g : Π x, P x), is_equiv (@apD10 A P f g))
          → funext
 
 namespace funext
@@ -21,11 +20,11 @@ namespace funext
     universe variables l k
     parameters [F : funext.{l k}] {A : Type.{l}} {P : A → Type.{k}} (f g : Π x, P x)
 
-    protected definition ap [instance] : IsEquiv (@apD10 A P f g) :=
+    protected definition ap [instance] : is_equiv (@apD10 A P f g) :=
       rec_on F (λ (H : Π A P f g, _), !H)
 
     definition path_forall : f ∼ g → f ≈ g :=
-      @IsEquiv.inv _ _ (@apD10 A P f g) ap
+      @is_equiv.inv _ _ (@apD10 A P f g) ap
 
   end
 
diff --git a/library/hott/axioms/ua.lean b/library/hott/axioms/ua.lean
index 302648177..007850d3f 100644
--- a/library/hott/axioms/ua.lean
+++ b/library/hott/axioms/ua.lean
@@ -3,7 +3,7 @@
 -- Author: Jakob von Raumer
 -- Ported from Coq HoTT
 import hott.path hott.equiv
-open path Equiv
+open path equiv
 
 --Ensure that the types compared are in the same universe
 section
@@ -11,15 +11,15 @@ section
   variables {A B : Type.{l}}
 
   definition isequiv_path (H : A ≈ B) :=
-    (@IsEquiv.transport Type (λX, X) A B H)
+    (@is_equiv.transport Type (λX, X) A B H)
 
   definition equiv_path (H : A ≈ B) : A ≃ B :=
-    Equiv.mk _ (isequiv_path H)
+    equiv.mk _ (isequiv_path H)
 
 end
 
 inductive ua_type [class] : Type :=
-  mk : (Π (A B : Type), IsEquiv (@equiv_path A B)) → ua_type
+  mk : (Π (A B : Type), is_equiv (@equiv_path A B)) → ua_type
 
 namespace ua_type
 
@@ -28,12 +28,12 @@ namespace ua_type
     parameters [F : ua_type.{k}] {A B: Type.{k}}
 
     -- Make the Equivalence given by the axiom an instance
-    protected definition inst [instance] : IsEquiv (@equiv_path.{k} A B) :=
+    protected definition inst [instance] : is_equiv (@equiv_path.{k} A B) :=
       rec_on F (λ H, H A B)
 
     -- This is the version of univalence axiom we will probably use most often
     definition ua : A ≃ B →  A ≈ B :=
-      @IsEquiv.inv _ _ (@equiv_path A B) inst
+      @is_equiv.inv _ _ (@equiv_path A B) inst
 
   end
 
diff --git a/library/hott/equiv.lean b/library/hott/equiv.lean
index 01400a871..b9a478fee 100644
--- a/library/hott/equiv.lean
+++ b/library/hott/equiv.lean
@@ -8,75 +8,32 @@ open path function
 -- Equivalences
 -- ------------
 
-definition Sect {A B : Type} (s : A → B) (r : B → A) := Πx : A, r (s x) ≈ x
-
--- -- TODO: need better means of declaring structures
--- -- TODO: note that Coq allows projections to be declared to be coercions on the fly
-
--- Structure IsEquiv
-
-inductive IsEquiv [class] {A B : Type} (f : A → B) :=
-mk : Π
+-- This is our definition of equivalence. In the HoTT-book it's called
+-- ihae (half-adjoint equivalence).
+structure is_equiv [class] {A B : Type} (f : A → B) :=
   (inv : B → A)
-  (retr : Sect inv f)
-  (sect : Sect f inv)
-  (adj : Πx, retr (f x) ≈ ap f (sect x)),
-IsEquiv f
+  (retr : (f ∘ inv) ∼ id)
+  (sect : (inv ∘ f) ∼ id)
+  (adj : Πx, retr (f x) ≈ ap f (sect x))
 
-namespace IsEquiv
+-- A more bundled version of equivalence to calculate with
+structure equiv (A B : Type) :=
+  (to_fun : A → B)
+  (to_is_equiv : is_equiv to_fun)
 
-  definition inv {A B : Type} (f : A → B) [H : IsEquiv f] : B → A :=
-    IsEquiv.rec (λinv retr sect adj, inv) H
-
-  -- TODO: note: does not type check without giving the type
-  definition retr {A B : Type} (f : A → B) [H : IsEquiv f] : Sect (inv f) f :=
-    IsEquiv.rec (λinv retr sect adj, retr) H
-
-  definition sect {A B : Type} (f : A → B) [H : IsEquiv f] : Sect f (inv f) :=
-    IsEquiv.rec (λinv retr sect adj, sect) H
-
-  definition adj {A B : Type} (f : A → B) [H : IsEquiv f] :
-             Πx, retr f (f x) ≈ ap f (sect f x) :=
-    IsEquiv.rec (λinv retr sect adj, adj) H
+ -- Some instances and closure properties of equivalences
+namespace is_equiv
 
   postfix `⁻¹` := inv
 
-end IsEquiv
-
--- Structure Equiv
-
-inductive Equiv (A B : Type) : Type :=
-mk : Π
-  (equiv_fun : A → B)
-  (equiv_isequiv : IsEquiv equiv_fun),
-Equiv A B
-
-namespace Equiv
-
-  --Note: No coercion here
-  definition equiv_fun {A B : Type} (e : Equiv A B) : A → B :=
-    Equiv.rec (λequiv_fun equiv_isequiv, equiv_fun) e
-
-  definition equiv_isequiv [instance] {A B : Type} (e : Equiv A B) : IsEquiv (equiv_fun e) :=
-    Equiv.rec (λequiv_fun equiv_isequiv, equiv_isequiv) e
-
-  infix `≃`:25 := Equiv
-
-end Equiv
-
-  -- Some instances and closure properties of equivalences
-
-namespace IsEquiv
-  variables {A B C : Type} {f : A → B} {g : B → C} {f' : A → B}
+  variables {A B C : Type} (f : A → B) (g : B → C) {f' : A → B}
 
   -- The identity function is an equivalence.
-
-  definition id_closed [instance] : (@IsEquiv A A id) := IsEquiv.mk id (λa, idp) (λa, idp) (λa, idp)
+  protected definition id_is_equiv : (@is_equiv A A id) := is_equiv.mk id (λa, idp) (λa, idp) (λa, idp)
 
   -- The composition of two equivalences is, again, an equivalence.
-
-  definition comp_closed [instance] (Hf : IsEquiv f) (Hg : IsEquiv g) : (IsEquiv (g ∘ f)) :=
-    IsEquiv.mk ((inv f) ∘ (inv g))
+  protected definition compose [Hf : is_equiv f] [Hg : is_equiv g] : (is_equiv (g ∘ f)) :=
+    is_equiv.mk ((inv f) ∘ (inv g))
                (λc, ap g (retr f (g⁻¹ c)) ⬝ retr g c)
                (λa, ap (inv f) (sect g (f a)) ⬝ sect f a)
                (λa, (whiskerL _ (adj g (f a))) ⬝
@@ -89,54 +46,53 @@ namespace IsEquiv
                )
 
   -- Any function equal to an equivalence is an equivlance as well.
-  definition path_closed (Hf : IsEquiv f) (Heq : f ≈ f') : (IsEquiv f') :=
+  definition path_closed [Hf : is_equiv f] (Heq : f ≈ f') : (is_equiv f') :=
      path.rec_on Heq Hf
 
   -- Any function pointwise equal to an equivalence is an equivalence as well.
-  definition homotopic (Hf : IsEquiv f) (Heq : f ∼ f') : (IsEquiv f') :=
-    let sect' := (λ b, (Heq (inv f b))⁻¹ ⬝ retr f b) in
-    let retr' := (λ a, (ap (inv f) (Heq a))⁻¹ ⬝ sect f a) in
+  definition homotopy_closed [Hf : is_equiv f] (Hty : f ∼ f') : (is_equiv f') :=
+    let sect' := (λ b, (Hty (inv f b))⁻¹ ⬝ retr f b) in
+    let retr' := (λ a, (ap (inv f) (Hty a))⁻¹ ⬝ sect f a) in
     let adj' := (λ (a : A),
-      let ff'a := Heq a in
+      let ff'a := Hty a in
       let invf := inv f in
       let secta := sect f a in
       let retrfa := retr f (f a) in
       let retrf'a := retr f (f' a) in
       have eq1 : _ ≈ _,
         from calc ap f secta ⬝ ff'a
-              ≈ retrfa ⬝ ff'a : (ap _ (adj f _ ))⁻¹
-          ... ≈ ap (f ∘ invf) ff'a ⬝ retrf'a : !concat_A1p⁻¹
-          ... ≈ ap f (ap invf ff'a) ⬝ retr f (f' a) : {ap_compose invf f _},
+              ≈ retrfa ⬝ ff'a : ap _ (@adj _ _ f _ _)
+          ... ≈ ap (f ∘ invf) ff'a ⬝ retrf'a : concat_A1p
+          ... ≈ ap f (ap invf ff'a) ⬝ retrf'a : ap_compose invf f,
       have eq2 : _ ≈ _,
         from calc retrf'a
               ≈ (ap f (ap invf ff'a))⁻¹ ⬝ (ap f secta ⬝ ff'a) : moveL_Vp _ _ _ (eq1⁻¹)
-          ... ≈ ap f (ap invf ff'a)⁻¹ ⬝ (ap f secta ⬝ Heq a) : {ap_V invf ff'a}
-          ... ≈ ap f (ap invf ff'a)⁻¹ ⬝ (Heq (invf (f a)) ⬝ ap f' secta) : {!concat_Ap}
-          ... ≈ (ap f (ap invf ff'a)⁻¹ ⬝ Heq (invf (f a))) ⬝ ap f' secta : {!concat_pp_p⁻¹}
-          ... ≈ (ap f ((ap invf ff'a)⁻¹) ⬝ Heq (invf (f a))) ⬝ ap f' secta : {!ap_V⁻¹}
-          ... ≈ (Heq (invf (f' a)) ⬝ ap f' ((ap invf ff'a)⁻¹)) ⬝ ap f' secta : {!concat_Ap}
-          ... ≈ (Heq (invf (f' a)) ⬝ (ap f' (ap invf ff'a))⁻¹) ⬝ ap f' secta : {!ap_V}
-          ... ≈ Heq (invf (f' a)) ⬝ ((ap f' (ap invf ff'a))⁻¹ ⬝ ap f' secta) : !concat_pp_p,
+          ... ≈ ap f (ap invf ff'a)⁻¹ ⬝ (ap f secta ⬝ Hty a) : ap_V invf ff'a
+          ... ≈ ap f (ap invf ff'a)⁻¹ ⬝ (Hty (invf (f a)) ⬝ ap f' secta) : concat_Ap
+          ... ≈ (ap f (ap invf ff'a)⁻¹ ⬝ Hty (invf (f a))) ⬝ ap f' secta : concat_pp_p
+          ... ≈ (ap f ((ap invf ff'a)⁻¹) ⬝ Hty (invf (f a))) ⬝ ap f' secta : ap_V
+          ... ≈ (Hty (invf (f' a)) ⬝ ap f' ((ap invf ff'a)⁻¹)) ⬝ ap f' secta : concat_Ap
+          ... ≈ (Hty (invf (f' a)) ⬝ (ap f' (ap invf ff'a))⁻¹) ⬝ ap f' secta : ap_V
+          ... ≈ Hty (invf (f' a)) ⬝ ((ap f' (ap invf ff'a))⁻¹ ⬝ ap f' secta) : concat_pp_p,
       have eq3 : _ ≈ _,
-        from calc (Heq (invf (f' a)))⁻¹ ⬝ retr f (f' a)
+        from calc (Hty (invf (f' a)))⁻¹ ⬝ retrf'a
               ≈ (ap f' (ap invf ff'a))⁻¹ ⬝ ap f' secta : moveR_Vp _ _ _ eq2
-          ... ≈ (ap f' ((ap invf ff'a)⁻¹)) ⬝ ap f' secta : {!ap_V⁻¹}
-          ... ≈ ap f' ((ap invf ff'a)⁻¹ ⬝ secta) : !ap_pp⁻¹,
+          ... ≈ (ap f' ((ap invf ff'a)⁻¹)) ⬝ ap f' secta : ap_V
+          ... ≈ ap f' ((ap invf ff'a)⁻¹ ⬝ secta) : ap_pp,
     eq3) in
-  IsEquiv.mk (inv f) sect' retr' adj'
-end IsEquiv
-
-namespace IsEquiv
-
-  variables {A B : Type} (f : A → B) (g : B → A)
-            (ret : Sect g f) (sec : Sect f g)
+  is_equiv.mk (inv f) sect' retr' adj'
+end is_equiv
 
+namespace is_equiv
   context
-  set_option unifier.max_steps 30000
-  --To construct an equivalence it suffices to state the proof that the inverse is a quasi-inverse.
-  definition adjointify : IsEquiv f :=
-    let sect' := (λx, ap g (ap f (inverse (sec x))) ⬝ ap g (ret (f x)) ⬝ sec x) in
-    let adj' := (λ (a : A),
+  parameters {A B : Type} (f : A → B) (g : B → A)
+            (ret : f ∘ g ∼ id) (sec : g ∘ f ∼ id)
+
+  definition adjointify_sect' : g ∘ f ∼ id :=
+    (λx, ap g (ap f (inverse (sec x))) ⬝ ap g (ret (f x)) ⬝ sec x)
+
+  definition adjointify_adj' : Π (x : A), ret (f x) ≈ ap f (adjointify_sect' x) :=
+    (λ (a : A),
       let fgretrfa := ap f (ap g (ret (f a))) in
       let fgfinvsect := ap f (ap g (ap f ((sec a)⁻¹))) in
       let fgfa := f (g (f a)) in
@@ -144,7 +100,7 @@ namespace IsEquiv
       have eq1 : ap f (sec a) ≈ _,
         from calc ap f (sec a)
               ≈ idp ⬝ ap f (sec a) : !concat_1p⁻¹
-          ... ≈ (ret (f a) ⬝ (ret (f a)⁻¹)) ⬝ ap f (sec a) : {!concat_pV⁻¹}
+          ... ≈ (ret (f a) ⬝ (ret (f a)⁻¹)) ⬝ ap f (sec a) : concat_pV
           ... ≈ ((ret (fgfa))⁻¹ ⬝ ap (f ∘ g) (ret (f a))) ⬝ ap f (sec a) : {!concat_pA1⁻¹}
           ... ≈ ((ret (fgfa))⁻¹ ⬝ fgretrfa) ⬝ ap f (sec a) : {ap_compose g f _}
           ... ≈ (ret (fgfa))⁻¹ ⬝ (fgretrfa ⬝ ap f (sec a)) : !concat_pp_p,
@@ -164,46 +120,51 @@ namespace IsEquiv
           ... ≈ retrfa⁻¹ ⬝ ap f ((ap g (ap f ((sec a)⁻¹)) ⬝ ap g (ret (f a))) ⬝ sec a) : {!ap_pp⁻¹},
       have eq4 : ret (f a) ≈ ap f ((ap g (ap f ((sec a)⁻¹)) ⬝ ap g (ret (f a))) ⬝ sec a),
         from moveR_M1 _ _ eq3,
-      eq4) in
-    IsEquiv.mk g ret sect' adj'
-  end
-end IsEquiv
+      eq4)
 
-namespace IsEquiv
+  definition adjointify : is_equiv f :=
+    is_equiv.mk g ret adjointify_sect' adjointify_adj'
+
+  end
+end is_equiv
+
+namespace is_equiv
   variables {A B: Type} (f : A → B)
 
   --The inverse of an equivalence is, again, an equivalence.
-  definition inv_closed [instance] [Hf : IsEquiv f] : (IsEquiv (inv f)) :=
+  definition inv_closed [instance] [Hf : is_equiv f] : (is_equiv (inv f)) :=
     adjointify (inv f) f (sect f) (retr f)
 
-end IsEquiv
+end is_equiv
 
-namespace IsEquiv
+namespace is_equiv
   variables {A : Type}
   section
-  variables {B C : Type} (f : A → B) {f' : A → B} [Hf : IsEquiv f]
+  variables {B C : Type} (f : A → B) {f' : A → B} [Hf : is_equiv f]
   include Hf
 
-  definition cancel_R (g : B → C) [Hgf : IsEquiv (g ∘ f)] : (IsEquiv g) :=
-    homotopic (comp_closed !inv_closed Hgf) (λb, ap g (retr f b))
+  definition cancel_R (g : B → C) [Hgf : is_equiv (g ∘ f)] : (is_equiv g) :=
+    have Hfinv [visible] : is_equiv (f⁻¹), from inv_closed f,
+    @homotopy_closed _ _ _ _ (compose (f⁻¹) (g ∘ f)) (λb, ap g (@retr _ _ f _ b))
 
-  definition cancel_L (g : C → A) [Hgf : IsEquiv (f ∘ g)] : (IsEquiv g) :=
-    homotopic (comp_closed Hgf !inv_closed) (λa, sect f (g a))
+  definition cancel_L (g : C → A) [Hgf : is_equiv (f ∘ g)] : (is_equiv g) :=
+    have Hfinv [visible] : is_equiv (f⁻¹), from inv_closed f,
+    @homotopy_closed _ _ _ _ (compose (f ∘ g) (f⁻¹)) (λa, sect f (g a))
 
   --Rewrite rules
   definition moveR_M {x : A} {y : B} (p : x ≈ (inv f) y) : (f x ≈ y) :=
-    (ap f p) ⬝ (retr f y)
+    (ap f p) ⬝ (@retr _ _ f _ y)
 
   definition moveL_M {x : A} {y : B} (p : (inv f) y ≈ x) : (y ≈ f x) :=
     (moveR_M f (p⁻¹))⁻¹
 
   definition moveR_V {x : B} {y : A} (p : x ≈ f y) : (inv f) x ≈ y :=
-    ap (inv f) p ⬝ sect f y
+    ap (f⁻¹) p ⬝ sect f y
 
   definition moveL_V {x : B} {y : A} (p : f y ≈ x) : y ≈ (inv f) x :=
     (moveR_V f (p⁻¹))⁻¹
 
-  definition ap_closed [instance] (x y : A) : IsEquiv (ap f) :=
+  definition ap_closed [instance] (x y : A) : is_equiv (ap f) :=
     adjointify (ap f)
       (λq, (inverse (sect f x)) ⬝ ap (f⁻¹) q ⬝ sect f y)
       (λq, !ap_pp
@@ -233,67 +194,72 @@ namespace IsEquiv
 
   definition equiv_rect_comp (P : B → Type)
       (df : Π (x : A), P (f x)) (x : A) : equiv_rect f P df (f x) ≈ df x :=
-    let eq1 := (apD df (sect f x)) in
     calc equiv_rect f P df (f x)
           ≈ transport P (retr f (f x)) (df (f⁻¹ (f x))) : idp
       ... ≈ transport P (ap f (sect f x)) (df (f⁻¹ (f x))) : adj f
       ... ≈ transport (P ∘ f) (sect f x) (df (f⁻¹ (f x))) : transport_compose
-      ... ≈ df x : eq1
+      ... ≈ df x : apD df (sect f x)
 
   end
 
   --Transporting is an equivalence
-  protected definition transport [instance] (P : A → Type) {x y : A} (p : x ≈ y) : (IsEquiv (transport P p)) :=
-    IsEquiv.mk (transport P (p⁻¹)) (transport_pV P p) (transport_Vp P p) (transport_pVp P p)
+  protected definition transport [instance] (P : A → Type) {x y : A} (p : x ≈ y) : (is_equiv (transport P p)) :=
+    is_equiv.mk (transport P (p⁻¹)) (transport_pV P p) (transport_Vp P p) (transport_pVp P p)
 
-end IsEquiv
+end is_equiv
+
+namespace equiv
+
+  instance [persistent] to_is_equiv
+
+  infix `≃`:25 := equiv
 
-namespace Equiv
   context
   parameters {A B C : Type} (eqf : A ≃ B)
 
-  private definition f : A → B := equiv_fun eqf
-  private definition Hf : IsEquiv f := equiv_isequiv eqf
+  private definition f : A → B := to_fun eqf
+  private definition Hf [instance] : is_equiv f := to_is_equiv eqf
 
-  protected definition id : A ≃ A := Equiv.mk id IsEquiv.id_closed
+  protected definition refl : A ≃ A := equiv.mk id is_equiv.id_is_equiv
 
-  protected theorem compose (eqg: B ≃ C) : A ≃ C :=
-    Equiv.mk ((equiv_fun eqg) ∘ f)
-             (IsEquiv.comp_closed Hf (equiv_isequiv eqg))
+  theorem trans (eqg: B ≃ C) : A ≃ C :=
+    equiv.mk ((to_fun eqg) ∘ f)
+             (is_equiv.compose f (to_fun eqg))
 
-  theorem path_closed (f' : A → B) (Heq : equiv_fun eqf ≈ f') : A ≃ B :=
-    Equiv.mk f' (IsEquiv.path_closed Hf Heq)
+  theorem path_closed (f' : A → B) (Heq : to_fun eqf ≈ f') : A ≃ B :=
+    equiv.mk f' (is_equiv.path_closed f Heq)
 
-  theorem inv_closed : B ≃ A :=
-    Equiv.mk (IsEquiv.inv f) !IsEquiv.inv_closed
+  theorem symm : B ≃ A :=
+    equiv.mk (is_equiv.inv f) !is_equiv.inv_closed
 
-  theorem cancel_R {g : B → C} (Hgf : IsEquiv (g ∘ f)) : B ≃ C :=
-    Equiv.mk g (IsEquiv.cancel_R f _)
+  theorem cancel_R (g : B → C) [Hgf : is_equiv (g ∘ f)] : B ≃ C :=
+    equiv.mk g (is_equiv.cancel_R f _)
 
-  theorem cancel_L {g : C → A} (Hgf : IsEquiv (f ∘ g)) : C ≃ A :=
-    Equiv.mk g (IsEquiv.cancel_L f _)
+  theorem cancel_L (g : C → A) [Hgf : is_equiv (f ∘ g)] : C ≃ A :=
+    equiv.mk g (is_equiv.cancel_L f _)
 
   protected theorem transport (P : A → Type) {x y : A} {p : x ≈ y} : (P x) ≃ (P y) :=
-    Equiv.mk (transport P p) (IsEquiv.transport P p)
+    equiv.mk (transport P p) (is_equiv.transport P p)
 
   end
 
   context
   parameters {A B : Type} (eqf eqg : A ≃ B)
 
-  private definition Hf [instance] : IsEquiv (equiv_fun eqf) := equiv_isequiv eqf
-  private definition Hg [instance] : IsEquiv (equiv_fun eqg) := equiv_isequiv eqg
+  private definition Hf [instance] : is_equiv (to_fun eqf) := to_is_equiv eqf
+  private definition Hg [instance] : is_equiv (to_fun eqg) := to_is_equiv eqg
 
+  --We need this theorem for the funext_from_ua proof
   theorem inv_eq (p : eqf ≈ eqg)
-      : IsEquiv.inv (equiv_fun eqf) ≈ IsEquiv.inv (equiv_fun eqg) :=
+      : is_equiv.inv (to_fun eqf) ≈ is_equiv.inv (to_fun eqg) :=
     path.rec_on p idp
 
   end
 
   -- calc enviroment
   -- Note: Calculating with substitutions needs univalence
-  calc_trans compose
-  calc_refl id
-  calc_symm inv_closed
+  calc_trans trans
+  calc_refl refl
+  calc_symm symm
 
-end Equiv
+end equiv
diff --git a/library/hott/equiv_precomp.lean b/library/hott/equiv_precomp.lean
index 376115ab5..ed38539bf 100644
--- a/library/hott/equiv_precomp.lean
+++ b/library/hott/equiv_precomp.lean
@@ -5,7 +5,7 @@
 import hott.equiv hott.axioms.funext
 open path function funext
 
-namespace IsEquiv
+namespace is_equiv
   context
 
   --Precomposition of arbitrary functions with f
@@ -15,15 +15,15 @@ namespace IsEquiv
   definition postcomp {A B : Type} (f : A → B) (C : Type) (l : C → A) : C → B := f ∘ l
 
   --Precomposing with an equivalence is an equivalence
-  definition precompose [instance] {A B : Type} (f : A → B) [F : funext] [Hf : IsEquiv f] (C : Type):
-      IsEquiv (precomp f C) :=
+  definition precompose [instance] {A B : Type} (f : A → B) [F : funext] [Hf : is_equiv f] (C : Type)
+      : is_equiv (precomp f C) :=
     adjointify (precomp f C) (λh, h ∘ f⁻¹)
       (λh, path_forall _ _ (λx, ap h (sect f x)))
       (λg, path_forall _ _ (λy, ap g (retr f y)))
 
   --Postcomposing with an equivalence is an equivalence
-  definition postcompose [instance] {A B : Type} (f : A → B) [F : funext] [Hf : IsEquiv f] (C : Type):
-      IsEquiv (postcomp f C) :=
+  definition postcompose [instance] {A B : Type} (f : A → B) [F : funext] [Hf : is_equiv f] (C : Type)
+      : is_equiv (postcomp f C) :=
     adjointify (postcomp f C) (λl, f⁻¹ ∘ l)
       (λh, path_forall _ _ (λx, retr f (h x)))
       (λg, path_forall _ _ (λy, sect f (g y)))
@@ -32,8 +32,8 @@ namespace IsEquiv
   --then that function is also an equivalence.  It's convenient to know
   --that we only need to assume the equivalence when the other type is
   --the domain or the codomain.
-  protected definition isequiv_precompose_eq {A B : Type} (f : A → B) (C D : Type) (Ceq : IsEquiv (precomp f C))
-      (Deq : IsEquiv (precomp f D)) (k : C → D) (h : A → C) :
+  protected definition isequiv_precompose_eq {A B : Type} (f : A → B) (C D : Type)
+      (Ceq : is_equiv (precomp f C)) (Deq : is_equiv (precomp f D)) (k : C → D) (h : A → C) :
       k ∘ (inv (precomp f C)) h ≈ (inv (precomp f D)) (k ∘ h) :=
     let invD := inv (precomp f D) in
     let invC := inv (precomp f C) in
@@ -42,40 +42,40 @@ namespace IsEquiv
 		... ≈ k ∘ (invC h) : !sect,
       eq1⁻¹
 
-  definition isequiv_precompose {A B : Type} (f : A → B) (Aeq : IsEquiv (precomp f A))
-      (Beq : IsEquiv (precomp f B)) : (IsEquiv f) :=
+  definition isequiv_precompose {A B : Type} (f : A → B) (Aeq : is_equiv (precomp f A))
+      (Beq : is_equiv (precomp f B)) : (is_equiv f) :=
     let invA := inv (precomp f A) in
     let invB := inv (precomp f B) in
-    let sect' : Sect (invA id) f := (λx,
+    let sect' : f ∘ (invA id) ∼ id  := (λx,
       calc f (invA id x) ≈ (f ∘ invA id) x : idp
 	... ≈ invB (f ∘ id) x : apD10 (!isequiv_precompose_eq)
 	... ≈ invB (precomp f B id) x : idp
 	... ≈ x : apD10 (sect (precomp f B) id))
       in
-    let retr' : Sect f (invA id) := (λx,
+    let retr' : (invA id) ∘ f ∼ id := (λx,
       calc invA id (f x) ≈ precomp f A (invA id) x : idp
 	... ≈ x : apD10 (retr (precomp f A) id)) in
     adjointify f (invA id) sect' retr'
 
   end
 
-end IsEquiv
+end is_equiv
 
 --Bundled versions of the previous theorems
-namespace Equiv
+namespace equiv
 
   definition precompose [F : funext] {A B C : Type} {eqf : A ≃ B}
       : (B → C) ≃ (A → C) :=
-    let f := equiv_fun eqf in
-    let Hf := equiv_isequiv eqf in
-    Equiv.mk (IsEquiv.precomp f C)
-      (@IsEquiv.precompose A B f F Hf C)
+    let f := to_fun eqf in
+    let Hf := to_is_equiv eqf in
+    equiv.mk (is_equiv.precomp f C)
+      (@is_equiv.precompose A B f F Hf C)
 
   definition postcompose [F : funext] {A B C : Type} {eqf : A ≃ B}
       : (C → A) ≃ (C → B) :=
-    let f := equiv_fun eqf in
-    let Hf := equiv_isequiv eqf in
-    Equiv.mk (IsEquiv.postcomp f C)
-      (@IsEquiv.postcompose A B f F Hf C)
+    let f := to_fun eqf in
+    let Hf := to_is_equiv eqf in
+    equiv.mk (is_equiv.postcomp f C)
+      (@is_equiv.postcompose A B f F Hf C)
 
-end Equiv
+end equiv
diff --git a/library/hott/funext_from_ua.lean b/library/hott/funext_from_ua.lean
index 94cca2b3d..d427baac0 100644
--- a/library/hott/funext_from_ua.lean
+++ b/library/hott/funext_from_ua.lean
@@ -5,47 +5,47 @@
 import hott.equiv hott.funext_varieties hott.axioms.ua hott.axioms.funext
 import data.prod data.sigma data.unit
 
-open path function prod sigma truncation Equiv IsEquiv unit ua_type
+open path function prod sigma truncation equiv is_equiv unit ua_type
 
 context
   universe variables l
   parameter [UA : ua_type.{l+1}]
 
   protected theorem ua_isequiv_postcompose {A B : Type.{l+1}} {C : Type}
-      {w : A → B} {H0 : IsEquiv w} : IsEquiv (@compose C A B w) :=
-    let w' := Equiv.mk w H0 in
-    let eqinv : A ≈ B := ((@IsEquiv.inv _ _ _ (@ua_type.inst UA A B)) w') in
+      {w : A → B} {H0 : is_equiv w} : is_equiv (@compose C A B w) :=
+    let w' := equiv.mk w H0 in
+    let eqinv : A ≈ B := ((@is_equiv.inv _ _ _ (@ua_type.inst UA A B)) w') in
     let eq' := equiv_path eqinv in
-    IsEquiv.adjointify (@compose C A B w)
-      (@compose C B A (IsEquiv.inv w))
+    is_equiv.adjointify (@compose C A B w)
+      (@compose C B A (is_equiv.inv w))
       (λ (x : C → B),
         have eqretr : eq' ≈ w',
           from (@retr _ _ (@equiv_path A B) (@ua_type.inst UA A B) w'),
-        have invs_eq : (equiv_fun eq')⁻¹ ≈ (equiv_fun w')⁻¹,
+        have invs_eq : (to_fun eq')⁻¹ ≈ (to_fun w')⁻¹,
           from inv_eq eq' w' eqretr,
-        have eqfin : (equiv_fun eq') ∘ ((equiv_fun eq')⁻¹ ∘ x) ≈ x,
+        have eqfin : (to_fun eq') ∘ ((to_fun eq')⁻¹ ∘ x) ≈ x,
           from (λ p,
             (@path.rec_on Type.{l+1} A
-              (λ B' p', Π (x' : C → B'), (equiv_fun (equiv_path p'))
-                ∘ ((equiv_fun (equiv_path p'))⁻¹ ∘ x') ≈ x')
+              (λ B' p', Π (x' : C → B'), (to_fun (equiv_path p'))
+                ∘ ((to_fun (equiv_path p'))⁻¹ ∘ x') ≈ x')
               B p (λ x', idp))
             ) eqinv x,
-        have eqfin' : (equiv_fun w') ∘ ((equiv_fun eq')⁻¹ ∘ x) ≈ x,
+        have eqfin' : (to_fun w') ∘ ((to_fun eq')⁻¹ ∘ x) ≈ x,
           from eqretr ▹ eqfin,
-        have eqfin'' : (equiv_fun w') ∘ ((equiv_fun w')⁻¹ ∘ x) ≈ x,
+        have eqfin'' : (to_fun w') ∘ ((to_fun w')⁻¹ ∘ x) ≈ x,
           from invs_eq ▹ eqfin',
         eqfin''
       )
       (λ (x : C → A),
         have eqretr : eq' ≈ w',
           from (@retr _ _ (@equiv_path A B) ua_type.inst w'),
-        have invs_eq : (equiv_fun eq')⁻¹ ≈ (equiv_fun w')⁻¹,
+        have invs_eq : (to_fun eq')⁻¹ ≈ (to_fun w')⁻¹,
           from inv_eq eq' w' eqretr,
-        have eqfin : (equiv_fun eq')⁻¹ ∘ ((equiv_fun eq') ∘ x) ≈ x,
+        have eqfin : (to_fun eq')⁻¹ ∘ ((to_fun eq') ∘ x) ≈ x,
           from (λ p, path.rec_on p idp) eqinv,
-        have eqfin' : (equiv_fun eq')⁻¹ ∘ ((equiv_fun w') ∘ x) ≈ x,
+        have eqfin' : (to_fun eq')⁻¹ ∘ ((to_fun w') ∘ x) ≈ x,
           from eqretr ▹ eqfin,
-        have eqfin'' : (equiv_fun w')⁻¹ ∘ ((equiv_fun w') ∘ x) ≈ x,
+        have eqfin'' : (to_fun w')⁻¹ ∘ ((to_fun w') ∘ x) ≈ x,
           from invs_eq ▹ eqfin',
         eqfin''
       )
@@ -56,22 +56,22 @@ context
     := Σ xy : B × B, pr₁ xy ≈ pr₂ xy
 
   protected definition isequiv_src_compose {A B : Type}
-      : @IsEquiv (A → diagonal B)
+      : @is_equiv (A → diagonal B)
                  (A → B)
                  (compose (pr₁ ∘ dpr1)) :=
     @ua_isequiv_postcompose _ _ _ (pr₁ ∘ dpr1)
-        (IsEquiv.adjointify (pr₁ ∘ dpr1)
+        (is_equiv.adjointify (pr₁ ∘ dpr1)
           (λ x, dpair (x , x) idp) (λx, idp)
           (λ x, sigma.rec_on x
             (λ xy, prod.rec_on xy
               (λ b c p, path.rec_on p idp))))
 
   protected definition isequiv_tgt_compose {A B : Type}
-      : @IsEquiv (A → diagonal B)
+      : @is_equiv (A → diagonal B)
                  (A → B)
                  (compose (pr₂ ∘ dpr1)) :=
     @ua_isequiv_postcompose _ _ _ (pr2 ∘ dpr1)
-        (IsEquiv.adjointify (pr2 ∘ dpr1)
+        (is_equiv.adjointify (pr2 ∘ dpr1)
           (λ x, dpair (x , x) idp) (λx, idp)
           (λ x, sigma.rec_on x
             (λ xy, prod.rec_on xy
@@ -83,13 +83,13 @@ context
         let d := λ (x : A), dpair (f x , f x) idp in
         let e := λ (x : A), dpair (f x , g x) (p x) in
         let precomp1 :=  compose (pr₁ ∘ dpr1) in
-        have equiv1 [visible] : IsEquiv precomp1,
+        have equiv1 [visible] : is_equiv precomp1,
           from @isequiv_src_compose A B,
-        have equiv2 [visible] : Π x y, IsEquiv (ap precomp1),
-          from IsEquiv.ap_closed precomp1,
+        have equiv2 [visible] : Π x y, is_equiv (ap precomp1),
+          from is_equiv.ap_closed precomp1,
         have H' : Π (x y : A → diagonal B),
             pr₁ ∘ dpr1 ∘ x ≈ pr₁ ∘ dpr1 ∘ y → x ≈ y,
-          from (λ x y, IsEquiv.inv (ap precomp1)),
+          from (λ x y, is_equiv.inv (ap precomp1)),
         have eq2 : pr₁ ∘ dpr1 ∘ d ≈ pr₁ ∘ dpr1 ∘ e,
           from idp,
         have eq0 : d ≈ e,
@@ -110,7 +110,7 @@ theorem ua_implies_weak_funext [ua3 : ua_type.{k+1}] [ua4 : ua_type.{k+2}] : wea
   have pequiv : Π (x : A), P x ≃ U x,
     from (λ x, @equiv_contr_unit(P x) (allcontr x)),
   have psim : Π (x : A), P x ≈ U x,
-    from (λ x, @IsEquiv.inv _ _
+    from (λ x, @is_equiv.inv _ _
       equiv_path ua_type.inst (pequiv x)),
   have p : P ≈ U,
     from @ua_implies_funext_nondep _ A Type P U psim,
diff --git a/library/hott/funext_varieties.lean b/library/hott/funext_varieties.lean
index f96f88319..37386beb8 100644
--- a/library/hott/funext_varieties.lean
+++ b/library/hott/funext_varieties.lean
@@ -27,9 +27,9 @@ definition weak_funext.{l k} :=
 -- TODO: Get class inference to work locally
 definition funext_implies_naive_funext [F : funext] : naive_funext :=
   (λ A P f g h,
-    have Fefg: IsEquiv (@apD10 A P f g),
+    have Fefg: is_equiv (@apD10 A P f g),
       from (@funext.ap F A P f g),
-    have eq1 : _, from (@IsEquiv.inv _ _ (@apD10 A P f g) Fefg h),
+    have eq1 : _, from (@is_equiv.inv _ _ (@apD10 A P f g) Fefg h),
     eq1
   )
 
@@ -100,11 +100,11 @@ theorem weak_funext_implies_funext (wf : weak_funext.{l+1 k+1}) : funext.{l+1 k+
       proof htpy_ind_beta _ f eq_to_f idp qed,
     have t2 : apD10 (sim2path f (idhtpy f)) ≈ (idhtpy f),
       proof ap apD10 t1 qed,
-    have sect : Sect (sim2path g) apD10,
+    have sect : apD10 ∘ (sim2path g) ∼ id,
       proof (htpy_ind _ f (λ g' x, apD10 (sim2path g' x) ≈ x) t2) g qed,
-    have retr : Sect apD10 (sim2path g),
+    have retr : (sim2path g) ∘ apD10 ∼ id,
       from (λ h, path.rec_on h (htpy_ind_beta _ f _ idp)),
-    IsEquiv.adjointify apD10 (sim2path g) sect retr)
+    is_equiv.adjointify apD10 (sim2path g) sect retr)
 
 definition naive_funext_implies_funext : naive_funext -> funext :=
   compose weak_funext_implies_funext naive_funext_implies_weak_funext
diff --git a/library/hott/path.lean b/library/hott/path.lean
index 33abbaaf0..5850fbc36 100644
--- a/library/hott/path.lean
+++ b/library/hott/path.lean
@@ -193,10 +193,10 @@ path.rec_on p idp
 
 definition ap01 := ap
 
-definition pointwise_paths {A : Type} {P : A → Type} (f g : Πx, P x) : Type :=
+definition homotopy [reducible] {A : Type} {P : A → Type} (f g : Πx, P x) : Type :=
 Πx : A, f x ≈ g x
 
-notation f ∼ g := pointwise_paths f g
+notation f ∼ g := homotopy f g
 
 definition apD10 {A} {B : A → Type} {f g : Πx, B x} (H : f ≈ g) : f ∼ g :=
 λx, path.rec_on H idp
diff --git a/library/hott/trunc.lean b/library/hott/trunc.lean
index 4cf136528..6240c4c70 100644
--- a/library/hott/trunc.lean
+++ b/library/hott/trunc.lean
@@ -205,47 +205,48 @@ namespace truncation
   /- interaction with equivalences -/
 
   section
-  open IsEquiv Equiv
+  open is_equiv equiv
 
   --should we remove the following two theorems as they are special cases of "trunc_equiv"
-  definition equiv_preserves_contr (f : A → B) [Hf : IsEquiv f] [HA: is_contr A] : (is_contr B) :=
-  is_contr.mk (f (center A)) (λp, moveR_M f !contr)
+  definition equiv_preserves_contr (f : A → B) [Hf : is_equiv f] [HA: is_contr A] : (is_contr B) :=
+    is_contr.mk (f (center A)) (λp, moveR_M f !contr)
 
-  theorem contr_equiv (f : A ≃ B) [HA: is_contr A] : is_contr B :=
-  equiv_preserves_contr (equiv_fun f)
+  set_option elaborator.trace_instances true
+  theorem contr_equiv (H : A ≃ B) [HA: is_contr A] : is_contr B :=
+    @equiv_preserves_contr _ _ (to_fun H) (to_is_equiv H) _
 
   definition contr_equiv_contr [HA : is_contr A] [HB : is_contr B] : A ≃ B :=
-  Equiv.mk
+  equiv.mk
     (λa, center B)
-    (IsEquiv.adjointify (λa, center B) (λb, center A) contr contr)
+    (is_equiv.adjointify (λa, center B) (λb, center A) contr contr)
 
-  definition trunc_equiv (n : trunc_index) (f : A → B) [H : IsEquiv f] [HA : is_trunc n A]
+  definition trunc_equiv (n : trunc_index) (f : A → B) [H : is_equiv f] [HA : is_trunc n A]
       : is_trunc n B :=
   trunc_index.rec_on n
-    (λA (HA : is_contr A) B f (H : IsEquiv f), !equiv_preserves_contr)
-    (λn IH A (HA : is_trunc n.+1 A) B f (H : IsEquiv f), @is_trunc_succ _ _ (λ x y : B,
+    (λA (HA : is_contr A) B f (H : is_equiv f), !equiv_preserves_contr)
+    (λn IH A (HA : is_trunc n.+1 A) B f (H : is_equiv f), @is_trunc_succ _ _ (λ x y : B,
       IH (f⁻¹ x ≈ f⁻¹ y) !succ_is_trunc (x ≈ y) ((ap (f⁻¹))⁻¹) !inv_closed))
     A HA B f H
 
   definition trunc_equiv' (n : trunc_index) (f : A ≃ B) [HA : is_trunc n A] : is_trunc n B :=
-  trunc_equiv n (equiv_fun f)
+  trunc_equiv n (to_fun f)
 
   definition isequiv_iff_hprop [HA : is_hprop A] [HB : is_hprop B] (f : A → B) (g : B → A)
-      : IsEquiv f :=
-  IsEquiv.adjointify f g (λb, !is_hprop.elim) (λa, !is_hprop.elim)
+      : is_equiv f :=
+  is_equiv.adjointify f g (λb, !is_hprop.elim) (λa, !is_hprop.elim)
 
   -- definition equiv_iff_hprop_uncurried [HA : is_hprop A] [HB : is_hprop B] : (A ↔ B) → (A ≃ B)  := sorry
 
   definition equiv_iff_hprop [HA : is_hprop A] [HB : is_hprop B] (f : A → B) (g : B → A) : A ≃ B :=
-  Equiv.mk f (isequiv_iff_hprop f g)
+  equiv.mk f (isequiv_iff_hprop f g)
   end
 
   /- interaction with the Unit type -/
 
   -- A contractible type is equivalent to [Unit]. *)
   definition equiv_contr_unit [H : is_contr A] : A ≃ unit :=
-    Equiv.mk (λ (x : A), ⋆)
-      (IsEquiv.mk (λ (u : unit), center A)
+    equiv.mk (λ (x : A), ⋆)
+      (is_equiv.mk (λ (u : unit), center A)
         (λ (u : unit), unit.rec_on u idp)
         (λ (x : A), contr x)
         (λ (x : A), (!ap_const)⁻¹))
diff --git a/library/hott/types/prod.lean b/library/hott/types/prod.lean
index 65d8f6204..3142af488 100644
--- a/library/hott/types/prod.lean
+++ b/library/hott/types/prod.lean
@@ -8,7 +8,7 @@ Theorems about products
 -/
 
 import ..trunc data.prod
-open path Equiv IsEquiv truncation prod
+open path equiv is_equiv truncation prod
 
 variables {A A' B B' C D : Type}
           {a a' a'' : A} {b b₁ b₂ b' b'' : B} {u v w : A × B}
@@ -21,15 +21,13 @@ namespace prod
 
   /- Symmetry -/
 
-  definition isequiv_prod_symm [instance] (A B : Type) : IsEquiv (@flip A B) :=
+  definition isequiv_prod_symm [instance] (A B : Type) : is_equiv (@flip A B) :=
   adjointify flip
              flip
              (λu, destruct u (λb a, idp))
              (λu, destruct u (λa b, idp))
 
   definition equiv_prod_symm (A B : Type) : A × B ≃ B × A :=
-  Equiv.mk flip _
-
-  check typeof idp : flip (flip (a,b)) ≈ (a,b)
+    equiv.mk flip _
 
 end prod
diff --git a/library/hott/types/sigma.lean b/library/hott/types/sigma.lean
index 42bd425c8..656eabad1 100644
--- a/library/hott/types/sigma.lean
+++ b/library/hott/types/sigma.lean
@@ -8,7 +8,7 @@ Theorems about sigma-types (dependent sums)
 -/
 
 import ..trunc .prod
-open path sigma sigma.ops Equiv IsEquiv
+open path sigma sigma.ops equiv is_equiv
 
 namespace sigma
   -- remove the ₁'s (globally)
@@ -104,17 +104,17 @@ namespace sigma
 
   definition transport_pr1_path_sigma_uncurried {B' : A → Type} (pq : Σ(p : u.1 ≈ v.1), p ▹ u.2 ≈ v.2)
       : transport (λx, B' x.1) (@path_sigma_uncurried A B u v pq) ≈ transport B' pq.1 :=
-  destruct pq transport_pr1_path_sigma
+    destruct pq transport_pr1_path_sigma
 
   definition isequiv_path_sigma /-[instance]-/ (u v : Σa, B a)
-      : IsEquiv (@path_sigma_uncurried A B u v) :=
+      : is_equiv (@path_sigma_uncurried A B u v) :=
   adjointify path_sigma_uncurried
              (λp, ⟨p..1, p..2⟩)
              eta_path_sigma_uncurried
              dpair_path_sigma_uncurried
 
   definition equiv_path_sigma (u v : Σa, B a) : (Σ(p : u.1 ≈ v.1),  p ▹ u.2 ≈ v.2) ≃ (u ≈ v) :=
-  Equiv.mk path_sigma_uncurried !isequiv_path_sigma
+    equiv.mk path_sigma_uncurried !isequiv_path_sigma
 
   definition path_sigma_dpair_pp_pp (p1 : a  ≈ a' ) (q1 : p1 ▹ b  ≈ b' )
                                     (p2 : a' ≈ a'') (q2 : p2 ▹ b' ≈ b'') :
@@ -239,39 +239,39 @@ namespace sigma
   /- Equivalences -/
 
   --remove explicit arguments of IsEquiv
-  definition isequiv_functor_sigma [H1 : IsEquiv f] [H2 : Π a, @IsEquiv (B a) (B' (f a)) (g a)]
-      : IsEquiv (functor_sigma f g) :=
-  adjointify (functor_sigma f g)
+  definition isequiv_functor_sigma [H1 : is_equiv f] [H2 : Π a, @is_equiv (B a) (B' (f a)) (g a)]
+      : is_equiv (functor_sigma f g) :=
+  /-adjointify (functor_sigma f g)
              (functor_sigma (f⁻¹) (λ(x : A') (y : B' x), ((g (f⁻¹ x))⁻¹ ((retr f x)⁻¹ ▹ y))))
-             sorry
+             sorry-/
              sorry
 
-  definition equiv_functor_sigma [H1 : IsEquiv f] [H2 : Π a, IsEquiv (g a)] : (Σa, B a) ≃ (Σa', B' a') :=
-  Equiv.mk (functor_sigma f g) !isequiv_functor_sigma
+  definition equiv_functor_sigma [H1 : is_equiv f] [H2 : Π a, is_equiv (g a)] : (Σa, B a) ≃ (Σa', B' a') :=
+  equiv.mk (functor_sigma f g) !isequiv_functor_sigma
 
   context --remove
   irreducible inv function.compose --remove
-  definition equiv_functor_sigma' (Hf : A ≃ A') (Hg : Π a, B a ≃ B' (equiv_fun Hf a)) :
+  definition equiv_functor_sigma' (Hf : A ≃ A') (Hg : Π a, B a ≃ B' (to_fun Hf a)) :
       (Σa, B a) ≃ (Σa', B' a') :=
-  equiv_functor_sigma (equiv_fun Hf) (λ a, equiv_fun (Hg a))
+  equiv_functor_sigma (to_fun Hf) (λ a, to_fun (Hg a))
   end --remove
 
   /- definition 3.11.9(i): Summing up a contractible family of types does nothing. -/
   open truncation
   definition isequiv_pr1_contr [instance] (B : A → Type) [H : Π a, is_contr (B a)]
-      : IsEquiv (@dpr1 A B) :=
+      : is_equiv (@dpr1 A B) :=
   adjointify dpr1
              (λa, ⟨a, !center⟩)
              (λa, idp)
              (λu, path_sigma idp !contr)
 
   definition equiv_sigma_contr [H : Π a, is_contr (B a)] : (Σa, B a) ≃ A :=
-  Equiv.mk dpr1 _
+  equiv.mk dpr1 _
 
   /- definition 3.11.9(ii): Dually, summing up over a contractible type does nothing. -/
 
   definition equiv_contr_sigma (B : A → Type) [H : is_contr A] : (Σa, B a) ≃ B (center A) :=
-  Equiv.mk _ (adjointify
+  equiv.mk _ (adjointify
     (λu, contr u.1⁻¹ ▹ u.2)
     (λb, ⟨!center, b⟩)
     (λb, ap (λx, x ▹ b) !path2_contr)
@@ -292,7 +292,7 @@ namespace sigma
   --               apply (destruct v), intros (b, c),
   --               apply idp,
   -- end
-  Equiv.mk _ (adjointify
+  equiv.mk _ (adjointify
     (λav, ⟨⟨av.1, av.2.1⟩, av.2.2⟩)
     (λuc, ⟨uc.1.1, uc.1.2, !eta_sigma⁻¹ ▹ uc.2⟩)
     proof (λuc, destruct uc (λu, destruct u (λa b c, idp))) qed
@@ -300,7 +300,7 @@ namespace sigma
 
   open prod
   definition equiv_sigma_prod (C : (A × A') → Type) : (Σa a', C (a,a')) ≃ (Σu, C u) :=
-  Equiv.mk _ (adjointify
+  equiv.mk _ (adjointify
     (λav, ⟨(av.1, av.2.1), av.2.2⟩)
     (λuc, ⟨pr₁ (uc.1), pr₂ (uc.1), !eta_prod⁻¹ ▹ uc.2⟩)
     proof (λuc, destruct uc (λu, prod.destruct u (λa b c, idp))) qed
@@ -313,14 +313,14 @@ namespace sigma
   calc
     (Σa a', C (a, a')) ≃ Σu, C u : equiv_sigma_prod
                  ... ≃ Σv, C (flip v) : equiv_functor_sigma' !equiv_prod_symm
-                                          (λu, prod.destruct u (λa a', Equiv.id))
+                                          (λu, prod.destruct u (λa a', equiv.refl))
                  ... ≃ (Σa' a, C (a, a')) : equiv_sigma_prod
 
   definition equiv_sigma_symm (C : A → A' → Type) : (Σa a', C a a') ≃ (Σa' a, C a a') :=
   sigma.equiv_sigma_symm_prod (λu, C (pr1 u) (pr2 u))
 
   definition equiv_sigma0_prod (A B : Type) : (Σ(a : A), B) ≃ A × B :=
-  Equiv.mk _ (adjointify
+  equiv.mk _ (adjointify
     (λs, (s.1, s.2))
     (λp, ⟨pr₁ p, pr₂ p⟩)
     proof (λp, prod.destruct p (λa b, idp)) qed
@@ -340,7 +340,7 @@ begin
   apply (truncation.trunc_index.rec_on n),
     intros (A, B, HA, HB),
       apply trunc_equiv',
-        apply Equiv.inv_closed,
+        apply equiv.symm,
           apply equiv_contr_sigma, apply HA,
       apply HB,
      intros (n, IH, A, B, HA, HB),