Stream: Is there code for X?
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.
Mario Carneiro (Jul 01 2020 at 17:29):
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
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
Chris Hughes (Jul 01 2020 at 19:59):
pequiv, but that's from subsets to subsets.
Yury G. Kudryashov (Jul 01 2020 at 21:26):
Moreover, there is
Scott Olson (Jul 02 2020 at 14:22):
I guess you're looking for something like
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