# 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.

## 1 Answer

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.

• This question shows a common problem that many students have with definitions in math. It comes up when you define a word that already has connotations, in this case "function". The only data you can use in proofs based on this new definition are the properties given by the definition (until someone has proved some theorems you can use). If the fact that a function in the general usage of mathematical English is determined by its values is not given in the definition, you can't use it. In general, if you see a math definition of a word, throw away its connotations! – SixWingedSeraph Aug 17 '16 at 21:27
• 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
• Yes, that's right. – Mike Shulman Aug 18 '16 at 5:02
• @Zhangsheng ''I do not know product types are actually pairs" But isn't that obvious from the fact that the constructor of product type creates elements by making pairs? Why bother proving that by defining dependent functions out of product types? – pxc3110 Jan 2 at 21:01
• @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