bundled one-sided invertible functions

Stream: Is there code for X?

[Eric Wieser]

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]

There is encodable A

[Eric Wieser]

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

[Eric Wieser]

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]

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

[Yury G. Kudryashov]

Moreover, there is pequiv and local_equiv.

[Scott Olson]

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?