# The uniqueness principle for products in the HoTT Book

This is about a point I do not understand in Section 1.5 of the HoTT Book. Here is the relevant excerpt:

To be able to define dependent functions over the product type, we have to generalize the recursor. Given $C:A\times B\to\mathcal U$, we may define a function $$f:\prod_{(x:A\times B)}C(x)$$ by providing a function $$g:\prod_{(x:A)}\prod_{(y:B)}C((x,y))$$ with defining equation $$f((x,y)):\equiv g(x)(y).$$ For example, in this way we can prove the propositional uniqueness principle, which says that every element of $A\times B$ is equal to a pair. Specifically, we can construct a function $$\operatorname{uniq}_{A\times B}:\prod_{x:A\times B}\Big(\big(\operatorname{pr_1}(x),\operatorname{pr_2}(x)\big)=_{A\times B}x\Big).$$ Here we are using the identity type, which we are going to introduce below in $\S$1.12. However, all we need to know now is that there is a reflexivity element $$\operatorname{refl}_x:x=_Ax$$ for any $x:A$. Given this, we can define $$\operatorname{uniq}_{A\times B}((a,b)):\equiv\operatorname{refl}_{(a,b)}.\tag{1}$$ This construction works, because in the case that $x:\equiv(a,b)$ we can calculate $$\Big(\operatorname{pr_1}\big((a,b)\big),\operatorname{pr_2}\big((a,b)\big)\Big)\equiv(a,b)$$ using the defining equations for the projections. Therefore, $$\operatorname{refl}_{(a,b)}:\Big(\operatorname{pr_1}\big((a,b)\big),\operatorname{pr_2}\big((a,b)\big)\Big)=(a,b)$$ is well-typed, since both sides of the equality are judgmentally equal.

The whole section is available at http://planetmath.org/15producttypes. The whole book is available at http://homotopytypetheory.org/book/. (To find the above paragraph in the section or in the book, you can search for the chain of characters "works, because".)

I think I see why the judgmental equality $$\Big(\operatorname{pr_1}\big((a,b)\big),\operatorname{pr_2}\big((a,b)\big)\Big)\equiv(a,b)$$ holds for all $a:A$ and all $b:B$. The authors seem to say that this implies that the judgmental equality $$\big(\operatorname{pr_1}(x),\operatorname{pr_2}(x)\big)\equiv x$$ holds for all $x:A\times B$. I do not understand why.

Instead of $(1)$ I would have expected $$\operatorname{uniq}_{A\times B}(x):\equiv\operatorname{refl}_x,\tag{2}$$ but even with $(1)$ replaced by $(2)$ my non understanding remains.

• I would not say that the judgemental equality for $x$ follows from the judgemental equality for $(a, b)$, but certainly the propositional equality follows. Dec 21, 2014 at 9:25
• Your comment confirms the fact that I don't understand the point! Could you spell out the reason why the propositional equality for $x$ follows from the judgemental equality for $(a,b)$? (When I posted the question, I told myself: "the best thing that could happen would be that @ZhenLin answers it". I'm delighted!) Dec 21, 2014 at 9:43
• It has to do with the induction principle for products. Dec 21, 2014 at 10:14
• @ZhenLin - Thanks! But my non understanding of HoTT is such that I need a detailed explanation rather than a hint... Dec 21, 2014 at 11:20

You have copied out the induction principle for products. We are now applying that principle with the type family $C(x) :\equiv (((\mathsf{pr}_1(x),\mathsf{pr}_2(x))=x)$. The desired function $f$ will be our proof that $((\mathsf{pr}_1(x),\mathsf{pr}_2(x))=x)$ for all $x:A\times B$. The induction principle says that to obtain $f$, it suffices to give $g$, which means to show that $((\mathsf{pr}_1((a,b)),\mathsf{pr}_2((a,b)))=(a,b))$ for all $a:A$ and $b:B$. But in this case, the two sides are judgmentally equal, so we can define $g(a,b):\equiv \mathsf{refl}_{(a,b)}$.