diff --git a/library/algebra/category/constructions.lean b/library/algebra/category/constructions.lean
index 9de421d75..9d0a23a1c 100644
--- a/library/algebra/category/constructions.lean
+++ b/library/algebra/category/constructions.lean
@@ -174,9 +174,9 @@ namespace category
   variables {ob : Type} {C : category ob} {c : ob}
   protected definition slice_obs (C : category 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              := sigma.pr1 a
+  protected definition to_ob_def (a : slice_obs C c) : to_ob a = sigma.pr1 a := rfl
+  protected definition ob_hom (a : slice_obs C c) : hom (to_ob a) c := sigma.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₂
@@ -185,14 +185,14 @@ namespace category
   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)          := sigma.pr1 f
+  protected definition commute (f : slice_hom a b) : ob_hom b ∘ (hom_hom f) = ob_hom a := sigma.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
 
   definition slice_category (C : category ob) (c : ob) : category (slice_obs C c) :=
   mk (λa b, slice_hom a b)
-     (λ a b c g f, dpair (hom_hom g ∘ hom_hom f)
+     (λ a b c g f, sigma.mk (hom_hom g ∘ hom_hom f)
        (show ob_hom c ∘ (hom_hom g ∘ hom_hom f) = ob_hom a,
          proof
          calc
@@ -200,7 +200,7 @@ namespace category
              ... = ob_hom b ∘ hom_hom f : {commute g}
              ... = ob_hom a : {commute f}
          qed))
-     (λ a, dpair id !id_right)
+     (λ a, sigma.mk id !id_right)
      (λ a b c d h g f, dpair_eq    !assoc    !proof_irrel)
      (λ a b f,         sigma.equal !id_left  !proof_irrel)
      (λ a b f,         sigma.equal !id_right !proof_irrel)
@@ -235,8 +235,8 @@ namespace category
 
   definition postcomposition_functor {x y : D} (h : x ⟶ y)
       : Slice_category D x ⇒ Slice_category D y :=
-  functor.mk (λ a, dpair (to_ob a) (h ∘ ob_hom a))
-             (λ a b f, dpair (hom_hom f)
+  functor.mk (λ a, sigma.mk (to_ob a) (h ∘ ob_hom a))
+             (λ a b f, sigma.mk (hom_hom f)
        (calc
          (h ∘ ob_hom b) ∘ hom_hom f = h ∘ (ob_hom b ∘ hom_hom f) : assoc h (ob_hom b) (hom_hom f)⁻¹
            ... = h ∘ ob_hom a : congr_arg (λx, h ∘ x) (commute f)))
@@ -326,21 +326,21 @@ namespace category
   variables {ob : Type} {C : category ob}
   protected definition arrow_obs (ob : Type) (C : category ob) := Σ(a b : ob), hom a b
   variables {a b : arrow_obs ob C}
-  protected definition src    (a : arrow_obs ob C) : ob                  := dpr1 a
-  protected definition dst    (a : arrow_obs ob C) : ob                  := dpr2' a
-  protected definition to_hom (a : arrow_obs ob C) : hom (src a) (dst a) := dpr3 a
+  protected definition src    (a : arrow_obs ob C) : ob                  := sigma.pr1 a
+  protected definition dst    (a : arrow_obs ob C) : ob                  := sigma.pr2' a
+  protected definition to_hom (a : arrow_obs ob C) : hom (src a) (dst a) := sigma.pr3 a
 
   protected definition arrow_hom (a b : arrow_obs ob C) : Type :=
   Σ (g : hom (src a) (src b)) (h : hom (dst a) (dst b)), to_hom b ∘ g = h ∘ to_hom a
 
-  protected definition hom_src (m : arrow_hom a b) : hom (src a) (src b) := dpr1 m
-  protected definition hom_dst (m : arrow_hom a b) : hom (dst a) (dst b) := dpr2' m
+  protected definition hom_src (m : arrow_hom a b) : hom (src a) (src b) := sigma.pr1 m
+  protected definition hom_dst (m : arrow_hom a b) : hom (dst a) (dst b) := sigma.pr2' m
   protected definition commute (m : arrow_hom a b) : to_hom b ∘ (hom_src m) = (hom_dst m) ∘ to_hom a
-  := dpr3 m
+  := sigma.pr3 m
 
   definition arrow (ob : Type) (C : category ob) : category (arrow_obs ob C) :=
   mk (λa b, arrow_hom a b)
-     (λ a b c g f, dpair (hom_src g ∘ hom_src f) (dpair (hom_dst g ∘ hom_dst f)
+     (λ a b c g f, sigma.mk (hom_src g ∘ hom_src f) (sigma.mk (hom_dst g ∘ hom_dst f)
         (show to_hom c ∘ (hom_src g ∘ hom_src f) = (hom_dst g ∘ hom_dst f) ∘ to_hom a,
          proof
          calc
@@ -351,7 +351,7 @@ namespace category
            ... = (hom_dst g ∘ hom_dst f) ∘ to_hom a  : !assoc
          qed)
        ))
-     (λ a, dpair id (dpair id (!id_right ⬝ (symm !id_left))))
+     (λ a, sigma.mk id (sigma.mk id (!id_right ⬝ (symm !id_left))))
      (λ a b c d h g f, ndtrip_eq       !assoc    !assoc    !proof_irrel)
      (λ a b f,         ndtrip_equal !id_left  !id_left  !proof_irrel)
      (λ a b f,         ndtrip_equal !id_right !id_right !proof_irrel)
diff --git a/library/data/sigma/thms.lean b/library/data/sigma/thms.lean
index 8728c2c1e..29d84d151 100644
--- a/library/data/sigma/thms.lean
+++ b/library/data/sigma/thms.lean
@@ -13,11 +13,11 @@ namespace sigma
 
   theorem dpair_eq {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} (H₁ : a₁ = a₂) (H₂ : eq.rec_on H₁ b₁ = b₂) :
     ⟨a₁, b₁⟩ = ⟨a₂, b₂⟩ :=
-  dcongr_arg2 dpair H₁ H₂
+  dcongr_arg2 mk H₁ H₂
 
   theorem dpair_heq {a : A} {a' : A'} {b : B a} {b' : B' a'}
       (HB : B == B') (Ha : a == a') (Hb : b == b') : ⟨a, b⟩ == ⟨a', b'⟩ :=
-  hcongr_arg4 @dpair (heq.type_eq Ha) HB Ha Hb
+  hcongr_arg4 @mk (heq.type_eq Ha) HB Ha Hb
 
   protected theorem equal {p₁ p₂ : Σa : A, B a} :
     ∀(H₁ : p₁.1 = p₂.1) (H₂ : eq.rec_on H₁ p₁.2 = p₂.2), p₁ = p₂ :=
@@ -40,11 +40,11 @@ namespace sigma
   definition dtrip (a : A) (b : B a) (c : C a b) := ⟨a, b, c⟩
   definition dquad (a : A) (b : B a) (c : C a b) (d : D a b c) := ⟨a, b, c, d⟩
 
-  definition dpr1' (x : Σ a, B a) := x.1
-  definition dpr2' (x : Σ a b, C a b) := x.2.1
-  definition dpr3  (x : Σ a b, C a b) := x.2.2
-  definition dpr3' (x : Σ a b c, D a b c) := x.2.2.1
-  definition dpr4  (x : Σ a b c, D a b c) := x.2.2.2
+  definition pr1' (x : Σ a, B a) := x.1
+  definition pr2' (x : Σ a b, C a b) := x.2.1
+  definition pr3  (x : Σ a b, C a b) := x.2.2
+  definition pr3' (x : Σ a b c, D a b c) := x.2.2.1
+  definition pr4  (x : Σ a b c, D a b c) := x.2.2.2
 
   theorem dtrip_eq {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} {c₁ : C a₁ b₁} {c₂ : C a₂ b₂}
       (H₁ : a₁ = a₂) (H₂ : eq.rec_on H₁ b₁ = b₂) (H₃ : cast (dcongr_arg2 C H₁ H₂) c₁ = c₂) :
@@ -57,8 +57,8 @@ namespace sigma
   hdcongr_arg3 dtrip H₁ (heq.of_eq H₂) H₃
 
   theorem ndtrip_equal {A B : Type} {C : A → B → Type} {p₁ p₂ : Σa b, C a b} :
-      ∀(H₁ : dpr1 p₁ = dpr1 p₂) (H₂ : dpr2' p₁ = dpr2' p₂)
-      (H₃ : eq.rec_on (congr_arg2 C H₁ H₂) (dpr3 p₁) = dpr3 p₂), p₁ = p₂ :=
+      ∀(H₁ : pr1 p₁ = pr1 p₂) (H₂ : pr2' p₁ = pr2' p₂)
+      (H₃ : eq.rec_on (congr_arg2 C H₁ H₂) (pr3 p₁) = pr3 p₂), p₁ = p₂ :=
   destruct p₁ (take a₁ q₁, destruct q₁ (take b₁ c₁, destruct p₂ (take a₂ q₂, destruct q₂
     (take b₂ c₂ H₁ H₂ H₃, ndtrip_eq H₁ H₂ H₃))))
 
diff --git a/library/init/sigma.lean b/library/init/sigma.lean
index e3c9adb9d..ede5fa4c9 100644
--- a/library/init/sigma.lean
+++ b/library/init/sigma.lean
@@ -9,18 +9,18 @@ prelude
 import init.num init.wf init.logic init.tactic
 
 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 `⟨`:max t:(foldr `,` (e r, dpair e r)) `⟩`:0 := t --input ⟨ ⟩ as \< \>
+  postfix `.1`:(max+1) := pr1
+  postfix `.2`:(max+1) := pr2
   end ops
 
   open ops well_founded
diff --git a/tests/lean/run/forest_height.lean b/tests/lean/run/forest_height.lean
index 308336d8a..53b7db492 100644
--- a/tests/lean/run/forest_height.lean
+++ b/tests/lean/run/forest_height.lean
@@ -68,28 +68,28 @@ sum.cases_on tf₁
     (λ a₁ f₁ (r : Π (tf₂ : tree_forest A), tf₂ ≺ sum.inl (tree.node a₁ f₁) → map.res B tf₂),
        show map.res B (sum.inl (tree.node a₁ f₁)), from
        have rf₁ : map.res B (sum.inr f₁), from r (sum.inr f₁) (tree_forest.height_lt.node a₁ f₁),
-       have nf₁ : forest B, from sum.cases_on (dpr₁ rf₁)
+       have nf₁ : forest B, from sum.cases_on (pr₁ rf₁)
           (λf (h : kind (sum.inl f) = kind (sum.inr f₁)), absurd (eq.symm h) bool.ff_ne_tt)
           (λf h, f)
-          (dpr₂ rf₁),
-       dpair (sum.inl (tree.node (f a₁) nf₁)) rfl))
+          (pr₂ rf₁),
+       sigma.mk (sum.inl (tree.node (f a₁) nf₁)) rfl))
   (λ f : forest A, forest.cases_on f
     (λ r : Π (tf₂ : tree_forest A), tf₂ ≺ sum.inr (forest.nil A) → map.res B tf₂,
        show map.res B (sum.inr (forest.nil A)), from
-       dpair (sum.inr (forest.nil B)) rfl)
+       sigma.mk (sum.inr (forest.nil B)) rfl)
     (λ t₁ f₁ (r : Π (tf₂ : tree_forest A), tf₂ ≺ sum.inr (forest.cons t₁ f₁) → map.res B tf₂),
        show map.res B (sum.inr (forest.cons t₁ f₁)), from
        have rt₁ : map.res B (sum.inl t₁), from r (sum.inl t₁) (tree_forest.height_lt.cons₁ t₁ f₁),
        have rf₁ : map.res B (sum.inr f₁), from r (sum.inr f₁) (tree_forest.height_lt.cons₂ t₁ f₁),
-       have nt₁ : tree B, from sum.cases_on (dpr₁ rt₁)
+       have nt₁ : tree B, from sum.cases_on (pr₁ rt₁)
          (λ t h, t)
          (λ f h, absurd h bool.ff_ne_tt)
-         (dpr₂ rt₁),
-       have nf₁ : forest B, from sum.cases_on (dpr₁ rf₁)
+         (pr₂ rt₁),
+       have nf₁ : forest B, from sum.cases_on (pr₁ rf₁)
           (λf (h : kind (sum.inl f) = kind (sum.inr f₁)), absurd (eq.symm h) bool.ff_ne_tt)
           (λf h, f)
-          (dpr₂ rf₁),
-       dpair (sum.inr (forest.cons nt₁ nf₁)) rfl))
+          (pr₂ rf₁),
+       sigma.mk (sum.inr (forest.cons nt₁ nf₁)) rfl))
 
 definition map {A B : Type} (f : A → B) (tf : tree_forest A) : map.res B tf :=
 well_founded.fix (@map.F A B f) tf
