1.5 Product types

Given types $A,B:\mathcal{U}$ we introduce the type $A\times B:\mathcal{U}$ , which we call their cartesian product. We also introduce a nullary product type, called the unit type $\mathbf{1}:\mathcal{U}$ . We intend the elements of $A\times B$ to be pairs $(a,b):A\times B$ , where $a : A$ and $b : B$ , and the only element of $\mathbf{1}$ to be some particular object $\star:\mathbf{1}$ . However, unlike in set theory, where we define ordered pairs to be particular sets and then collect them all together into the cartesian product, in type theory, ordered pairs are a primitive concept, as are functions.

Remark 1.5.1.

There is a general pattern for introduction of a new kind of type in type theory, and because products are our second example following this pattern,¹¹The description of universes above is an exception. it is worth emphasizing the general form: To specify a type, we specify:

1.

how to form new types of this kind, via formation rules. (For example, we can form the function type $A\to B$ when $A$ is a type and when $B$ is a type. We can form the dependent function type $\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)% }}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod% _{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}% }{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}B(x)$ when $A$ is a type and $B(x)$ is a type for $x : A$ .)
2.

how to construct elements of that type. These are called the type’s constructors or introduction rules. (For example, a function type has one constructor, $\lambda$ -abstraction. Recall that a direct definition like $f(x):\!\!\equiv 2x$ can equivalently be phrased as a $\lambda$ -abstraction $f:\!\!\equiv{\lambda}x.\,2x$ .)
3.

how to use elements of that type. These are called the type’s eliminators or elimination rules. (For example, the function type has one eliminator, namely function application.)
4.

a computation rule²²also referred to as $\beta$ -reduction, which expresses how an eliminator acts on a constructor. (For example, for functions, the computation rule states that $({\lambda}x.\,\Phi)(a)$ is judgmentally equal to the substitution of $a$ for $x$ in $\Phi$ .)
5.

