subsingleton (set A) of is_empty A

Stream: Is there code for X?

[Rémy Degenne]

Do we have this?

example {α} [is_empty α] : subsingleton (set α) := sorry

[Adam Topaz]

Even better:

import data.set.basic

example {α} [is_empty α] : unique (set α) := by { unfold set, apply_instance }

[Eric Wieser]

I think so, but it's not an instance for performance reasons.

[Eric Wieser]

docs#set.unique_empty

[Adam Topaz]

The general thing is that [is_empty X] implies unique (X \to Y) for any sort Y

[Adam Topaz]

I don't know if we defined the corresponding thing for set X though.

[Rémy Degenne]

if I replace set α by α → Prop the instance is found. But replacing set by its definition is something we should not have to do.

[Adam Topaz]

Yes, I agree. See Eric's link above. It's there.

[Rémy Degenne]

thanks for set.unique_empty!

[Eric Wieser]

Adam confused me into crossing out my comment about it not being an instance

[Eric Wieser]

#6025 tracks the task of actually making it an instanc

[Adam Topaz]

Eric Wieser said:

Adam confused me into crossing out my comment about it not being an instance

sorry ;)