diff --git a/tests/lean/run/nested_rec.lean b/tests/lean/run/nested_rec.lean
index 320ea9b64..ba3173bd7 100644
--- a/tests/lean/run/nested_rec.lean
+++ b/tests/lean/run/nested_rec.lean
@@ -5,16 +5,16 @@ open nat prod sigma
 --   g (succ x) := g (g x)
 definition g.F (x : nat) : (Π y, y < x → Σ r : nat, r ≤ y) → Σ r : nat, r ≤ x :=
 nat.cases_on x
-  (λ f, (dpair zero (le.refl zero)))
+  (λ f, ⟨zero, le.refl zero⟩)
   (λ x₁ (f : Π y, y < succ x₁ → Σ r : nat, r ≤ y),
      let p₁    := f x₁ (lt.base x₁) in
-     let gx₁   := dpr₁ p₁ in
-     let p₂    := f gx₁ (lt.of_le_of_lt (dpr₂ p₁) (lt.base x₁)) in
-     let ggx₁  := dpr₁ p₂ in
-     dpair ggx₁ (le.step (le.trans (dpr₂ p₂) (dpr₂ p₁))))
+     let gx₁   := pr₁ p₁ in
+     let p₂    := f gx₁ (lt.of_le_of_lt (pr₂ p₁) (lt.base x₁)) in
+     let ggx₁  := pr₁ p₂ in
+     ⟨ggx₁, le.step (le.trans (pr₂ p₂) (pr₂ p₁))⟩)
 
 definition g (x : nat) : nat :=
