Zulip Chat Archive

Stream: new members

Topic: Type with one element

Nicolò Cavalleri (Oct 30 2020 at 13:57):

Does there exist in Lean a "canonical type with one element", like in set theory could be the set 1 = {0}? I want to identify type F : Type* with a function 1 \to Type* and I wonder what 1 should be

Mario Carneiro (Oct 30 2020 at 13:59):


Mario Carneiro (Oct 30 2020 at 13:59):

or punit if you need a universe polymorphic version

Eric Wieser (Oct 30 2020 at 14:37):

You can also use [unique T] if you want your theorem to apply to all types T with one element

Last updated: Dec 20 2023 at 11:08 UTC