Zulip Chat Archive

Stream: Is there code for X?

Topic: bundled one-sided invertible functions


view this post on Zulip Eric Wieser (Jul 01 2020 at 17:23):

I recently found (function.embedding) for injective functions - is there a similar type for functions bundled with a one-sided inverse? I found for functions with a two-sided inverse.

view this post on Zulip Mario Carneiro (Jul 01 2020 at 17:29):

There is encodable A

view this post on Zulip Eric Wieser (Jul 01 2020 at 17:39):

I think I'm looking for that but a) without the constraint on nat, and b) in the form of a structure like embedding.

view this post on Zulip Eric Wieser (Jul 01 2020 at 17:41):

Perhaps I should be thinking of a two-sided inverse from A to a subset of B, instead of a one-sided inverse from A to B

view this post on Zulip Chris Hughes (Jul 01 2020 at 19:59):

There is pequiv, but that's from subsets to subsets.

view this post on Zulip Yury G. Kudryashov (Jul 01 2020 at 21:26):

Moreover, there is pequiv and local_equiv.

view this post on Zulip Scott Olson (Jul 02 2020 at 14:22):

I guess you're looking for something like split_epi/split_mono but specialized to types and functions instead of objects and arrows in any category?


Last updated: May 17 2021 at 16:26 UTC