chore(library/init): adjust Sort vs Type in definitions

library/init/core.lean

@@ -146,7 +146,7 @@ or.inl ha
 def or.intro_right (a : Prop) {b : Prop} (hb : b) : or a b :=
 or.inr hb
 
-structure sigma {α : Type u} (β : α → Sort v) :=
+structure sigma {α : Type u} (β : α → Type v) :=
 mk :: (fst : α) (snd : β fst)
 
 structure psigma {α : Sort u} (β : α → Sort v) :=

library/init/data/sigma/basic.lean

@@ -7,10 +7,11 @@ prelude
 import init.logic init.wf
 
 notation `Σ` binders `, ` r:(scoped p, sigma p) := r
+notation `Σ'` binders `, ` r:(scoped p, psigma p) := r
 
 universe variables u v
 
-lemma ex_of_sig {α : Type u} {p : α → Prop} : (Σ x, p x) → ∃ x, p x
+lemma ex_of_psig {α : Type u} {p : α → Prop} : (Σ' x, p x) → ∃ x, p x
 | ⟨x, hx⟩ := ⟨x, hx⟩
 
 namespace sigma

library/init/function.lean

@@ -7,22 +7,23 @@ General operations on functions.
 -/
 prelude
 import init.data.prod init.funext init.logic
-notation f ` $ `:1 a:0 := f a
 universe variables u₁ u₂ u₃ u₄
-variables {α : Type u₁} {β : Type u₂} {φ : Type u₃} {δ : Type u₄} {ζ : Type u₁}
 
-@[inline, reducible] def function.comp (f : β → φ) (g : α → β) : α → φ :=
+namespace function
+notation f ` $ `:1 a:0 := f a
+
+variables {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {δ : Sort u₄} {ζ : Sort u₁}
+
+@[inline, reducible] def comp (f : β → φ) (g : α → β) : α → φ :=
 λ x, f (g x)
 
-@[inline, reducible] def function.dcomp {β : α → Type u₂} {φ : Π {x : α}, β x → Type u₃}
+@[inline, reducible] def dcomp {β : α → Sort u₂} {φ : Π {x : α}, β x → Sort u₃}
   (f : Π {x : α} (y : β x), φ y) (g : Π x, β x) : Π x, φ (g x) :=
 λ x, f (g x)
 
 infixr  ` ∘ `      := function.comp
 infixr  ` ∘' `:80  := function.dcomp
 
-namespace function
-
 @[reducible] def comp_right (f : β → β → β) (g : α → β) : β → α → β :=
 λ b a, f b (g a)
 
@@ -36,27 +37,15 @@ namespace function
   : α → β → ζ :=
 λ x y, op (f x y) (g x y)
 
-@[reducible] def const (β : Type u₂) (a : α) : β → α :=
+@[reducible] def const (β : Sort u₂) (a : α) : β → α :=
 λ x, a
 
-@[reducible] def swap {φ : α → β → Type u₃} (f : Π x y, φ x y) : Π y x, φ x y :=
+@[reducible] def swap {φ : α → β → Sort u₃} (f : Π x y, φ x y) : Π y x, φ x y :=
 λ y x, f x y
 
-@[reducible] def app {β : α → Type u₂} (f : Π x, β x) (x : α) : β x :=
+@[reducible] def app {β : α → Sort u₂} (f : Π x, β x) (x : α) : β x :=
 f x
 
-@[reducible] def curry : (α × β → φ) → α → β → φ :=
-λ f a b, f (a, b)
-
-@[reducible] def uncurry : (α → β → φ) → α × β → φ :=
-λ f ⟨a, b⟩, f a b
-
-lemma curry_uncurry (f : α → β → φ) : curry (uncurry f) = f :=
-rfl
-
-lemma uncurry_curry (f : α × β → φ) : uncurry (curry f) = f :=
-funext (λ ⟨a, b⟩, rfl)
-
 infixl  ` on `:1         := on_fun
 notation f ` -[` op `]- ` g  := combine f op g
 
@@ -91,17 +80,11 @@ lemma bijective_comp {g : β → φ} {f : α → β} : bijective g → bijective
 -- g is a left inverse to f
 def left_inverse (g : β → α) (f : α → β) : Prop := ∀ x, g (f x) = x
 
-def id_of_left_inverse {g : β → α} {f : α → β} : left_inverse g f → g ∘ f = id :=
-assume h, funext h
-
 def has_left_inverse (f : α → β) : Prop := ∃ finv : β → α, left_inverse finv f
 
 -- g is a right inverse to f
 def right_inverse (g : β → α) (f : α → β) : Prop := left_inverse f g
 
-def id_of_right_inverse {g : β → α} {f : α → β} : right_inverse g f → f ∘ g = id :=
-assume h, funext h
-
 def has_right_inverse (f : α → β) : Prop := ∃ finv : β → α, right_inverse finv f
 
 lemma injective_of_left_inverse {g : β → α} {f : α → β} : left_inverse g f → injective f :=
@@ -139,3 +122,26 @@ lemma surjective_id : surjective (@id α) := take a, ⟨a, rfl⟩
 lemma bijective_id : bijective (@id α) := ⟨injective_id, surjective_id⟩
 
 end function
+
+namespace function
+variables {α : Type u₁} {β : Type u₂} {φ : Type u₃}
+
+@[reducible] def curry : (α × β → φ) → α → β → φ :=
+λ f a b, f (a, b)
+
+@[reducible] def uncurry : (α → β → φ) → α × β → φ :=
+λ f ⟨a, b⟩, f a b
+
+lemma curry_uncurry (f : α → β → φ) : curry (uncurry f) = f :=
+rfl
+
+lemma uncurry_curry (f : α × β → φ) : uncurry (curry f) = f :=
+funext (λ ⟨a, b⟩, rfl)
+
+def id_of_left_inverse {g : β → α} {f : α → β} : left_inverse g f → g ∘ f = id :=
+assume h, funext h
+
+def id_of_right_inverse {g : β → α} {f : α → β} : right_inverse g f → f ∘ g = id :=
+assume h, funext h
+
+end function

library/init/logic.lean

@@ -982,7 +982,7 @@ lemma let_eq {α : Sort v} {β : Sort u} {a₁ a₂ : α} {b₁ b₂ : α → β
 λ h₁ h₂, eq.rec_on h₁ (h₂ a₁)
 
 section relation
-variables {α : Type u} {β : Type v} (r : β → β → Prop)
+variables {α : Sort u} {β : Sort v} (r : β → β → Prop)
 local infix `≺`:50 := r
 
 def reflexive := ∀ x, x ≺ x

tests/lean/anc1.lean

@@ -4,7 +4,7 @@ check (⟨trivial, trivial⟩ : true ∧ true)
 
 example : true := sorry
 
-check (⟨1, sorry⟩ : Σ x : nat, x > 0)
+check (⟨1, sorry⟩ : Σ' x : nat, x > 0)
 
 open tactic
 

tests/lean/anc1.lean.expected.out

@@ -1,6 +1,6 @@
 (1, 2) : ℕ × ℕ
 and.intro trivial trivial : true ∧ true
-sigma.mk 1 sorry : Σ (x : ℕ), x > 0
+psigma.mk 1 sorry : Σ' (x : ℕ), x > 0
 show true, from true.intro : true
 Exists.intro 1 (id_locked (1 ≠ 0) (λ (a : 1 = 0), nat.no_confusion a)) : ∃ (x : ℕ), 1 ≠ 0
 λ (A B C : Prop) (Ha : A) (Hb : B) (Hc : C), show B ∧ A, from and.intro Hb Ha :

tests/lean/elab6.lean.expected.out

@@ -1,9 +1,9 @@
-H : @transitive.{0} nat R
+H : @transitive.{1} nat R
 @F.{u_1} ?M_1 : Π ⦃a : ?M_1⦄ {b : ?M_1}, ?M_1 → Π ⦃e : ?M_1⦄, ?M_1 → ?M_1 → ?M_1
 @F.{0} bool ?M_1 ?M_2 bool.tt : Π ⦃e : bool⦄, bool → bool → bool
 @F.{0} bool ?M_1 ?M_2 bool.tt ?M_3 bool.tt : bool → bool
 @F.{0} bool ?M_1 ?M_2 bool.tt ?M_3 bool.tt bool.tt : bool
-H : @transitive.{0} nat R
+H : @transitive.{1} nat R
 @F.{u_1} ?M_1 : Π ⦃a : ?M_1⦄ {b : ?M_1}, ?M_1 → Π ⦃e : ?M_1⦄, ?M_1 → ?M_1 → ?M_1
 @F.{0} bool ?M_1 ?M_2 bool.tt : Π ⦃e : bool⦄, bool → bool → bool
 @F.{0} bool ?M_1 ?M_2 bool.tt ?M_3 bool.tt : bool → bool

tests/lean/notation4.lean

@@ -3,5 +3,5 @@ open sigma
 inductive List (T : Type) : Type | nil {} : List | cons   : T → List → List open List notation h :: t  := cons h t notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l
 check ∃ (A : Type) (x y : A), x = y
 check ∃ (x : num), x = 0
-check Σ (x : num), x = 10
+check Σ' (x : num), x = 10
 check Σ (A : Type), List A

tests/lean/notation4.lean.expected.out

@@ -1,4 +1,4 @@
 ∃ (A : Type) (x y : A), x = y : Prop
 ∃ (x : num), x = 0 : Prop
-Σ (x : num), x = 10 : Type
+Σ' (x : num), x = 10 : Type
 Σ (A : Type), List A : Type 1

tests/lean/run/match_convoy.lean

@@ -53,19 +53,19 @@ quotient.rec_on_subsingleton₂ b₁ b₂ (λ l₁ l₂,
 attribute [instance]
 noncomputable definition decidable_subbag2 {A} (b₁ b₂ : bag A) : decidable (b₁ ⊆ b₂) :=
 quotient.rec_on_subsingleton₂ b₁ b₂ (λ l₁ l₂,
-  match sigma.mk (subcount l₁ l₂) rfl : (Σ (b : _), subcount l₁ l₂ = b) → _ with
-  | sigma.mk tt H := is_true (all_of_subcount_eq_tt H)
-  | sigma.mk ff H := is_false (λ h,
+  match psigma.mk (subcount l₁ l₂) rfl : (Σ' (b : _), subcount l₁ l₂ = b) → _ with
+  | psigma.mk tt H := is_true (all_of_subcount_eq_tt H)
+  | psigma.mk ff H := is_false (λ h,
             exists.elim (ex_of_subcount_eq_ff H)
             (λ w hw, absurd (h w) hw))
   end)
 
-local notation ⟦ a , b ⟧ := sigma.mk a b
+local notation ⟦ a , b ⟧ := psigma.mk a b
 
 attribute [instance]
 noncomputable definition decidable_subbag3 {A} (b₁ b₂ : bag A) : decidable (b₁ ⊆ b₂) :=
 quotient.rec_on_subsingleton₂ b₁ b₂ (λ l₁ l₂,
-  match ⟦subcount l₁ l₂, rfl⟧ : (Σ (b : _), subcount l₁ l₂ = b) → _ with
+  match ⟦subcount l₁ l₂, rfl⟧ : (Σ' (b : _), subcount l₁ l₂ = b) → _ with
   | ⟦tt, H⟧ := is_true (all_of_subcount_eq_tt H)
   | ⟦ff, H⟧ := is_false (λ h,
             exists.elim (ex_of_subcount_eq_ff H)

tests/lean/run/struct_value.lean

@@ -31,13 +31,13 @@ print p3
 
 check { point3d . x := 1, y := 2, z := 3 }
 
-check (⟨10, rfl⟩ : Σ x : nat, x = x)
+check (⟨10, rfl⟩ : Σ' x : nat, x = x)
 
-check ((| 10, rfl |) : Σ x : nat, x = x)
+check ((| 10, rfl |) : Σ' x : nat, x = x)
 
-check ({ fst := 10, snd := rfl } : Σ x : nat, x = x)
+check ({ fst := 10, snd := rfl } : Σ' x : nat, x = x)
 
-definition f (a : nat) : Σ x : nat, x = x :=
+definition f (a : nat) : Σ' x : nat, x = x :=
 { fst := a, snd := rfl }
 
 print f