diff --git a/hott/algebra/precategory/constructions.hlean b/hott/algebra/precategory/constructions.hlean
index ec2e4eece..30671e9fc 100644
--- a/hott/algebra/precategory/constructions.hlean
+++ b/hott/algebra/precategory/constructions.hlean
@@ -168,9 +168,9 @@ namespace precategory
   variables {ob : Type} {C : precategory ob} {c : ob}
   protected definition slice_obs (C : precategory ob) (c : ob) := Σ(b : ob), hom b c
   variables {a b : slice_obs C c}
-  protected definition to_ob  (a : slice_obs C c) : ob              := dpr1 a
-  protected definition to_ob_def (a : slice_obs C c) : to_ob a = dpr1 a := rfl
-  protected definition ob_hom (a : slice_obs C c) : hom (to_ob a) c := dpr2 a
+  protected definition to_ob  (a : slice_obs C c) : ob              := pr1 a
+  protected definition to_ob_def (a : slice_obs C c) : to_ob a = pr1 a := rfl
+  protected definition ob_hom (a : slice_obs C c) : hom (to_ob a) c := pr2 a
   -- protected theorem slice_obs_equal (H₁ : to_ob a = to_ob b)
   --     (H₂ : eq.drec_on H₁ (ob_hom a) = ob_hom b) : a = b :=
   -- sigma.equal H₁ H₂
@@ -179,8 +179,8 @@ namespace precategory
   protected definition slice_hom (a b : slice_obs C c) : Type :=
   Σ(g : hom (to_ob a) (to_ob b)), ob_hom b ∘ g = ob_hom a
 
-  protected definition hom_hom  (f : slice_hom a b) : hom (to_ob a) (to_ob b)          := dpr1 f
-  protected definition commute (f : slice_hom a b) : ob_hom b ∘ (hom_hom f) = ob_hom a := dpr2 f
+  protected definition hom_hom  (f : slice_hom a b) : hom (to_ob a) (to_ob b)          := pr1 f
+  protected definition commute (f : slice_hom a b) : ob_hom b ∘ (hom_hom f) = ob_hom a := pr2 f
   -- protected theorem slice_hom_equal (f g : slice_hom a b) (H : hom_hom f = hom_hom g) : f = g :=
   -- sigma.equal H !proof_irrel
 
diff --git a/hott/algebra/precategory/iso.hlean b/hott/algebra/precategory/iso.hlean
index 8ed2205ea..d9ad03a84 100644
--- a/hott/algebra/precategory/iso.hlean
+++ b/hott/algebra/precategory/iso.hlean
@@ -21,7 +21,7 @@ namespace morphism
         exact (pr₂ S.2),
     fapply adjointify,
         intro H, apply (is_iso.rec_on H), intros (g, η, ε),
-        exact (dpair g (pair η ε)),
+        exact (sigma.mk g (pair η ε)),
       intro H, apply (is_iso.rec_on H), intros (g, η, ε), apply idp,
     intro S, apply (sigma.rec_on S), intros (g, ηε),
     apply (prod.rec_on ηε), intros (η, ε), apply idp,
@@ -35,7 +35,7 @@ namespace morphism
       intro S, apply isomorphic.mk, apply (S.2),
       fapply adjointify,
         intro p, apply (isomorphic.rec_on p), intros (f, H),
-        exact (dpair f H),
+        exact (sigma.mk f H),
       intro p, apply (isomorphic.rec_on p), intros (f, H), apply idp,
     intro S, apply (sigma.rec_on S), intros (f, H), apply idp,
   end
diff --git a/hott/init/axioms/funext_from_ua.hlean b/hott/init/axioms/funext_from_ua.hlean
index 89a9fddac..b48c2ae15 100644
--- a/hott/init/axioms/funext_from_ua.hlean
+++ b/hott/init/axioms/funext_from_ua.hlean
@@ -59,10 +59,10 @@ context
   protected definition isequiv_src_compose {A B : Type}
       : @is_equiv (A → diagonal B)
                  (A → B)
