alt Hacker NewsOf 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`.
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.