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.
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.