an optional uniqueness principle³³also referred to as $\eta$ -expansion, which expresses uniqueness of maps into or out of that type. For some types, the uniqueness principle characterizes maps into the type, by stating that every element of the type is uniquely determined by the results of applying eliminators to it, and can be reconstructed from those results by applying a constructor—thus expressing how constructors act on eliminators, dually to the computation rule. (For example, for functions, the uniqueness principle says that any function $f$ is judgmentally equal to the “expanded” function ${\lambda}x.\,f(x)$ , and thus is uniquely determined by its values.) For other types, the uniqueness principle says that every map (function) from that type is uniquely determined by some data. (An example is the coproduct type introduced in §1.7 (http://planetmath.org/17coproducttypes), whose uniqueness principle is mentioned in §2.15 (http://planetmath.org/215universalproperties).)

When the uniqueness principle is not taken as a rule of judgmental equality, it is often nevertheless provable as a propositional equality from the other rules for the type. In this case we call it a propositional uniqueness principle. (In later chapters we will also occasionally encounter propositional computation rules.)

The inference rules in §A.3 (http://planetmath.org/a3homotopytypetheory) are organized and named accordingly; see, for example, §A.2.4 (http://planetmath.org/a24dependentfunctiontypespitypes), where each possibility is realized.

The way to construct pairs is obvious: given $a : A$ and $b : B$ , we may form $(a,b):A\times B$ . Similarly, there is a unique way to construct elements of $\mathbf{1}$ , namely we have $\star:\mathbf{1}$ . We expect that “every element of $A\times B$ is a pair”, which is the uniqueness principle for products; we do not assert this as a rule of type theory, but we will prove it later on as a propositional equality.

Now, how can we use pairs, i.e. how can we define functions out of a product type? Let us first consider the definition of a non-dependent function $f:A\times B\to C$ . Since we intend the only elements of $A\times B$ to be pairs, we expect to be able to define such a function by prescribing the result when $f$ is applied to a pair $(a,b)$ . We can prescribe these results by providing a function $g:A\to B\to C$ . Thus, we introduce a new rule (the elimination rule for products), which says that for any such $g$ , we can define a function $f:A\times B\to C$ by

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

We avoid writing $g(a,b)$ here, in order to emphasize that $g$ is not a function on a product. (However, later on in the book we will often write $g(a,b)$ both for functions on a product and for curried functions of two variables.) This defining equation is the computation rule for product types.

Note that in set theory, we would justify the above definition of $f$ by the fact that every element of $A\times B$ is a pair, so that it suffices to define $f$ on 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 tuples, and from this (or more precisely, from its more general version for dependent functions, below) we will be able to prove that every element of $A\times B$ is a pair. From a category-theoretic perspective, we can say that we define the product $A\times B$ to be left adjoint to the “exponential” $B\to C$ , which we have already introduced.

As an example, we can derive the projection functions

	$\displaystyle\mathsf{pr}_{1}$	$\displaystyle:A\times B\to A$
	$\displaystyle\mathsf{pr}_{2}$	$\displaystyle:A\times B\to B$

with the defining equations

	$\displaystyle\mathsf{pr}_{1}((a,b))$	$\displaystyle:\!\!\equiv a$
	$\displaystyle\mathsf{pr}_{2}((a,b))$	$\displaystyle:\!\!\equiv b.$

Rather than invoking this principle of function definition every time we want to define a function, an alternative approach is to invoke it once, in a universal case, and then simply apply the resulting function in all other cases. That is, we may define a function of type

\mathsf{rec}_{A\times B}:\mathchoice{\prod_{C:\mathcal{U}}\,}{\mathchoice{{% \textstyle\prod_{(C:\mathcal{U})}}}{\prod_{(C:\mathcal{U})}}{\prod_{(C:% \mathcal{U})}}{\prod_{(C:\mathcal{U})}}}{\mathchoice{{\textstyle\prod_{(C:% \mathcal{U})}}}{\prod_{(C:\mathcal{U})}}{\prod_{(C:\mathcal{U})}}{\prod_{(C:% \mathcal{U})}}}{\mathchoice{{\textstyle\prod_{(C:\mathcal{U})}}}{\prod_{(C:% \mathcal{U})}}{\prod_{(C:\mathcal{U})}}{\prod_{(C:\mathcal{U})}}}(A\to B\to C)% \to A\times B\to C

(1.5.2)

with the defining equation

\mathsf{rec}_{A\times B}(C,g,(a,b)):\!\!\equiv g(a)(b).

Then instead of defining functions such as $\mathsf{pr}_{1}$ and $\mathsf{pr}_{2}$ directly by a defining equation, we could define

	$\displaystyle\mathsf{pr}_{1}$	$\displaystyle:\!\!\equiv\mathsf{rec}_{A\times B}(A,{\lambda}a.\,{\lambda}b.\,a)$
	$\displaystyle\mathsf{pr}_{2}$	$\displaystyle:\!\!\equiv\mathsf{rec}_{A\times B}(B,{\lambda}a.\,{\lambda}b.\,b).$

We refer to the function $\mathsf{rec}_{A\times B}$ as the recursor for product types. The name “recursor” is a bit unfortunate here, since no recursion is taking place. It comes from the fact that product types are a degenerate example of a general framework for inductive types, and for types such as the natural numbers, the recursor will actually be recursive. We may also speak of the recursion principle for cartesian products, meaning the fact that we can define a function $f:A\times B\to C$ as above by giving its value on pairs.

We leave it as a simple exercise to show that the recursor can be derived from the projections and vice versa.

We also have a recursor for the unit type:

\mathsf{rec}_{\mathbf{1}}:\mathchoice{\prod_{C:\mathcal{U}}\,}{\mathchoice{{% \textstyle\prod_{(C:\mathcal{U})}}}{\prod_{(C:\mathcal{U})}}{\prod_{(C:% \mathcal{U})}}{\prod_{(C:\mathcal{U})}}}{\mathchoice{{\textstyle\prod_{(C:% \mathcal{U})}}}{\prod_{(C:\mathcal{U})}}{\prod_{(C:\mathcal{U})}}{\prod_{(C:% \mathcal{U})}}}{\mathchoice{{\textstyle\prod_{(C:\mathcal{U})}}}{\prod_{(C:% \mathcal{U})}}{\prod_{(C:\mathcal{U})}}{\prod_{(C:\mathcal{U})}}}C\to\mathbf{1% }\to C

with the defining equation

\mathsf{rec}_{\mathbf{1}}(C,c,\star):\!\!\equiv c.

Although we include it to maintain the pattern of type definitions, the recursor for $\mathbf{1}$ is completely useless, because we could have defined such a function directly by simply ignoring the argument of type $\mathbf{1}$ .

To be able to define dependent functions over the product type, we have to generalize the recursor. Given $C:A\times B\to\mathcal{U}$ , we may define a function $f:\mathchoice{\prod_{x:A\times B}\,}{\mathchoice{{\textstyle\prod_{(x:A\times B% )}}}{\prod_{(x:A\times B)}}{\prod_{(x:A\times B)}}{\prod_{(x:A\times B)}}}{% \mathchoice{{\textstyle\prod_{(x:A\times B)}}}{\prod_{(x:A\times B)}}{\prod_{(% x:A\times B)}}{\prod_{(x:A\times B)}}}{\mathchoice{{\textstyle\prod_{(x:A% \times B)}}}{\prod_{(x:A\times B)}}{\prod_{(x:A\times B)}}{\prod_{(x:A\times B% )}}}C(x)$ by providing a function $g:\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:% A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{% \prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x% :A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}\mathchoice{\prod_{y:B}\,}% {\mathchoice{{\textstyle\prod_{(y:B)}}}{\prod_{(y:B)}}{\prod_{(y:B)}}{\prod_{(% y:B)}}}{\mathchoice{{\textstyle\prod_{(y:B)}}}{\prod_{(y:B)}}{\prod_{(y:B)}}{% \prod_{(y:B)}}}{\mathchoice{{\textstyle\prod_{(y:B)}}}{\prod_{(y:B)}}{\prod_{(% y:B)}}{\prod_{(y:B)}}}C((x,y))$ with defining equation

f((x,y)):\!\!\equiv g(x)(y).

For example, in this way we can prove the propositional uniqueness principle, which says that every element of $A\times B$ is equal to a pair. Specifically, we can construct a function

\mathsf{uppt}:\mathchoice{\prod_{x:A\times B}\,}{\mathchoice{{\textstyle\prod_% {(x:A\times B)}}}{\prod_{(x:A\times B)}}{\prod_{(x:A\times B)}}{\prod_{(x:A% \times B)}}}{\mathchoice{{\textstyle\prod_{(x:A\times B)}}}{\prod_{(x:A\times B% )}}{\prod_{(x:A\times B)}}{\prod_{(x:A\times B)}}}{\mathchoice{{\textstyle% \prod_{(x:A\times B)}}}{\prod_{(x:A\times B)}}{\prod_{(x:A\times B)}}{\prod_{(% x:A\times B)}}}((\mathsf{pr}_{1}{(x)},\mathsf{pr}_{2}{(x)})=_{A\times B}x).

Here we are using the identity type, which we are going to introduce below in §1.12 (http://planetmath.org/112identitytypes). However, all we need to know now is that there is a reflexivity element $\mathsf{refl}_{x}:x=_{A}x$ for any $x : A$ . Given this, we can define

\mathsf{uppt}((a,b)):\!\!\equiv\mathsf{refl}_{(a,b)}.

This construction works, because in the case that $x:\!\!\equiv(a,b)$ we can calculate

(\mathsf{pr}_{1}((a,b)),\mathsf{pr}_{2}{((a,b))})\equiv(a,b)

using the defining equations for the projections. Therefore,

\mathsf{refl}_{(a,b)}:(\mathsf{pr}_{1}((a,b)),\mathsf{pr}_{2}{((a,b))})=(a,b)

is well-typed, since both sides of the equality are judgmentally equal.

More generally, the ability to define dependent functions in this way means that to prove a property for all elements of a product, it is enough to prove it for its canonical elements, the tuples. When we come to inductive types such as the natural numbers, the analogous property will be the ability to write proofs by induction. Thus, if we do as we did above and apply this principle once in the universal case, we call the resulting function induction for product types: given $A,B:\mathcal{U}$ we have

\mathsf{ind}_{A\times B}:\mathchoice{\prod_{C:A\times B\to\mathcal{U}}\,}{% \mathchoice{{\textstyle\prod_{(C:A\times B\to\mathcal{U})}}}{\prod_{(C:A\times B% \to\mathcal{U})}}{\prod_{(C:A\times B\to\mathcal{U})}}{\prod_{(C:A\times B\to% \mathcal{U})}}}{\mathchoice{{\textstyle\prod_{(C:A\times B\to\mathcal{U})}}}{% \prod_{(C:A\times B\to\mathcal{U})}}{\prod_{(C:A\times B\to\mathcal{U})}}{% \prod_{(C:A\times B\to\mathcal{U})}}}{\mathchoice{{\textstyle\prod_{(C:A\times B% \to\mathcal{U})}}}{\prod_{(C:A\times B\to\mathcal{U})}}{\prod_{(C:A\times B\to% \mathcal{U})}}{\prod_{(C:A\times B\to\mathcal{U})}}}\Bigl{(}\mathchoice{\prod_% {(x:A)}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}% }{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_% {(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}% {\prod_{(x:A)}}{\prod_{(x:A)}}}\mathchoice{\prod_{(y:B)}\,}{\mathchoice{{% \textstyle\prod_{(y:B)}}}{\prod_{(y:B)}}{\prod_{(y:B)}}{\prod_{(y:B)}}}{% \mathchoice{{\textstyle\prod_{(y:B)}}}{\prod_{(y:B)}}{\prod_{(y:B)}}{\prod_{(y% :B)}}}{\mathchoice{{\textstyle\prod_{(y:B)}}}{\prod_{(y:B)}}{\prod_{(y:B)}}{% \prod_{(y:B)}}}C((x,y))\Bigr{)}\to\mathchoice{\prod_{x:A\times B}\,}{% \mathchoice{{\textstyle\prod_{(x:A\times B)}}}{\prod_{(x:A\times B)}}{\prod_{(% x:A\times B)}}{\prod_{(x:A\times B)}}}{\mathchoice{{\textstyle\prod_{(x:A% \times B)}}}{\prod_{(x:A\times B)}}{\prod_{(x:A\times B)}}{\prod_{(x:A\times B% )}}}{\mathchoice{{\textstyle\prod_{(x:A\times B)}}}{\prod_{(x:A\times B)}}{% \prod_{(x:A\times B)}}{\prod_{(x:A\times B)}}}C(x)

with the defining equation

\mathsf{ind}_{A\times B}(C,g,(a,b)):\!\!\equiv g(a)(b).

Similarly, we may speak of a dependent function defined on pairs being obtained from the induction principle of the cartesian product. It is easy to see that the recursor is just the special case of induction in the case that the family $C$ is constant. Because induction describes how to use an element of the product type, induction is also called the (dependent) eliminator, and recursion the non-dependent eliminator.

Induction for the unit type turns out to be more useful than the recursor:

\mathsf{ind}_{\mathbf{1}}:\mathchoice{\prod_{C:\mathbf{1}\to\mathcal{U}}\,}{% \mathchoice{{\textstyle\prod_{(C:\mathbf{1}\to\mathcal{U})}}}{\prod_{(C:% \mathbf{1}\to\mathcal{U})}}{\prod_{(C:\mathbf{1}\to\mathcal{U})}}{\prod_{(C:% \mathbf{1}\to\mathcal{U})}}}{\mathchoice{{\textstyle\prod_{(C:\mathbf{1}\to% \mathcal{U})}}}{\prod_{(C:\mathbf{1}\to\mathcal{U})}}{\prod_{(C:\mathbf{1}\to% \mathcal{U})}}{\prod_{(C:\mathbf{1}\to\mathcal{U})}}}{\mathchoice{{\textstyle% \prod_{(C:\mathbf{1}\to\mathcal{U})}}}{\prod_{(C:\mathbf{1}\to\mathcal{U})}}{% \prod_{(C:\mathbf{1}\to\mathcal{U})}}{\prod_{(C:\mathbf{1}\to\mathcal{U})}}}C(% \star)\to\mathchoice{\prod_{x:\mathbf{1}}\,}{\mathchoice{{\textstyle\prod_{(x:% \mathbf{1})}}}{\prod_{(x:\mathbf{1})}}{\prod_{(x:\mathbf{1})}}{\prod_{(x:% \mathbf{1})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbf{1})}}}{\prod_{(x:% \mathbf{1})}}{\prod_{(x:\mathbf{1})}}{\prod_{(x:\mathbf{1})}}}{\mathchoice{{% \textstyle\prod_{(x:\mathbf{1})}}}{\prod_{(x:\mathbf{1})}}{\prod_{(x:\mathbf{1% })}}{\prod_{(x:\mathbf{1})}}}C(x)

with the defining equation

\mathsf{ind}_{\mathbf{1}}(C,c,\star):\!\!\equiv c.

Induction enables us to prove the propositional uniqueness principle for $\mathbf{1}$ , which asserts that its only inhabitant is $\star$ . That is, we can construct

\mathsf{upun}:\mathchoice{\prod_{x:\mathbf{1}}\,}{\mathchoice{{\textstyle\prod% _{(x:\mathbf{1})}}}{\prod_{(x:\mathbf{1})}}{\prod_{(x:\mathbf{1})}}{\prod_{(x:% \mathbf{1})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbf{1})}}}{\prod_{(x:% \mathbf{1})}}{\prod_{(x:\mathbf{1})}}{\prod_{(x:\mathbf{1})}}}{\mathchoice{{% \textstyle\prod_{(x:\mathbf{1})}}}{\prod_{(x:\mathbf{1})}}{\prod_{(x:\mathbf{1% })}}{\prod_{(x:\mathbf{1})}}}x=\star

by using the defining equations

\mathsf{upun}(\star):\!\!\equiv\mathsf{refl}_{\star}

or equivalently by using induction:

\mathsf{upun}:\!\!\equiv\mathsf{ind}_{\mathbf{1}}({\lambda}x.\,x=\star,\mathsf% {refl}_{\star}).

Title	1.5 Product types
\metatable