-                 (compose (pr₁ ∘ dpr1)) :=
-    @ua_isequiv_postcompose _ _ _ (pr₁ ∘ dpr1)
-        (is_equiv.adjointify (pr₁ ∘ dpr1)
-          (λ x, dpair (x , x) idp) (λx, idp)
+                 (compose (pr₁ ∘ pr1)) :=
+    @ua_isequiv_postcompose _ _ _ (pr₁ ∘ pr1)
+        (is_equiv.adjointify (pr₁ ∘ pr1)
+          (λ x, sigma.mk (x , x) idp) (λx, idp)
           (λ x, sigma.rec_on x
             (λ xy, prod.rec_on xy
               (λ b c p, eq.rec_on p idp))))
@@ -70,10 +70,10 @@ context
   protected definition isequiv_tgt_compose {A B : Type}
       : @is_equiv (A → diagonal B)
                  (A → B)
-                 (compose (pr₂ ∘ dpr1)) :=
-    @ua_isequiv_postcompose _ _ _ (pr2 ∘ dpr1)
-        (is_equiv.adjointify (pr2 ∘ dpr1)
-          (λ x, dpair (x , x) idp) (λx, idp)
+                 (compose (pr₂ ∘ pr1)) :=
+    @ua_isequiv_postcompose _ _ _ (pr2 ∘ pr1)
+        (is_equiv.adjointify (pr2 ∘ pr1)
+          (λ x, sigma.mk (x , x) idp) (λx, idp)
           (λ x, sigma.rec_on x
             (λ xy, prod.rec_on xy
               (λ b c p, eq.rec_on p idp))))
@@ -81,21 +81,21 @@ context
   theorem nondep_funext_from_ua {A : Type} {B : Type.{l+1}}
       : Π {f g : A → B}, f ∼ g → f = g :=
     (λ (f g : A → B) (p : f ∼ g),
-        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
+        let d := λ (x : A), sigma.mk (f x , f x) idp in
+        let e := λ (x : A), sigma.mk (f x , g x) (p x) in
+        let precomp1 :=  compose (pr₁ ∘ pr1) in
         have equiv1 [visible] : is_equiv precomp1,
           from @isequiv_src_compose A B,
         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,
+            pr₁ ∘ pr1 ∘ x = pr₁ ∘ pr1 ∘ y → x = y,
           from (λ x y, is_equiv.inv (ap precomp1)),
-        have eq2 : pr₁ ∘ dpr1 ∘ d = pr₁ ∘ dpr1 ∘ e,
+        have eq2 : pr₁ ∘ pr1 ∘ d = pr₁ ∘ pr1 ∘ e,
           from idp,
         have eq0 : d = e,
           from H' d e eq2,
-        have eq1 : (pr₂ ∘ dpr1) ∘ d = (pr₂ ∘ dpr1) ∘ e,
+        have eq1 : (pr₂ ∘ pr1) ∘ d = (pr₂ ∘ pr1) ∘ e,
           from ap _ eq0,
         eq1
     )
diff --git a/hott/init/axioms/funext_varieties.hlean b/hott/init/axioms/funext_varieties.hlean
index 227d9cfb6..4523003ca 100644
--- a/hott/init/axioms/funext_varieties.hlean
+++ b/hott/init/axioms/funext_varieties.hlean
@@ -58,22 +58,22 @@ context
   protected definition idhtpy : f ∼ f := (λ x, idp)
 
   definition contr_basedhtpy [instance] : is_contr (Σ (g : Π x, B x), f ∼ g) :=
-    is_contr.mk (dpair f idhtpy)
+    is_contr.mk (sigma.mk f idhtpy)
       (λ dp, sigma.rec_on dp
         (λ (g : Π x, B x) (h : f ∼ g),
           let r := λ (k : Π x, Σ y, f x = y),
-            @dpair _ (λg, f ∼ g)
-              (λx, dpr1 (k x)) (λx, dpr2 (k x)) in
-          let s := λ g h x, @dpair _ (λy, f x = y) (g x) (h x) in
+            @sigma.mk _ (λg, f ∼ g)
+              (λx, pr1 (k x)) (λx, pr2 (k x)) in
+          let s := λ g h x, @sigma.mk _ (λy, f x = y) (g x) (h x) in
           have t1 : Πx, is_contr (Σ y, f x = y),
             from (λx, !contr_basedpaths),
           have t2 : is_contr (Πx, Σ y, f x = y),
             from !wf,
-          have t3 : (λ x, @dpair _ (λ y, f x = y) (f x) idp) = s g h,
+          have t3 : (λ x, @sigma.mk _ (λ y, f x = y) (f x) idp) = s g h,
             from @path_contr (Π x, Σ y, f x = y) t2 _ _,
-          have t4 : r (λ x, dpair (f x) idp) = r (s g h),
+          have t4 : r (λ x, sigma.mk (f x) idp) = r (s g h),
             from ap r t3,
-          have endt : dpair f idhtpy = dpair g h,
+          have endt : sigma.mk f idhtpy = sigma.mk g h,
             from t4,
           endt
         )
@@ -82,7 +82,7 @@ context
   parameters (Q : Π g (h : f ∼ g), Type) (d : Q f idhtpy)
 
   definition htpy_ind (g : Πx, B x) (h : f ∼ g) : Q g h :=
-    @transport _ (λ gh, Q (dpr1 gh) (dpr2 gh)) (dpair f idhtpy) (dpair g h)
+    @transport _ (λ gh, Q (pr1 gh) (pr2 gh)) (sigma.mk f idhtpy) (sigma.mk g h)
       (@path_contr _ contr_basedhtpy _ _) d
 
   definition htpy_ind_beta : htpy_ind f idhtpy = d :=
diff --git a/hott/init/hedberg.hlean b/hott/init/hedberg.hlean
index f6832e8f5..bd2dab47b 100644
--- a/hott/init/hedberg.hlean
+++ b/hott/init/hedberg.hlean
@@ -8,7 +8,7 @@ Hedberg's Theorem: every type with decidable equality is a hset
 -/
 prelude
 import init.nat init.trunc
-open eq eq.ops nat truncation sigma.ops
+open eq eq.ops nat truncation sigma
 
 -- TODO(Leo): move const coll and path_coll to a different file?
 private definition const {A B : Type} (f : A → B) := ∀ x y, f x = f y
diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean
index c4093033d..22e6c6261 100644
--- a/hott/init/trunc.hlean
+++ b/hott/init/trunc.hlean
@@ -176,7 +176,7 @@ namespace truncation
   /- instances -/
 
   definition contr_basedpaths [instance] {A : Type} (a : A) : is_contr (Σ(x : A), a = x) :=
-  is_contr.mk (dpair a idp) (λp, sigma.rec_on p (λ b q, eq.rec_on q idp))
+  is_contr.mk (sigma.mk a idp) (λp, sigma.rec_on p (λ b q, eq.rec_on q idp))
 
   -- definition is_trunc_is_hprop [instance] {n : trunc_index} : is_hprop (is_trunc n A) := sorry
 
diff --git a/hott/init/types/sigma.hlean b/hott/init/types/sigma.hlean
index ce2324acd..316bb4d5e 100644
--- a/hott/init/types/sigma.hlean
+++ b/hott/init/types/sigma.hlean
@@ -4,22 +4,20 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
 -/
 prelude
-import ..num ..wf ..logic ..tactic
+import init.num
 
 structure sigma {A : Type} (B : A → Type) :=
-dpair :: (dpr1 : A) (dpr2 : B dpr1)
+mk :: (pr1 : A) (pr2 : B pr1)
 
 notation `Σ` binders `,` r:(scoped P, sigma P) := r
 
 namespace sigma
-
-  notation `dpr₁` := dpr1
-  notation `dpr₂` := dpr2
+  notation `pr₁` := pr1
+  notation `pr₂` := pr2
+  notation `⟨`:max t:(foldr `,` (e r, mk e r)) `⟩`:0 := t --input ⟨ ⟩ as \< \>
 
   namespace ops
-  postfix `.1`:(max+1) := dpr1
-  postfix `.2`:(max+1) := dpr2
-  notation `⟨` t:(foldr `,` (e r, sigma.dpair e r)) `⟩`:0 := t --input ⟨ ⟩ as \< \>
+  postfix `.1`:(max+1) := pr1
+  postfix `.2`:(max+1) := pr2
   end ops
-
 end sigma
diff --git a/hott/pointed.hlean b/hott/pointed.hlean
index 7682c1833..8c0c0818d 100644
--- a/hott/pointed.hlean
+++ b/hott/pointed.hlean
@@ -23,7 +23,7 @@ namespace is_pointed
   -- A sigma type of pointed components is pointed
   protected definition sigma [instance] {P : A → Type} [G : is_pointed A]
       [H : is_pointed (P (point A))] : is_pointed (Σx, P x) :=
-    is_pointed.mk (sigma.dpair (point A) (point (P (point A))))
+    is_pointed.mk (sigma.mk (point A) (point (P (point A))))
 
   protected definition prod [H1 : is_pointed A] [H2 : is_pointed B]
       : is_pointed (A × B) :=
diff --git a/hott/types/pi.hlean b/hott/types/pi.hlean
index 6f620ade1..67a8840da 100644
--- a/hott/types/pi.hlean
+++ b/hott/types/pi.hlean
@@ -79,7 +79,7 @@ namespace pi
     : (Π(b : B a), p ▹D (f b) = g (p ▹ b)) ≃ (p ▹ f = g) :=
   eq.rec_on p (λg, !homotopy_equiv_path) g
 
-  section open sigma.ops
+  section open sigma sigma.ops
   /- more implicit arguments:
   (Π(b : B a), eq.transport C (sigma.path p idp) (f b) = g (p ▹ b)) ≃
   (Π(b : B a), transportD B (λ(a : A) (b : B a), C ⟨a, b⟩) p b (f b) = g (eq.transport B p b)) -/
diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean
index 97ac35323..ef55e1da6 100644
--- a/hott/types/sigma.hlean
+++ b/hott/types/sigma.hlean
@@ -26,7 +26,7 @@ namespace sigma
   definition eta3 (u : Σa b c, D a b c) : ⟨u.1, u.2.1, u.2.2.1, u.2.2.2⟩ = u :=
   destruct u (λu1 u2, destruct u2 (λu21 u22, destruct u22 (λu221 u222, idp)))
 
-  definition dpair_eq_dpair (p : a = a') (q : p ▹ b = b') : dpair a b = dpair a' b' :=
+  definition dpair_eq_dpair (p : a = a') (q : p ▹ b = b') : sigma.mk a b = sigma.mk a' b' :=
   eq.rec_on p (λb b' q, eq.rec_on q idp) b b' q
 
   /- In Coq they often have to give u and v explicitly -/
@@ -38,7 +38,7 @@ namespace sigma
   /- Projections of paths from a total space -/
 
   definition path_pr1 (p : u = v) : u.1 = v.1 :=
-  ap dpr1 p
+  ap pr1 p
 
   postfix `..1`:(max+1) := path_pr1
 
@@ -50,7 +50,7 @@ namespace sigma
   postfix `..2`:(max+1) := path_pr2
 
   definition dpair_sigma_path (p : u.1 = v.1) (q : p ▹ u.2 = v.2)
-      :  dpair (sigma.path p q)..1 (sigma.path p q)..2 = ⟨p, q⟩ :=
+      :  sigma.mk (sigma.path p q)..1 (sigma.path p q)..2 = ⟨p, q⟩ :=
   begin
     reverts (p, q),
     apply (destruct u), intros (u1, u2),
@@ -85,11 +85,11 @@ namespace sigma
 
   /- the uncurried version of sigma_eq. We will prove that this is an equivalence -/
 
-  definition sigma_path_uncurried (pq : Σ(p : dpr1 u = dpr1 v), p ▹ (dpr2 u) = dpr2 v) : u = v :=
+  definition sigma_path_uncurried (pq : Σ(p : pr1 u = pr1 v), p ▹ (pr2 u) = pr2 v) : u = v :=
   destruct pq sigma.path
 
   definition dpair_sigma_path_uncurried (pq : Σ(p : u.1 = v.1), p ▹ u.2 = v.2)
-      :  dpair (sigma_path_uncurried pq)..1 (sigma_path_uncurried pq)..2 = pq :=
+      :  sigma.mk (sigma_path_uncurried pq)..1 (sigma_path_uncurried pq)..2 = pq :=
   destruct pq dpair_sigma_path
 
   definition sigma_path_pr1_uncurried (pq : Σ(p : u.1 = v.1), p ▹ u.2 = v.2)
@@ -100,7 +100,7 @@ namespace sigma
       : (sigma_path_pr1_uncurried pq) ▹ (sigma_path_uncurried pq)..2 = pq.2 :=
   (!dpair_sigma_path_uncurried)..2
 
-  definition sigma_path_eta_uncurried (p : u = v) : sigma_path_uncurried (dpair p..1 p..2) = p :=
+  definition sigma_path_eta_uncurried (p : u = v) : sigma_path_uncurried (sigma.mk p..1 p..2) = p :=
   !sigma_path_eta
 
   definition transport_sigma_path_dpr1_uncurried {B' : A → Type}
@@ -158,7 +158,7 @@ namespace sigma
 
   /- Applying dpair to one argument is the same as dpair_eq_dpair with reflexivity in the first place. -/
 
-  definition ap_dpair (q : b₁ = b₂) : ap (dpair a) q = dpair_eq_dpair idp q :=
+  definition ap_dpair (q : b₁ = b₂) : ap (sigma.mk a) q = dpair_eq_dpair idp q :=
   eq.rec_on q idp
 
   /- Dependent transport is the same as transport along a sigma_eq. -/
@@ -318,14 +318,14 @@ namespace sigma
   /- definition 3.11.9(i): Summing up a contractible family of types does nothing. -/
   open truncation
   definition is_equiv_dpr1 [instance] (B : A → Type) [H : Π a, is_contr (B a)]
-      : is_equiv (@dpr1 A B) :=
-  adjointify dpr1
+      : is_equiv (@pr1 A B) :=
+  adjointify pr1
              (λa, ⟨a, !center⟩)
              (λa, idp)
              (λu, sigma.path idp !contr)
 
   definition equiv_of_all_contr [H : Π a, is_contr (B a)] : (Σa, B a) ≃ A :=
-  equiv.mk dpr1 _
+  equiv.mk pr1 _
 
   /- definition 3.11.9(ii): Dually, summing up over a contractible type does nothing. -/
 
@@ -375,7 +375,7 @@ namespace sigma
                  ... ≃ (Σa' a, C (a, a')) : assoc_equiv_prod
 
   definition symm_equiv (C : A → A' → Type) : (Σa a', C a a') ≃ (Σa' a, C a a') :=
-  symm_equiv_uncurried (λu, C (pr1 u) (pr2 u))
+  symm_equiv_uncurried (λu, C (prod.pr1 u) (prod.pr2 u))
 
   definition equiv_prod (A B : Type) : (Σ(a : A), B) ≃ A × B :=
   equiv.mk _ (adjointify
@@ -430,7 +430,7 @@ namespace sigma
 
   /- To prove equality in a subtype, we only need equality of the first component. -/
   definition path_hprop [H : Πa, is_hprop (B a)] (u v : Σa, B a) : u.1 = v.1 → u = v :=
-  (sigma_path_uncurried ∘ (@inv _ _ dpr1 (@is_equiv_dpr1 _ _ (λp, !succ_is_trunc))))
+  (sigma_path_uncurried ∘ (@inv _ _ pr1 (@is_equiv_dpr1 _ _ (λp, !succ_is_trunc))))
 
   definition is_equiv_path_hprop [instance] [H : Πa, is_hprop (B a)] (u v : Σa, B a)
       : is_equiv (path_hprop u v) :=
diff --git a/tests/lean/hott/329.hlean b/tests/lean/hott/329.hlean
index e50722551..f338639f1 100644
--- a/tests/lean/hott/329.hlean
+++ b/tests/lean/hott/329.hlean
@@ -3,10 +3,10 @@ open eq sigma
 variables {A : Type} {B : A → Type} {C : Πa, B a → Type} {D : Πa b, C a b → Type}
           {a a' a'' : A} {b b₁ b₂ : B a} {b' : B a'} {b'' : B a''} {u v w : Σa, B a}
 
-definition path_sigma_dpair (p : a = a') (q : p ▹ b = b') : dpair a b = dpair a' b' :=
+definition path_sigma_dpair (p : a = a') (q : p ▹ b = b') : sigma.mk a b = sigma.mk a' b' :=
 eq.rec_on p (λb b' q, eq.rec_on q idp) b b' q
 
-definition path_sigma (p :  dpr1 u = dpr1 v) (q : p ▹ dpr2 u = dpr2 v) : u = v :=
+definition path_sigma (p :  pr1 u = pr1 v) (q : p ▹ pr2 u = pr2 v) : u = v :=
 destruct u
          (λu1 u2, destruct v (λ v1 v2, path_sigma_dpair))
          p q
diff --git a/tests/lean/hott/sig_noc.hlean b/tests/lean/hott/sig_noc.hlean
index f60cf7b31..e30ff7baa 100644
--- a/tests/lean/hott/sig_noc.hlean
+++ b/tests/lean/hott/sig_noc.hlean
@@ -1,6 +1,6 @@
 namespace sigma
   open lift
-  open sigma.ops
+  open sigma.ops sigma
   variables {A : Type} {B : A → Type}
 
   variables {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂}
@@ -22,7 +22,7 @@ mk :: (A : Type) (B : A → Type) (a : A) (b : B a)
 set_option pp.implicit true
 
 namespace foo
-  open lift sigma.ops
+  open lift sigma sigma.ops
   universe variables l₁ l₂
   variables {A₁ : Type.{l₁}} {B₁ : A₁ → Type.{l₂}} {a₁ : A₁} {b₁ : B₁ a₁}
   variables {A₂ : Type.{l₁}} {B₂ : A₂ → Type.{l₂}} {a₂ : A₂} {b₂ : B₂ a₂}