Notation for univ

Stream: general

[Yaël Dillies]

We have no notation for set.univ and finset.univ. What do people think of introducing Ω as such a notation? That would an alternative to using it as the base type in probability theory.
cc @Jason KY.

[Jason KY.]

I think the decision to use of Ω : Type* in probability theory was very popular and I do use set.univ quite often when working with probability so I don't support using Ω for set.univ. It would be useful to have a notation for set.univhowever.

[Junyan Xu]

Is ⊤ not a notation?

[Yaël Dillies]

It's notation for docs#has_top.top

[Eric Rodriguez]

but that is defeq right?

[Yaël Dillies]

But not syntactically equal! So that will mess with rw.

[Yaël Dillies]

So ⊤ is notation for something that's defeq to univ, but that doesn't make it notation for univ.

[Eric Rodriguez]

a notation typeclass will have the same issue, and I'm not sure how you could make notation overriding work here unless you had a different one for finset/set

[Eric Rodriguez]

i guess this comes back to the age-old "we don't want mathematicians to have to use lattices" and stuff like that

[Thomas Browning]

Would redefining set.univ to ⊤ help?

[Yaël Dillies]

Maybe! I just don't want to be murdered by a mob of angry mathematicians.

[Patrick Massot]

I always love notations when they allow to bring Lean code closer to real world math. But set.univdoesn't exist in the real world (or you could say that X is notation for (set.univ : set X)) so I don't think a notation would help here.

[Johan Commelin]

Exactly for the reason that Patrick says, I wouldn't really mind writing ⊤ everywhere. I think that for a random mathematician ⊤ has about the same clarity as univ.

[Eric Rodriguez]

but we still preserve emptyc, right?

[Wrenna Robson]

Yeah, I have to say unless you are getting rid of emptyc I don't think this is a good idea.

[Wrenna Robson]

Do we use ℧ for anything?

[Wrenna Robson]

It has the advantage of looking a bit like a weird U

[Wrenna Robson]

but is also upside-down Ω so it has that association.

[Wrenna Robson]

Conceptually, I think the reason I don't like the top/bottom symbols is that while there is a natural lattice on sets, somehow the definition of sets doesn't rest on that - the empty and universal sets are defined before the lattice.

[Wrenna Robson]

Also, there might be contexts where you have a lattice of sets and you want to talk about the top of that lattice as opposed to the universal set.

[Eric Rodriguez]

the definition is already there, and you can already get goals of the form \top = coe \top today.

[Wrenna Robson]

True, true.

[Violeta Hernández]

I like ⊤. I don't want yet another ⊥ vs Ø vs 0 situation :stuck_out_tongue: