Zulip Chat Archive

Stream: Is there code for X?

Topic: singleton embedding


view this post on Zulip Yakov Pechersky (Mar 17 2021 at 16:39):

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?

view this post on Zulip Mario Carneiro (Mar 17 2021 at 16:41):

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

view this post on Zulip Mario Carneiro (Mar 17 2021 at 16:41):

you can define an is_lawful_singleton A unit instance

view this post on Zulip Yakov Pechersky (Mar 17 2021 at 16:42):

Ah, different "law"s then.


Last updated: May 07 2021 at 20:11 UTC