In HoTT book, section 1.5 (Product Types) in order to define the eliminators for the product type it assumes a function of type $g:A \rightarrow B \rightarrow C$ and then goes on to define the eliminator rule ,saying that we can define a function $f:A \times B \rightarrow C $ for any such g by:

$f((a, b)) :\equiv g (a) (b)$.

Then it states that

Note that in set theory, we would justify the above definition of $f$ by the fact that every element of $A \times B$ is an ordered pair, so that it suffices to define $f$ on such pairs. By contrast, type theory reverses the situation: we assume that a function on $A \times B$ is well-defined as soon as we specify its values on pairs, and from this we will be able to prove that every element of $A \times B$ is a pair.

Would you please explain in further detail what the above paragraph is trying to state?

  • $\begingroup$ It is just talking about the Intuitionistic proof theoritic way of proving that such a function $f$ does exist in comparison to set theoritic way of proving it. $\endgroup$ – Apoorv Jan 12 at 2:08

What is meant here, is that you can construct an identification $x=(\mathsf{pr}_1(x),\mathsf{pr}_2(x))$ for any $x:A\times B$. In other words, you can show $$\Pi_{(x:A\times B)}x=(\mathsf{pr}_1(x),\mathsf{pr}_2(x)).$$ In order to do this, we use the induction principle of $A\times B$. By the induction principle it suffices to show that $$\Pi_{(a:A)}\Pi_{(b:B)}(a,b)=(\mathsf{pr}_1(a,b),\mathsf{pr}_2(a,b)).$$ Now you simply observe that by the definition of the projection maps, there are judgmental equalities $\mathsf{pr}_1(a,b)\equiv a$ and $\mathsf{pr}_2(a,b)\equiv b$. Therefore, the above type reduces to $$\Pi_{(a:A)}\Pi_{(b:B)}(a,b)=(a,b),$$ which can be proved by reflexivity.

We conclude that every element of $A\times B$ can be identified with a pair, namely the pair of its own projections. The same is true for $\Sigma_{(x:A)}B(x)$.

| cite | improve this answer | |

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.