I am currently trying to understand the first chapter of the HoTT book and for 1.2 Functions Types of the book,



> 
> Since it is by definition ``the function that applies $f$ to its argument'' we consider it to be definitional equal to $f$:
>  $$
> f\equiv (\lambda x.f(x))
> $$
>  This equality is the **uniqueness principle for functions types**, because it shows that $f$ is uniquely determined by its values.
> 
> 
> 


I can understand its definitional equality as it is by construction. But I do not understand why we need to establish or state this uniqueness principle. I am tempted to think of this uniqueness principle as obvious, but I think there is some underlying reason for this. I am guessing it has to do with the big picture of how each type is introduced systematically by the formation, introduction, elimination, computation rules but I can't seem to relate to them.


Thank you very much.



Uniqueness Principle for function types
It is not true "by construction". Remember that at this point in the theory a "function" is an abstract undefined thing, not something "defined by its action on inputs" as it is in set theory. The only thing we can do with a "function" is apply it to an argument; the only way we have to make "functions" is to $\lambda$-abstract take an expression involving a variable. So if I have a "function" $f$, apply it to a variable $x$ to get an expression $f(x)$, then abstract that to get $\lambda x.f(x)$, I have a new "function". There's nothing in this abstract picture (before we assert the uniqueness principle) that says that this new "function" must be the same as the "function" $f$ that I started with.


