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
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 , perhaps because it allows us to write "For every "?
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 corresponds to something like Lean's
nonempty (A ≅ B) -- ours is a predicate. And what are all those
→ₐ things? They're all just .
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):
nonempty is in the root namespace because it is actually
Last updated: May 18 2021 at 07:19 UTC