-dpr₁ (well_founded.fix g.F x)
+pr₁ (well_founded.fix g.F x)
 
 example : g 3 = 0 :=
 rfl
@@ -26,10 +26,10 @@ theorem g_zero : g 0 = 0 :=
 rfl
 
 theorem g_succ (a : nat) : g (succ a) = g (g a) :=
-have aux : well_founded.fix g.F (succ a) = dpair (g (g a)) _, from
+have aux : well_founded.fix g.F (succ a) = sigma.mk (g (g a)) _, from
   well_founded.fix_eq g.F (succ a),
-calc g (succ a) = dpr₁ (well_founded.fix g.F (succ a)) : rfl
-          ...   = dpr₁ (dpair (g (g a)) _)             : aux
+calc g (succ a) = pr₁ (well_founded.fix g.F (succ a)) : rfl
+          ...   = pr₁ (sigma.mk (g (g a)) _)          : aux
           ...   = g (g a)                              : rfl
 
 theorem g_all_zero (a : nat) : g a = zero :=
diff --git a/tests/lean/run/sigma_no_confusion.lean b/tests/lean/run/sigma_no_confusion.lean
index 0745db264..f41b5ca1d 100644
--- a/tests/lean/run/sigma_no_confusion.lean
+++ b/tests/lean/run/sigma_no_confusion.lean
@@ -17,12 +17,12 @@ namespace sigma
     eq.rec_on H₁₂ aux H₁₂
  end manual
 
