Zulip Chat Archive
Stream: new members
Topic: Singleton type
Bjørn Kjos-Hanssen (Dec 29 2023 at 03:17):
What's a good way to say that a type has just one element?
We could do
∃! x : α, True
but is there a more direct way, something like this?
isSingletonType α
Mario Carneiro (Dec 29 2023 at 03:29):
Unique A
Mario Carneiro (Dec 29 2023 at 03:29):
Bjørn Kjos-Hanssen (Dec 29 2023 at 03:47):
Mario Carneiro said:
Unique A
Or maybe
Nonempty (Unique A)
Eric Wieser (Dec 29 2023 at 17:21):
Or just Nonempty A
Matt Diamond (Dec 29 2023 at 17:29):
@Eric Wieser that doesn't express that the type only has one element, though
Eric Wieser (Dec 29 2023 at 17:30):
Whoops, I guess I meant [Nonempty A] [Subsingleton A]
Last updated: May 02 2025 at 03:31 UTC