why `nonempty`?

Stream: maths

[Kevin Buzzard]

So the community seems to have decided that the best way to express the predicate "I am non-empty" on a term of type set X is via dot notation, i.e. defining the predicate set.nonempty. Is it just true in general that any predicate P on set X should just be called set.P and should always be dealt with that way, and we can just let the notationiser fix this up, because it looks weird for mathematicians? [For linguistic reasons unrelated to computers, we mathematicians adopted the notation $X\not=\emptyset$, perhaps because it allows us to write "For every $\emptyset\not=X\in S,\ldots$"?

[Kevin Buzzard]

Also, which predicates should be classes?

[Kevin Buzzard]

I also think that current mathematical usage of $A\cong B$ corresponds to something like Lean's nonempty (A ≅ B) -- ours is a predicate. And what are all those →ₐ things? They're all just $\to$.

[Mario Carneiro]

I think the reason it is called set.nonempty is simply because nonempty already exists and means something else

[Mario Carneiro]

I would say it is similar to nat.succ; you don't have to use dot notation for it, it's just in the namespace, but you can if you want

[Kevin Buzzard]

We don't mind you using it, we just want it to be hidden from us by the notationizer.

[Kevin Buzzard]

Presumably nonempty is in the root namespace because it is actually Sort.nonempty