What's the need for a pair type $A \times B$ in Homotopy Type Theory? I'm reading the Homotopy Type Theory book and I got confused about the following issue.


*

*The book defines a primitive $\Pi$-type  as the generalization of the function type.

*The $\Pi$-type can be regarded as the Cartesian product over a family of types:
$$\Pi_{x:A}B(x)$$
(that is, the "set" of all functions from $x:A$ to $B(x)$)

*Now immediately after the book defines a primitive product type $A \times B$ and call it their Cartesian product.


Given that we already have the $\Pi$-type to stand for the generalized version of the Cartesian products, defining a product type $A \times B$ as a primitive type in HoTT seems superfluous to me, since cartesian products could, in principle, be constructed by the $\Pi$-type. So I ask:

Why is the product type $A \times B$ really needed in HoTT?

At the same time, what are the constructors and eliminators of the product type $A \times B$ ?
It seems to me it is so:


*

*constructor: $α→β →(α × β)$

*eliminator 1: $(α × β)→α$ 

*eliminator 2: $(α × β)→β$


If it is correct, it makes me even more confused: if we can construct $α × β$ from the function type, it seems to me the function type is more basic, so that the product type is superfluous.
I would be glad if you shed some light on the issue.
 A: 
Why is the product type $A\times B$ really needed in HoTT?

Two answers:


*

*See exercise 1.6.  You can construct $A\times B$ as a special case of a $\Pi$-type, but it requires function extensionality, and only satisfies the laws propositionally.

*The goal is not to give an absolutely minimal axiomatization of a theory.  Exercise 1.5 shows that we could omit general coproduct types without these problems, but coproducts are conceptually and practically important.  Analogously, introductions to set theory usually state separation and replacement separately even though the former follows from the latter.  Here, we also have that all of these are special cases of the general notion of inductive type, which is what we really want to assert.

if we can construct α×β from the function type, it seems to me the function type is more basic, so that the product type is superfluous.

The fact that the eliminator and constructors of the product are functions does not mean the product is constructed from the function type.
