# Derivation of product type eliminator in type theory

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?

• 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. Jan 12 '20 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)$$.