Stream: maths

Topic: why nonempty?

Kevin Buzzard (Feb 16 2020 at 11:16):

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 (Feb 16 2020 at 11:17):

Also, which predicates should be classes?

Kevin Buzzard (Feb 16 2020 at 11:36):

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 (Feb 16 2020 at 12:04):

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

Mario Carneiro (Feb 16 2020 at 12:05):

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 (Feb 16 2020 at 12:36):

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

Kevin Buzzard (Feb 16 2020 at 12:38):

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

Last updated: May 18 2021 at 07:19 UTC