2.6 Cartesian product types

Given types $A$ and $B$, consider the cartesian product type $A\times B$. For any elements $x,y:A\times B$ and a path $p:x=_{A\times B}y$, by functoriality we can extract paths ${\mathsf{pr}_{1}}\mathopen{}\left({p}\right)\mathclose{}:\mathsf{pr}_{1}(x)=_{% A}\mathsf{pr}_{1}(y)$ and ${\mathsf{pr}_{2}}\mathopen{}\left({p}\right)\mathclose{}:\mathsf{pr}_{2}(x)=_{% B}\mathsf{pr}_{2}(y)$. Thus, we have a function

 $(x=_{A\times B}y)\to(\mathsf{pr}_{1}(x)=_{A}\mathsf{pr}_{1}(y))\times(\mathsf{% pr}_{2}(x)=_{B}\mathsf{pr}_{2}(y)).$ (2.6.1)
Theorem 2.6.2.

For any $x$ and $y$, the function (2.6.1) is an equivalence.

Read logically, this says that two pairs are equal if they are equal componentwise. Read category-theoretically, this says that the morphisms in a product groupoid are pairs of morphisms. Read homotopy-theoretically, this says that the paths in a product space are pairs of paths.

Proof.

We need a function in the other direction:

 $(\mathsf{pr}_{1}(x)=_{A}\mathsf{pr}_{1}(y))\times(\mathsf{pr}_{2}(x)=_{B}% \mathsf{pr}_{2}(y))\to(x=_{A\times B}y).$ (2.6.3)

By the induction rule for cartesian products, we may assume that $x$ and $y$ are both pairs, i.e. $x\equiv(a,b)$ and $y\equiv(a^{\prime},b^{\prime})$ for some $a,a^{\prime}:A$ and $b,b^{\prime}:B$. In this case, what we want is a function

 $(a=_{A}a^{\prime})\times(b=_{B}b^{\prime})\to\big{(}(a,b)=_{A\times B}(a^{% \prime},b^{\prime})\big{)}.$

Now by induction for the cartesian product in its domain, we may assume given $p:a=a^{\prime}$ and $q:b=b^{\prime}$. And by two path inductions, we may assume that $a\equiv a^{\prime}$ and $b\equiv b^{\prime}$ and both $p$ and $q$ are reflexivity. But in this case, we have $(a,b)\equiv(a^{\prime},b^{\prime})$ and so we can take the output to also be reflexivity.

It remains to prove that (2.6.3) is quasi-inverse to (2.6.1). This is a simple sequence of inductions, but they have to be done in the right order.

In one direction, let us start with $r:x=_{A\times B}y$. We first do a path induction on $r$ in order to assume that $x\equiv y$ and $r$ is reflexivity. In this case, since $\mathsf{ap}_{\mathsf{pr}_{1}}$ and $\mathsf{ap}_{\mathsf{pr}_{2}}$ are defined by path induction, (2.6.1) takes $r\equiv\mathsf{refl}_{x}$ to the pair $(\mathsf{refl}_{\mathsf{pr}_{1}x},\mathsf{refl}_{\mathsf{pr}_{2}x})$. Now by induction on $x$, we may assume $x\equiv(a,b)$, so that this is $(\mathsf{refl}_{a},\mathsf{refl}_{b})$. Thus, (2.6.3) takes it by definition to $\mathsf{refl}_{(a,b)}$, which (under our current assumptions) is $r$.

In the other direction, if we start with $s:(\mathsf{pr}_{1}(x)=_{A}\mathsf{pr}_{1}(y))\times(\mathsf{pr}_{2}(x)=_{B}% \mathsf{pr}_{2}(y))$, then we first do induction on $x$ and $y$ to assume that they are pairs $(a,b)$ and $(a^{\prime},b^{\prime})$, and then induction on $s:(a=_{A}a^{\prime})\times(b=_{B}b^{\prime})$ to reduce it to a pair $(p,q)$ where $p:a=a^{\prime}$ and $q:b=b^{\prime}$. Now by induction on $p$ and $q$, we may assume they are reflexivities $\mathsf{refl}_{a}$ and $\mathsf{refl}_{b}$, in which case (2.6.3) yields $\mathsf{refl}_{(a,b)}$ and then (2.6.1) returns us to $(\mathsf{refl}_{a},\mathsf{refl}_{b})\equiv(p,q)\equiv s$. ∎

