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.