Type with one element

Stream: new members

[Nicolò Cavalleri]

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]

unit

[Mario Carneiro]

or punit if you need a universe polymorphic version

[Eric Wieser]

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