troethe

6 ms·

1. 1.▲
   by troethe 9d ago

   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
2. 2.▲
   by troethe 9d ago

   > 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 `
3. 3.▲
   by troethe 9d ago

   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 `
4. 4.▲
   by troethe 9d ago

   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.
5. 5.▲
   by troethe 9d ago

   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 le
6. 6.▲
   by troethe 7mo ago

   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 anothe