2
According to the first chapter of the HoTT book, dependent functions beget products:
$$
(x : A) \rightarrow B\,x \equiv: \prod_{x : A} B\,x
$$
of which $A \times B$ is a special form ($A \times B \cong \prod_{b : \mathrm{Bool}} T\,b, T\,\mathrm{false} = A, T\,\mathrm{true} = B$),
and likewise, de...
