Dependent left_inverse

Stream: Is there code for X?

[Yakov Pechersky]

In #8885, I define the "obvious" inverse to coercing to a "with_top R", which needs a hypothesis to hold. What's the canonical way of phrasing this property? Is it via docs#set.inv_on and friends?

[Yakov Pechersky]

Unfortunately even those don't provide a dependent proof that one is actually in the set, for either the f or f'

[Yakov Pechersky]

@Anne Baanen

[Anne Baanen]

Most of this "logic" stuff seems to avoid dependent functions, so I don't expect there is a property quite like the one we're looking for.