In particular, we have shown that (2.6.1) has an inverse (2.6.3), which we may denote by

 $\mathsf{pair}^{\mathord{=}}:(\mathsf{pr}_{1}(x)=\mathsf{pr}_{1}(y))\times(% \mathsf{pr}_{2}(x)=\mathsf{pr}_{2}(y))\to(x=y).$

Note that a special case of this yields the propositional uniqueness principle for products: $z=(\mathsf{pr}_{1}(z),\mathsf{pr}_{2}(z))$.

It can be helpful to view $\mathsf{pair}^{\mathord{=}}$ as a constructor or introduction rule for $x=y$, analogous to the “pairing” constructor of $A\times B$ itself, which introduces the pair $(a,b)$ given $a:A$ and $b:B$. From this perspective, the two components of (2.6.1):

 $\displaystyle\mathsf{ap}_{\mathsf{pr}_{1}}$ $\displaystyle:(x=y)\to(\mathsf{pr}_{1}(x)=\mathsf{pr}_{1}(y))$ $\displaystyle\mathsf{ap}_{\mathsf{pr}_{2}}$ $\displaystyle:(x=y)\to(\mathsf{pr}_{2}(x)=\mathsf{pr}_{2}(y))$

are elimination rules. Similarly, the two homotopies which witness (2.6.3) as quasi-inverse to (2.6.1) consist, respectively, of propositional computation rules:

 $\displaystyle{\mathsf{ap}_{\mathsf{pr}_{1}}{(\mathsf{pair}^{\mathord{=}}(p,q)})}$ $\displaystyle={p}\qquad\text{for }p:\mathsf{pr}_{1}x=\mathsf{pr}_{1}y$ $\displaystyle{\mathsf{ap}_{\mathsf{pr}_{2}}{(\mathsf{pair}^{\mathord{=}}(p,q)})}$ $\displaystyle={q}\qquad\text{for }q:\mathsf{pr}_{2}x=\mathsf{pr}_{2}y$

and a propositional uniqueness principle:

 $r=\mathsf{pair}^{\mathord{=}}(\mathsf{ap}_{\mathsf{pr}_{1}}(r),\mathsf{ap}_{% \mathsf{pr}_{2}}(r))\qquad\text{for }r:x=_{A\times B}y.$

We can also characterize the reflexivity, inverses, and composition of paths in $A\times B$ componentwise:

 $\displaystyle{\mathsf{refl}_{(z:A\times B)}}$ $\displaystyle={\mathsf{pair}^{\mathord{=}}(\mathsf{refl}_{\mathsf{pr}_{1}z},% \mathsf{refl}_{\mathsf{pr}_{2}z})}$ $\displaystyle{\mathord{{p}^{-1}}}$ $\displaystyle={\mathsf{pair}^{\mathord{=}}\big{(}\mathord{{\mathsf{ap}_{% \mathsf{pr}_{1}}(p)}^{-1}},\,\mathord{{\mathsf{ap}_{\mathsf{pr}_{2}}(p)}^{-1}}% \big{)}}$ $\displaystyle{{p\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle% \centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1% .075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{% \scriptscriptstyle\,\centerdot\,}}}q}}$ $\displaystyle={\mathsf{pair}^{\mathord{=}}\big{(}{\mathsf{ap}_{\mathsf{pr}_{1}% }(p)}\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{% \mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{% \scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle% \,\centerdot\,}}}{\mathsf{ap}_{\mathsf{pr}_{1}}(q)},\,{\mathsf{ap}_{\mathsf{% pr}_{2}}(p)}\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}% }{\mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{% \scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle% \,\centerdot\,}}}{\mathsf{ap}_{\mathsf{pr}_{2}}(q)}\big{)}}.$

