3
$\begingroup$

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.

$\endgroup$
4
  • $\begingroup$ I would not say that the judgemental equality for $x$ follows from the judgemental equality for $(a, b)$, but certainly the propositional equality follows. $\endgroup$
    – Zhen Lin
    Dec 21, 2014 at 9:25
  • $\begingroup$ 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!) $\endgroup$ Dec 21, 2014 at 9:43
  • $\begingroup$ It has to do with the induction principle for products. $\endgroup$
    – Zhen Lin
    Dec 21, 2014 at 10:14
  • 1
    $\begingroup$ @ZhenLin - Thanks! But my non understanding of HoTT is such that I need a detailed explanation rather than a hint... $\endgroup$ Dec 21, 2014 at 11:20

1 Answer 1

3
$\begingroup$

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)}$.

$\endgroup$
1
  • 1
    $\begingroup$ Thank you very much for such a clear answer!!! $\endgroup$ Dec 22, 2014 at 7:59

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.