FWIW, Barr and Wells in a well respected reference on category theory
[1] use a different definition of a function than the one in this
book. Essentially they avoid insisting on the concrete model of a
function as a set of ordered pairs (which they call its graph), and
would regard two functions having identical graphs as being
nevertheless distinct if they have different co-domains (section
1.2). IMO their definition is better thought out and ultimately less
troublesome when it comes to reasoning about functions. The definition
of a function is always the first thing I check in any book about math
for a rough assessment of whether reading the rest of it might make me
dumber or smarter.
Indeed. The question "given a function as a set of ordered pairs, write code to decide if it is injective" has an answer, but replace that with "surjective" and suddenly you need to drag the codomain along as an extra parameter or the question makes no sense. This asymmetry bothers me.
EDIT: to be clear, "code" only works if your set is finite, but the principle of "does this question even have an answer" remains "yes" for injective and "no" for surjective without the codomain being named explicitly.
[1] https://abstractmath.org/CTCS/CTCS.pdf