singleton embedding

Stream: Is there code for X?

[Yakov Pechersky]

I can write:

/-- Promoting a `a : α` into `{a} : finset α` in an embedding. -/
def finset.singleton_embedding : α ↪ finset α := ⟨λ a, {a}, λ a b, singleton_inj.mp⟩

but I would think this is true for any is_lawful_singleton. Is it? Or at least, it seems to be the case for all the things that are an instance of is_lawful_singleton. Would providing singleton as an embedding in a generalized way be possible?

[Mario Carneiro]

No, is_lawful_singleton only says that singleton a = insert a empty, it doesn't say anything about injectivity

[Mario Carneiro]

you can define an is_lawful_singleton A unit instance

[Yakov Pechersky]

Ah, different "law"s then.