The same is true for the rest of the higher groupoid structure considered in §2.1 (http://planetmath.org/21typesarehighergroupoids). All of these equations can be derived by using path induction on the given paths and then returning reflexivity.

We now consider transport in a pointwise product of type families. Given type families $A,B:Z\to\mathcal{U}$, we abusively write $A\times B:Z\to\mathcal{U}$ for the type family defined by $(A\times B)(z):\!\!\equiv A(z)\times B(z)$. Now given $p:z=_{Z}w$ and $x:A(z)\times B(z)$, we can transport $x$ along $p$ to obtain an element of $A(w)\times B(w)$.

Theorem 2.6.4.

In the above situation, we have

 $\mathsf{transport}^{A\times B}(p,x)=_{A(y)\times B(y)}(\mathsf{transport}^{A}(% p,\mathsf{pr}_{1}x),\mathsf{transport}^{B}(p,\mathsf{pr}_{2}x)).$
Proof.

By path induction, we may assume $p$ is reflexivity, in which case we have

 $\displaystyle\mathsf{transport}^{A\times B}(p,x)$ $\displaystyle\equiv x$ $\displaystyle\mathsf{transport}^{A}(p,\mathsf{pr}_{1}x)$ $\displaystyle\equiv\mathsf{pr}_{1}x$ $\displaystyle\mathsf{transport}^{B}(p,\mathsf{pr}_{2}x)$ $\displaystyle\equiv\mathsf{pr}_{2}x.$

Thus, it remains to show $x=(\mathsf{pr}_{1}x,\mathsf{pr}_{2}x)$. But this is the propositional uniqueness principle for product types, which, as we remarked above, follows from Theorem 2.6.2 (http://planetmath.org/26cartesianproducttypes#Thmprethm1). ∎

Finally, we consider the functoriality of $\mathsf{ap}$ under cartesian products. Suppose given types $A,B,A^{\prime},B^{\prime}$ and functions $g:A\to A^{\prime}$ and $h:B\to B^{\prime}$; then we can define a function $f:A\times B\to A^{\prime}\times B^{\prime}$ by $f(x):\!\!\equiv(g(\mathsf{pr}_{1}x),h(\mathsf{pr}_{2}x))$.

Theorem 2.6.5.

In the above situation, given $x,y:A\times B$ and $p:\mathsf{pr}_{1}x=\mathsf{pr}_{1}y$ and $q:\mathsf{pr}_{2}x=\mathsf{pr}_{2}y$, we have

 ${f}\mathopen{}\left({\mathsf{pair}^{\mathord{=}}(p,q)}\right)\mathclose{}=_{(f% (x)=f(y))}\mathsf{pair}^{\mathord{=}}({g}\mathopen{}\left({p}\right)\mathclose% {},{h}\mathopen{}\left({q}\right)\mathclose{}).$
Proof.

Note first that the above equation is well-typed. On the one hand, since $\mathsf{pair}^{\mathord{=}}(p,q):x=y$ we have ${f}\mathopen{}\left({\mathsf{pair}^{\mathord{=}}(p,q)}\right)\mathclose{}:f(x)% =f(y)$. On the other hand, since $\mathsf{pr}_{1}(f(x))\equiv g(\mathsf{pr}_{1}x)$ and $\mathsf{pr}_{2}(f(x))\equiv h(\mathsf{pr}_{2}x)$, we also have $\mathsf{pair}^{\mathord{=}}({g}\mathopen{}\left({p}\right)\mathclose{},{h}% \mathopen{}\left({q}\right)\mathclose{}):f(x)=f(y)$.

Now, by induction, we may assume $x\equiv(a,b)$ and $y\equiv(a^{\prime},b^{\prime})$, in which case we have $p:a=a^{\prime}$ and $q:b=b^{\prime}$. Thus, by path induction, we may assume $p$ and $q$ are reflexivity, in which case the desired equation holds judgmentally. ∎

Title 2.6 Cartesian product types
\metatable