- theorem sigma.mk.inj_1 {A : Type} {B : A → Type} {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} (Heq : dpair a₁ b₁ = dpair a₂ b₂) : a₁ = a₂ :=
+ theorem sigma.mk.inj_1 {A : Type} {B : A → Type} {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} (Heq : mk a₁ b₁ = mk a₂ b₂) : a₁ = a₂ :=
  begin
    apply (no_confusion Heq), intros, assumption
  end
 
- theorem sigma.mk.inj_2 {A : Type} {B : A → Type} (a₁ a₂ : A) (b₁ : B a₁) (b₂ : B a₂) (Heq : dpair a₁ b₁ = dpair a₂ b₂) : b₁ == b₂ :=
+ theorem sigma.mk.inj_2 {A : Type} {B : A → Type} (a₁ a₂ : A) (b₁ : B a₁) (b₂ : B a₂) (Heq : mk a₁ b₁ = mk a₂ b₂) : b₁ == b₂ :=
  begin
    apply (no_confusion Heq), intros, eassumption
  end
diff --git a/tests/lean/run/structure_test.lean b/tests/lean/run/structure_test.lean
index 767f78b39..684b6c34d 100644
--- a/tests/lean/run/structure_test.lean
+++ b/tests/lean/run/structure_test.lean
@@ -18,7 +18,7 @@ section
   include E
    -- include Ha
 
-  structure point3d_color (B C : Type) (D : B → Type) extends point (foo A) B, sigma D renaming dpr1→y dpr2→w :=
+  structure point3d_color (B C : Type) (D : B → Type) extends point (foo A) B, sigma D renaming pr1→y pr2→w :=
   mk :: (c : color) (H : x == y)
 
   check point3d_color.c
diff --git a/tests/lean/run/vector_subterm_pred.lean b/tests/lean/run/vector_subterm_pred.lean
index 0d75d09e9..1cca841ac 100644
--- a/tests/lean/run/vector_subterm_pred.lean
+++ b/tests/lean/run/vector_subterm_pred.lean
@@ -9,7 +9,7 @@ namespace vector
 
 definition vec (A : Type) : Type := Σ n : nat, vector A n
 
-definition to_vec {A : Type} {n : nat} (v : vector A n) : vec A := dpair n v
+definition to_vec {A : Type} {n : nat} (v : vector A n) : vec A := ⟨n, v⟩
 
 inductive direct_subterm (A : Type) : vec A → vec A → Prop :=
 cons : Π (n : nat) (a : A) (v : vector A n), direct_subterm A (to_vec v) (to_vec (cons a v))