# Uniqueness Principle for function types

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.

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.
• With your explanations, I think it also explains to me why in the first paragraph of 1.2 it says that functions are a primitive concept in type theory! Hence, in 1.5 Product types which is also a primitive concept, there is a need to prove that every element of $A \times B$ is a pair $(a,b)$. Then, the introduction of product types seems to be saying, ''I do not know product types are actually pairs, but by defining dependent functions out of product types, I can then prove that the elements of $A \times B$ are indeed the pairs I hoped for it to be.' Is this what it says? – Zhangsheng Aug 18 '16 at 1:29
• @pxc3110 The constructor tells you that some elements of product types are pairs, but by itself that doesn't tell you that all elements of product types are pairs. You need some way to say "all elements of the type are obtained from its constructors", and for product types defined as in the HoTT Book, that's exactly what the elimination rule does. (There is another way to define product types, called a "negative" presentation, where instead of an elimination rule you have primitive projections and a uniqueness principle $p \equiv (\pi_1(p),\pi_2(p))$, which then plays that role.) – Mike Shulman Jan 3 at 6:22