diff --git a/hott/algebra/category/constructions/functor.hlean b/hott/algebra/category/constructions/functor.hlean
index 72c2fd31c..0ecfecc7b 100644
--- a/hott/algebra/category/constructions/functor.hlean
+++ b/hott/algebra/category/constructions/functor.hlean
@@ -96,7 +96,7 @@ namespace category
                   (@componentwise_is_iso _ _ _ _ (to_hom η) (struct η) c)
 
   definition componentwise_iso_id (c : C) : componentwise_iso (iso.refl F) c = iso.refl (F c) :=
-  iso.eq_mk (idpath (ID (F c)))
+  iso_eq (idpath (ID (F c)))
 
   definition componentwise_iso_iso_of_eq (p : F = G) (c : C)
     : componentwise_iso (iso_of_eq p) c = iso_of_eq (ap010 to_fun_ob p c) :=
@@ -133,8 +133,8 @@ namespace category
 
     definition iso_of_eq_eq_of_iso (η : F ≅ G) : iso_of_eq (eq_of_iso η) = η :=
     begin
-    apply iso.eq_mk,
-    apply nat_trans_eq_mk,
+    apply iso_eq,
+    apply nat_trans_eq,
     intro c,
     rewrite natural_map_hom_of_eq, esimp [eq_of_iso],
     rewrite ap010_functor_eq, esimp [hom_of_eq,eq_of_iso_ob],
diff --git a/hott/algebra/category/constructions/hset.hlean b/hott/algebra/category/constructions/hset.hlean
index f15113d26..9af0ee12d 100644
--- a/hott/algebra/category/constructions/hset.hlean
+++ b/hott/algebra/category/constructions/hset.hlean
@@ -42,8 +42,8 @@ namespace category
 
     definition is_equiv_iso_of_equiv (A B : Precategory_hset) : is_equiv (@iso_of_equiv A B) :=
     adjointify _ (λf, equiv_of_iso f)
-                 (λf, iso.eq_mk idp)
-                 (λf, equiv.eq_mk idp)
+                 (λf, iso_eq idp)
+                 (λf, equiv_eq idp)
     local attribute is_equiv_iso_of_equiv [instance]
 
     open sigma.ops
@@ -66,8 +66,8 @@ namespace category
                            (iso.to_inv f)
                            (ap10 (right_inverse (to_hom f)))
                            (ap10 (left_inverse  (to_hom f))))
-             (λf, iso.eq_mk idp)
-             (λf, equiv.eq_mk idp)
+             (λf, iso_eq idp)
+             (λf, equiv_eq idp)
 
     definition equiv_eq_iso (A B : Precategory_hset) : (A ≃ B) = (A ≅ B) :=
     ua !equiv_equiv_iso
diff --git a/hott/algebra/category/functor.hlean b/hott/algebra/category/functor.hlean
index 976833de5..9791a9fc1 100644
--- a/hott/algebra/category/functor.hlean
+++ b/hott/algebra/category/functor.hlean
@@ -191,9 +191,9 @@ namespace functor
     exact r,
   end
 
-  -- definition ap010_functor_eq_mk' {F₁ F₂ : C ⇒ D} (p : to_fun_ob F₁ = to_fun_ob F₂)
+  -- definition ap010_functor_eq' {F₁ F₂ : C ⇒ D} (p : to_fun_ob F₁ = to_fun_ob F₂)
   --   (q : p ▹ F₁ = F₂) (c : C) :
-  --   ap to_fun_ob (functor_eq_mk (apd10 p) (λa b f, _)) = p := sorry
+  --   ap to_fun_ob (functor_eq (apd10 p) (λa b f, _)) = p := sorry
   -- begin
   --   cases F₂, revert q, apply (homotopy.rec_on p), clear p, esimp, intros (p, q),
   --   cases p, clears (e_1, e_2),
