Derivation of product type eliminator in type theory

Question

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?

Answer 1

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