I think we can sit here and speculate which properties of left inverses are actually important for quite a while.

But we will only ever get a real answer to this question, when the original poster finishes formalizing the whole book and can tell us which weakenings break further proofs in the books and which won't.