troethe

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.

> your fix kinda breaks a lot of the structure of algebra in other ways

What are you referring to here in particular?

I think the property of `g` to be a well defined function is a lot more important than for its domain to be `B`, when `f(A)` is enough to make the composition well defined.

Of course I can compose `f: A -> B` and `g: f(A) -> A`. The composition maps a `x` from `A` to `g(f(x))` which is well defined. Therefore the composition is a function.

`g` and `f` aren't functions in a programming language and `A` and `B` are not types. There is nothing like a type checker forbidding you from composing `f: A -> B` and `g: f(A) -> A`.

No, f can still map to `B` and does not need to be surjective. We just loosened the definition of `g` a little in a way that doesn't matter.

While the proposed fix of requiring "either that A be inhabited or that B be uninhabited" works, it seems tacked on just to solve this particular edge-case.

I think a more elegant solution would be to soften the definition of a left inverse from a function `g: B -> A` to a function `g: f(A) -> A` where `f(A)` is the subset of elements in `B`, that actually get mapped to by `f` or in the words of the book's function definition, the set of "right" elements in `f`.

This solves the edge-case too, as `f(A) = f({}) = {}` and there exists (exactly one) function `g: {} -> {}`, which also trivially is a left inverse of `f`.

The real problem here was, that the statement `g: B -> A` needlessly required `g` to map back elements in B to A, that couldn't even be produced by `f` and should therefore be irrelevant for a left inverse.

On a lot of linux distros there is the `moreutils` package, which contains a command called `chronic`. Originally intended to be used in crontabs, it executes a command and only outputs its output if it fails. I think this could find another use case here.