Does the output of a total function need to be unique against the input? I'm reading Semantics with Applications and I'm confused about their definition of a total function. They define a function like so: N : Num → Z. And then they give some examples of N, and then state: > We have a total function N , if for all arguments n ∈ Num there is exactly one number n ∈ Z such that N [[n]] = n I get that total functions are basically functions defined on all inputs. But I don't understand why we need to additionally stipulate that there must be exactly one number n ∈ Z such that N [[n]] = n.

The stipulation is mostly relevant for preventing the instance of multivalued functions - functions that attain multiple values for a given input. For example, you could define $f(x) =\pm \sqrt x$ and then have $f(4)=2$ and $f(4)=-2$.

This stipulation prevents such cases.

That's not to say multivalued functions aren't useful or ever considered. But it seems that, with your first forays into functions and set theory and such, you'll usually stick to single-valued functions.

(There might be similar notions of totality for multivalued functions that don't make the stipulation, but this isn't something I would know about. If I had to guess as to _why_ we make the stipulation beyond "we want to focus on single-valued functions," I guess it's because multivalued functions might be more complicated to handle and that single-valued functions are easier and more familiar with most people.)