bundled surjective function

Stream: Is there code for X?

[Matt Diamond]

Does mathlib have a bundled surjective function type, like the way function.embedding is a bundled injective function?

[Matt Diamond]

I found a message from Aug 19, 2021 that mentioned not having them, but wanted to check if anything had changed since then.

[Junyan Xu]

Someone asked about bundled bijection more recently, but I think the answer to both is no.

[Matt Diamond]

gotcha

[Kevin Buzzard]

Is the lack of bundled surjectivity just a coincidence?

[Yaël Dillies]

Where does it come up? To me, injection shows up mostly because it represents subobjects.

[Kevin Buzzard]

Then surjection represents quotient objects

[Junyan Xu]

docs#finset.map uses embedding, and of course also Schröder–Bernstein (docs#function.embedding.antisymm with unbundled version above it). What are other prominent uses?