I suppose, but then your definition of composition requires checking compatibility of codomain/domain instead of it being automatic (and your definition of composition does not fit the shape to form a category), which seems way worse than stipulating f non-empty for some theorem that isn't even true for other categories either.

And for e.g. for vector spaces or modules over semisimple rings they're actually the same so there's a real statement being made to say they're not always.

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.