diff --git a/hott/algebra/category/iso.hlean b/hott/algebra/category/iso.hlean
index a40604e6c..bf7965446 100644
--- a/hott/algebra/category/iso.hlean
+++ b/hott/algebra/category/iso.hlean
@@ -154,12 +154,12 @@ namespace iso
   protected definition trans ⦃a b c : ob⦄ (H1 : a ≅ b) (H2 : b ≅ c) : a ≅ c :=
   mk (to_hom H2 ∘ to_hom H1)
 
-  protected definition eq_mk' {f f' : a ⟶ b} [H : is_iso f] [H' : is_iso f'] (p : f = f')
+  definition iso_mk_eq {f f' : a ⟶ b} [H : is_iso f] [H' : is_iso f'] (p : f = f')
       : iso.mk f = iso.mk f' :=
   apd011 iso.mk p !is_hprop.elim
 
-  protected definition eq_mk {f f' : a ≅ b} (p : to_hom f = to_hom f') : f = f' :=
-  by (cases f; cases f'; apply (iso.eq_mk' p))
+  definition iso_eq {f f' : a ≅ b} (p : to_hom f = to_hom f') : f = f' :=
+  by (cases f; cases f'; apply (iso_mk_eq p))
 
   -- The structure for isomorphism can be characterized up to equivalence by a sigma type.
   protected definition sigma_char ⦃a b : ob⦄ : (Σ (f : hom a b), is_iso f) ≃ (a ≅ b) :=
@@ -193,7 +193,7 @@ namespace iso
 
   definition iso_of_eq_con (p : a = b) (q : b = c)
     : iso_of_eq (p ⬝ q) = iso.trans (iso_of_eq p) (iso_of_eq q) :=
-  eq.rec_on q (eq.rec_on p (iso.eq_mk !id_comp⁻¹))
+  eq.rec_on q (eq.rec_on p (iso_eq !id_comp⁻¹))
 
   section
     open funext
diff --git a/hott/algebra/category/nat_trans.hlean b/hott/algebra/category/nat_trans.hlean
index b325624e5..b703e93af 100644
--- a/hott/algebra/category/nat_trans.hlean
+++ b/hott/algebra/category/nat_trans.hlean
@@ -38,25 +38,25 @@ namespace nat_trans
   protected definition ID [reducible] {C D : Precategory} (F : functor C D) : nat_trans F F :=
   id
 
-  definition nat_trans_eq_mk' {η₁ η₂ : Π (a : C), hom (F a) (G a)}
+  definition nat_trans_mk_eq {η₁ η₂ : Π (a : C), hom (F a) (G a)}
     (nat₁ : Π (a b : C) (f : hom a b), G f ∘ η₁ a = η₁ b ∘ F f)
     (nat₂ : Π (a b : C) (f : hom a b), G f ∘ η₂ a = η₂ b ∘ F f)
     (p : η₁ ∼ η₂)
       : nat_trans.mk η₁ nat₁ = nat_trans.mk η₂ nat₂ :=
   apd011 nat_trans.mk (eq_of_homotopy p) !is_hprop.elim
 
-  definition nat_trans_eq_mk {η₁ η₂ : F ⟹ G} : natural_map η₁ ∼ natural_map η₂ → η₁ = η₂ :=
-  nat_trans.rec_on η₁ (λf₁ nat₁, nat_trans.rec_on η₂ (λf₂ nat₂ p, !nat_trans_eq_mk' p))
+  definition nat_trans_eq {η₁ η₂ : F ⟹ G} : natural_map η₁ ∼ natural_map η₂ → η₁ = η₂ :=
+  nat_trans.rec_on η₁ (λf₁ nat₁, nat_trans.rec_on η₂ (λf₂ nat₂ p, !nat_trans_mk_eq p))
 
   protected definition assoc (η₃ : H ⟹ I) (η₂ : G ⟹ H) (η₁ : F ⟹ G) :
       η₃ ∘n (η₂ ∘n η₁) = (η₃ ∘n η₂) ∘n η₁ :=
-  nat_trans_eq_mk (λa, !assoc)
+  nat_trans_eq (λa, !assoc)
 
   protected definition id_left (η : F ⟹ G) : id ∘n η = η :=
-  nat_trans_eq_mk (λa, !id_left)
+  nat_trans_eq (λa, !id_left)
 
   protected definition id_right (η : F ⟹ G) : η ∘n id = η :=
-  nat_trans_eq_mk (λa, !id_right)
+  nat_trans_eq (λa, !id_right)
 
   protected definition sigma_char (F G : C ⇒ D) :
     (Σ (η : Π (a : C), hom (F a) (G a)), Π (a b : C) (f : hom a b), G f ∘ η a = η b ∘ F f) ≃  (F ⟹ G) :=
@@ -69,7 +69,7 @@ namespace nat_trans
           fapply sigma.mk,
             intro a, exact (H a),
           intros [a, b, f], exact (naturality H f),
-    intro η, apply nat_trans_eq_mk, intro a, apply idp,
+    intro η, apply nat_trans_eq, intro a, apply idp,
     intro S,
     fapply sigma_eq,
       apply eq_of_homotopy, intro a,
@@ -98,21 +98,21 @@ namespace nat_trans
 
   definition functor_nat_trans_compose_commute (η : F ⟹ G) (θ : F' ⟹ G')
     : (θ ∘nf G) ∘n (F' ∘fn η) = (G' ∘fn η) ∘n (θ ∘nf F) :=
-  nat_trans_eq_mk (λc, (naturality θ (η c))⁻¹)
+  nat_trans_eq (λc, (naturality θ (η c))⁻¹)
 
   definition fn_n_distrib (F' : D ⇒ E) (η : G ⟹ H) (θ : F ⟹ G)
     : F' ∘fn (η ∘n θ) = (F' ∘fn η) ∘n (F' ∘fn θ) :=
-  nat_trans_eq_mk (λc, !respect_comp)
+  nat_trans_eq (λc, !respect_comp)
 
   definition n_nf_distrib (η : G ⟹ H) (θ : F ⟹ G) (F' : B ⇒ C)
     : (η ∘n θ) ∘nf F' = (η ∘nf F') ∘n (θ ∘nf F') :=
-  nat_trans_eq_mk (λc, idp)
+  nat_trans_eq (λc, idp)
 
   definition fn_id (F' : D ⇒ E) : F' ∘fn nat_trans.ID F = nat_trans.id :=
-  nat_trans_eq_mk (λc, !respect_id)
+  nat_trans_eq (λc, !respect_id)
 
   definition id_nf (F' : B ⇒ C) : nat_trans.ID F ∘nf F' = nat_trans.id :=
-  nat_trans_eq_mk (λc, idp)
+  nat_trans_eq (λc, idp)
 
   definition id_fn (η : G ⟹ H) (c : C) : (functor.id ∘fn η) c = η c :=
   idp
diff --git a/hott/algebra/category/precategory.hlean b/hott/algebra/category/precategory.hlean
index f75137a39..f16640539 100644
--- a/hott/algebra/category/precategory.hlean
+++ b/hott/algebra/category/precategory.hlean
@@ -85,9 +85,6 @@ namespace category
     definition homset [reducible] (x y : ob) : hset :=
     hset.mk (hom x y) _
 
-    -- definition is_hprop_eq_hom [instance] : is_hprop (f = f') :=
-    -- !is_trunc_eq
-
   end basic_lemmas
   section squares
     parameters {ob : Type} [C : precategory ob]
@@ -165,11 +162,7 @@ namespace category
 
   /-Characterization of paths between precategories-/
 
-  -- auxiliary definition for speeding up precategory_eq_mk
-  private definition is_hprop_pi (A : Type) (B : A → Type) (H : Π (a : A), is_hprop (B a)) : is_hprop (Π (x : A), B x) :=
-  is_trunc_pi B (-2 .+1)
-
-  definition precategory_eq_mk (ob : Type)
+  definition precategory_mk'_eq (ob : Type)
     (hom1 : ob → ob → Type)
     (hom2 : ob → ob → Type)
     (homH1 : Π(a b : ob), is_hset (hom1 a b))
@@ -203,7 +196,7 @@ namespace category
     repeat (apply is_hprop.elim),
   end
 
-  definition precategory_eq_mk' (ob : Type)
+  definition precategory_eq (ob : Type)
     (C D : precategory ob)
     (p : @hom ob C = @hom ob D)
     (q : transport (λ x, Πa b c, x b c → x a b → x a c) p
@@ -211,10 +204,10 @@ namespace category
     (r : transport (λ x, Πa, x a a) p (@ID ob C) = @ID ob D) : C = D :=
   begin
     cases C, cases D,
-    apply precategory_eq_mk, apply q, apply r,
+    apply precategory_mk'_eq, apply q, apply r,
   end
 
-  definition precategory_eq_mk'' (ob : Type)
+  definition precategory_mk_eq (ob : Type)
     (hom1 : ob → ob → Type)
     (hom2 : ob → ob → Type)
     (homH1 : Π(a b : ob), is_hset (hom1 a b))
@@ -240,7 +233,7 @@ namespace category
     precategory.mk hom1 comp1 ID1 assoc1 id_left1 id_right1
     = precategory.mk hom2 comp2 ID2 assoc2 id_left2 id_right2 :=
   begin
-    fapply precategory_eq_mk,
+    fapply precategory_eq,
         apply eq_of_homotopy, intros,
         apply eq_of_homotopy, intros,
         exact (p _ _),
@@ -248,7 +241,7 @@ namespace category
     exact r,
   end
 
-  definition Precategory_eq_mk (C D : Precategory)
+  definition Precategory_eq (C D : Precategory)
     (p : carrier C = carrier D)
     (q : p ▹ (Precategory.struct C) = Precategory.struct D) : C = D :=
   begin
diff --git a/hott/algebra/category/yoneda.hlean b/hott/algebra/category/yoneda.hlean
index f25ca1692..224f8681a 100644
--- a/hott/algebra/category/yoneda.hlean
+++ b/hott/algebra/category/yoneda.hlean
@@ -68,11 +68,11 @@ namespace functor
     (Fhom F f) d = to_fun_hom F (f, id) := idp
 
   theorem functor_curry_id (c : C) : Fhom F (ID c) = nat_trans.id :=
-  nat_trans_eq_mk (λd, respect_id F _)
+  nat_trans_eq (λd, respect_id F _)
 
   theorem functor_curry_comp ⦃c c' c'' : C⦄ (f' : c' ⟶ c'') (f : c ⟶ c')
     : Fhom F (f' ∘ f) = Fhom F f' ∘n Fhom F f :=
-  nat_trans_eq_mk (λd, calc
+  nat_trans_eq (λd, calc
     natural_map (Fhom F (f' ∘ f)) d = F (f' ∘ f, id) : functor_curry_hom_def
       ... = F (f' ∘ f, id ∘ id)                      : by rewrite id_comp
       ... = F ((f',id) ∘ (f, id))                    : by esimp
@@ -158,7 +158,7 @@ namespace functor
   begin
   fapply functor_eq, exact (functor_curry_functor_uncurry_ob G),
   intros [c, c', f],
-  fapply nat_trans_eq_mk,
+  fapply nat_trans_eq,
   intro d,
   apply concat,
     {apply (ap (λx, x ∘ _)),
diff --git a/hott/init/funext.hlean b/hott/init/funext.hlean
index feeaa69e0..9ee2b4133 100644
--- a/hott/init/funext.hlean
+++ b/hott/init/funext.hlean
@@ -54,7 +54,7 @@ section
   universe variables l k
   parameters [wf : weak_funext.{l k}] {A : Type.{l}} {B : A → Type.{k}} (f : Π x, B x)
 
-  definition is_contr_sigma_homotopy [instance] : is_contr (Σ (g : Π x, B x), f ∼ g) :=
+  definition is_contr_sigma_homotopy : is_contr (Σ (g : Π x, B x), f ∼ g) :=
     is_contr.mk (sigma.mk f (homotopy.refl f))
       (λ dp, sigma.rec_on dp
         (λ (g : Π x, B x) (h : f ∼ g),
@@ -75,6 +75,7 @@ section
           endt
         )
       )
+  local attribute is_contr_sigma_homotopy [instance]
 
   parameters (Q : Π g (h : f ∼ g), Type) (d : Q f (homotopy.refl f))
 
diff --git a/hott/init/hedberg.hlean b/hott/init/hedberg.hlean
index 661a9b2dd..603f23797 100644
--- a/hott/init/hedberg.hlean
+++ b/hott/init/hedberg.hlean
@@ -44,4 +44,4 @@ section
    ... = q                      : aux)
 end
 
-attribute is_hset_of_decidable_eq [instance]
+attribute is_hset_of_decidable_eq [instance] [priority 600]
diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean
index be277d785..fbc7b59ea 100644
--- a/hott/init/trunc.hlean
+++ b/hott/init/trunc.hlean
@@ -118,7 +118,7 @@ namespace is_trunc
   /- truncation is upward close -/
 
   -- n-types are also (n+1)-types
-  definition is_trunc_succ [instance] [priority 100] (A : Type) (n : trunc_index)
+  definition is_trunc_succ [instance] [priority 900] (A : Type) (n : trunc_index)
     [H : is_trunc n A] : is_trunc (n.+1) A :=
   trunc_index.rec_on n
     (λ A (H : is_contr A), !is_trunc_succ_intro)
@@ -182,7 +182,8 @@ namespace is_trunc
 
   /- instances -/
 
-  definition is_contr_sigma_eq [instance] {A : Type} (a : A) : is_contr (Σ(x : A), a = x) :=
+  definition is_contr_sigma_eq [instance] [priority 800] {A : Type} (a : A)
+    : is_contr (Σ(x : A), a = x) :=
   is_contr.mk (sigma.mk a idp) (λp, sigma.rec_on p (λ b q, eq.rec_on q idp))
 
   definition is_contr_unit [instance] : is_contr unit :=
diff --git a/hott/types/equiv.hlean b/hott/types/equiv.hlean
index 4c09fe0bb..c324d2daa 100644
--- a/hott/types/equiv.hlean
+++ b/hott/types/equiv.hlean
@@ -48,7 +48,7 @@ namespace is_equiv
         {apply equiv.symm, apply sigma_pi_equiv_pi_sigma},
       fapply is_trunc_equiv_closed,
         {apply pi_equiv_pi_id, intro a,
-          apply (equiv_fiber_eq (fiber.mk (u.1 (f a)) (u.2 (f a))) (fiber.mk a idp))},
+          apply (fiber_eq_equiv (fiber.mk (u.1 (f a)) (u.2 (f a))) (fiber.mk a idp))},
       fapply is_trunc_pi,
       intro a, fapply @is_contr_eq,
       apply is_contr_fiber_of_is_equiv
@@ -83,16 +83,29 @@ namespace is_equiv
   theorem is_hprop_is_equiv [instance] : is_hprop (is_equiv f) :=
   is_hprop_of_imp_is_contr (λ(H : is_equiv f), is_trunc_equiv_closed -2 (equiv.symm !sigma_char'))
 
+  /- contractible fibers -/ -- TODO: uncomment this (needs to import instance is_hprop_is_trunc)
+  -- definition is_contr_fun [reducible] {A B : Type} (f : A → B) := Π(b : B), is_contr (fiber f b)
+
+  -- definition is_hprop_is_contr_fun (f : A → B) : is_hprop (is_contr_fun f) := _
+
+  -- definition is_equiv_of_is_contr_fun [instance] [H : is_contr_fun f] : is_equiv f :=
+  -- adjointify _ (λb, point (center (fiber f b)))
+  --              (λb, point_eq (center (fiber f b)))
+  --              (λa, ap point (contr (fiber.mk a idp)))
+
+  -- definition is_equiv_of_imp_is_equiv (H : B → is_equiv f) : is_equiv f :=
+  -- @is_equiv_of_is_contr_fun _ _ f (is_contr_fun.mk (λb, @is_contr_fiber_of_is_equiv _ _ _ (H b) _))
+
 end is_equiv
 
 namespace equiv
   open is_equiv
   variables {A B : Type}
 
-  protected definition eq_mk' {f f' : A → B} [H : is_equiv f] [H' : is_equiv f'] (p : f = f')
+  definition equiv_mk_eq {f f' : A → B} [H : is_equiv f] [H' : is_equiv f'] (p : f = f')
       : equiv.mk f H = equiv.mk f' H' :=
   apd011 equiv.mk p !is_hprop.elim
 
-  protected definition eq_mk {f f' : A ≃ B} (p : to_fun f = to_fun f') : f = f' :=
-  by (cases f; cases f'; apply (equiv.eq_mk' p))
+  definition equiv_eq {f f' : A ≃ B} (p : to_fun f = to_fun f') : f = f' :=
+  by (cases f; cases f'; apply (equiv_mk_eq p))
 end equiv
diff --git a/hott/types/fiber.hlean b/hott/types/fiber.hlean
index 7f3572a14..930f1f4ae 100644
--- a/hott/types/fiber.hlean
+++ b/hott/types/fiber.hlean
@@ -29,7 +29,7 @@ namespace fiber
     {intro x, cases x, apply idp},
   end
 
-  definition equiv_fiber_eq (x y : fiber f b)
+  definition fiber_eq_equiv (x y : fiber f b)
     : (x = y) ≃ (Σ(p : point x = point y), point_eq x = ap f p ⬝ point_eq y) :=
   begin
     apply equiv.trans,
@@ -46,6 +46,6 @@ namespace fiber
 
   definition fiber_eq {x y : fiber f b} (p : point x = point y)
     (q : point_eq x = ap f p ⬝ point_eq y) : x = y :=
-  to_inv !equiv_fiber_eq ⟨p, q⟩
+  to_inv !fiber_eq_equiv ⟨p, q⟩
 
 end fiber
diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean
index 39dd02fb8..793a0aab0 100644
--- a/hott/types/sigma.hlean
+++ b/hott/types/sigma.hlean
@@ -387,6 +387,6 @@ attribute sigma.is_trunc_sigma [instance] [priority 1505]
 
 open is_trunc sigma prod
 /- truncatedness -/
-definition prod.is_trunc_prod [instance] [priority 1510] (A B : Type) (n : trunc_index)
+definition prod.is_trunc_prod [instance] [priority 1490] (A B : Type) (n : trunc_index)
   [HA : is_trunc n A] [HB : is_trunc n B] : is_trunc n (A × B) :=
 is_trunc.is_trunc_equiv_closed n !equiv_prod
diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean
index 479851b0c..ebe4c3b7c 100644
--- a/hott/types/trunc.hlean
+++ b/hott/types/trunc.hlean
@@ -128,8 +128,7 @@ namespace is_trunc
     intro A, apply (trunctype.rec_on A), intros [A1, A2], apply idp,
   end
 
---  set_option pp.notation false
-  protected definition trunctype.eq (n : trunc_index) (A B : n-Type) :
+  protected definition trunctype_eq_equiv (n : trunc_index) (A B : n-Type) :
     (A = B) ≃ (carrier A = carrier B) :=
   calc
     (A = B) ≃ (trunctype.sigma_char n A = trunctype.sigma_char n B) : eq_equiv_fn_eq_of_equiv