set on Sort

Stream: general

[Kyle Miller]

set and subtype are very old parts of Lean (old enough that subtype dates to the time before universe variables, eight years ago). When set was introduced, the definitions for the two were

structure subtype {A : Type u} (P : A → Prop) :=
tag :: (elt_of : A) (has_property : P elt_of)

and

definition set (A : Type u) := A → Prop

At some point, subtype was changed to use Sort (which I believe didn't even exist yet), but set has had essentially the same definition ever since.

[Kyle Miller]

An important role for subtype these days is that it's used to create the has_coe_to_sort instance for set. The modern definition for subtype and set are

structure subtype {α : Sort u} (p : α → Prop) :=
(val : α) (property : p val)

def set (α : Type u) := α → Prop

Is there any reason we shouldn't define it as def set (α : Sort u) := α → Prop? This would allow us to write ↥{x | p x} or {x // p x} in all cases.

[Eric Wieser]

I think the answer is that it makes the type of set annoying for universe reasons

[Eric Wieser]

Similar to how we have separate sigma and psigma

[Kyle Miller]

Longer term, it seems that to make subtypes vs coerced sets more streamlined we should really embrace that has_coe_to_sort instance and redefine subtype to

structure subtype {α : Sort u} (s : set α) :=
(val : α) (property : val ∈ s)

which then gives a coercion instance like so: (modulo universe variable mistakes, I haven't tested this)

instance {α : Sort u} : has_coe_to_sort (set α) (Sort (max 1 u)) := ⟨subtype⟩

Then {x // p x} could be convenient notation for just subtype {x | p x}.

[Kyle Miller]

Eric Wieser said:

I think the answer is that it makes the type of set annoying for universe reasons

It's still the case with this that set α : Type u when α : Type u, but now set Prop : Type. Definitions and lemmas around set can still use Type u if that's more convenient universe-wise.

[Kyle Miller]

It might be that sigma vs psigma solves some universe variable issues, but why do we not have subtype and psubtype then? Maybe the reason it's fine for subtype means it can be fine for set.

[Eric Wieser]

It's still the case with this that set α : Type u when α : Type u, but now set Prop : Type.

Are you sure? I think the fear is that you end up with some stupid universe constraint like Sort (max (u+1) 1) (I'm not at lean to check)

[Eric Wieser]

What type is set A under your proposal when A : sort u?

[Kyle Miller]

With this, set : Sort u → Sort (max u 1) (vs the current set : Type u → Type u).

For comparison, right now we have subtype : Π {α : Sort u}, (α → Prop) → Sort (max 1 u).

Also:

• sigma : Π {α : Type u}, (α → Type v) → Type (max u v)
• psigma : Π {α : Sort u}, (α → Sort v) → Sort (max 1 u v)

[Eric Wieser]

Right, so what type is set α under that proposal where α : Type u?

[Kyle Miller]

Are you asking something else that this doesn't answer?
Kyle Miller said:

It's still the case with this that set α : Type u when α : Type u

[Violeta Hernández]

Has anyone tried this?