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 ${\mathrm{𝗉𝗋}}_1\left(p\right):{\mathrm{𝗉𝗋}}_1(x){=}_A{\mathrm{𝗉𝗋}}_1(y)$ and ${\mathrm{𝗉𝗋}}_2\left(p\right):{\mathrm{𝗉𝗋}}_2(x){=}_B{\mathrm{𝗉𝗋}}_2(y)$. Thus, we have a function

$$(x{=}_{A\times B}y)\to ({\mathrm{𝗉𝗋}}_1(x){=}_A{\mathrm{𝗉𝗋}}_1(y))\times ({\mathrm{𝗉𝗋}}_2(x){=}_B{\mathrm{𝗉𝗋}}_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:

$$({\mathrm{𝗉𝗋}}_1(x){=}_A{\mathrm{𝗉𝗋}}_1(y))\times ({\mathrm{𝗉𝗋}}_2(x){=}_B{\mathrm{𝗉𝗋}}_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 \left((a,b){=}_{A\times B}(a^{\prime },b^{\prime })\right).$$

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 ${\mathrm{𝖺𝗉}}_{{\mathrm{𝗉𝗋}}_1}$ and ${\mathrm{𝖺𝗉}}_{{\mathrm{𝗉𝗋}}_2}$ are defined by path induction, (2.6.1) takes $r\equiv {\mathrm{𝗋𝖾𝖿𝗅}}_x$ to the pair $({\mathrm{𝗋𝖾𝖿𝗅}}_{{\mathrm{𝗉𝗋}}_{1}x},{\mathrm{𝗋𝖾𝖿𝗅}}_{{\mathrm{𝗉𝗋}}_{2}x})$. Now by induction on $x$, we may assume $x\equiv (a,b)$, so that this is $({\mathrm{𝗋𝖾𝖿𝗅}}_a,{\mathrm{𝗋𝖾𝖿𝗅}}_b)$. Thus, (2.6.3) takes it by definition to ${\mathrm{𝗋𝖾𝖿𝗅}}_{(a,b)}$, which (under our current assumptions) is $r$.

In the other direction, if we start with $s:({\mathrm{𝗉𝗋}}_1(x){=}_A{\mathrm{𝗉𝗋}}_1(y))\times ({\mathrm{𝗉𝗋}}_2(x){=}_B{\mathrm{𝗉𝗋}}_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 ${\mathrm{𝗋𝖾𝖿𝗅}}_a$ and ${\mathrm{𝗋𝖾𝖿𝗅}}_b$, in which case (2.6.3) yields ${\mathrm{𝗋𝖾𝖿𝗅}}_{(a,b)}$ and then (2.6.1) returns us to $({\mathrm{𝗋𝖾𝖿𝗅}}_a,{\mathrm{𝗋𝖾𝖿𝗅}}_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

$${\mathrm{𝗉𝖺𝗂𝗋}}^{\mathrm{=}}:({\mathrm{𝗉𝗋}}_1(x)={\mathrm{𝗉𝗋}}_1(y))\times ({\mathrm{𝗉𝗋}}_2(x)={\mathrm{𝗉𝗋}}_2(y))\to (x=y).$$

Note that a special case of this yields the propositional uniqueness principle for products: $z=({\mathrm{𝗉𝗋}}_1(z),{\mathrm{𝗉𝗋}}_2(z))$.

It can be helpful to view ${\mathrm{𝗉𝖺𝗂𝗋}}^{\mathrm{=}}$ 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):

${\mathrm{𝖺𝗉}}_{{\mathrm{𝗉𝗋}}_1}$ $:(x=y)\to ({\mathrm{𝗉𝗋}}_1(x)={\mathrm{𝗉𝗋}}_1(y))$

${\mathrm{𝖺𝗉}}_{{\mathrm{𝗉𝗋}}_2}$ $:(x=y)\to ({\mathrm{𝗉𝗋}}_2(x)={\mathrm{𝗉𝗋}}_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:

${\mathrm{𝖺𝗉}}_{{\mathrm{𝗉𝗋}}_1}({\mathrm{𝗉𝖺𝗂𝗋}}^{\mathrm{=}}(p,q))$ $=p\mathit{\hspace{1em}\hspace{1em}}\text{for }p:{\mathrm{𝗉𝗋}}_{1}x={\mathrm{𝗉𝗋}}_{1}y$

${\mathrm{𝖺𝗉}}_{{\mathrm{𝗉𝗋}}_2}({\mathrm{𝗉𝖺𝗂𝗋}}^{\mathrm{=}}(p,q))$ $=q\mathit{\hspace{1em}\hspace{1em}}\text{for }q:{\mathrm{𝗉𝗋}}_{2}x={\mathrm{𝗉𝗋}}_{2}y$

and a propositional uniqueness principle:

$$r={\mathrm{𝗉𝖺𝗂𝗋}}^{\mathrm{=}}({\mathrm{𝖺𝗉}}_{{\mathrm{𝗉𝗋}}_1}(r),{\mathrm{𝖺𝗉}}_{{\mathrm{𝗉𝗋}}_2}(r))\mathit{\hspace{1em}\hspace{1em}}\text{for }r:x{=}_{A\times B}y.$$

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

${\mathrm{𝗋𝖾𝖿𝗅}}_{(z:A\times B)}$ $={\mathrm{𝗉𝖺𝗂𝗋}}^{\mathrm{=}}({\mathrm{𝗋𝖾𝖿𝗅}}_{{\mathrm{𝗉𝗋}}_{1}z},{\mathrm{𝗋𝖾𝖿𝗅}}_{{\mathrm{𝗉𝗋}}_{2}z})$

$p^{-1}$ $={\mathrm{𝗉𝖺𝗂𝗋}}^{\mathrm{=}}({\mathrm{𝖺𝗉}}_{{\mathrm{𝗉𝗋}}_1}{(p)}^{-1},{\mathrm{𝖺𝗉}}_{{\mathrm{𝗉𝗋}}_2}{(p)}^{-1})$

$pq$ $={\mathrm{𝗉𝖺𝗂𝗋}}^{\mathrm{=}}({\mathrm{𝖺𝗉}}_{{\mathrm{𝗉𝗋}}_1}(p){\mathrm{𝖺𝗉}}_{{\mathrm{𝗉𝗋}}_1}(q),{\mathrm{𝖺𝗉}}_{{\mathrm{𝗉𝗋}}_2}(p){\mathrm{𝖺𝗉}}_{{\mathrm{𝗉𝗋}}_2}(q)).$

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 𝒰$, we abusively write $A\times B:Z\to 𝒰$ 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

$${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{A\times B}(p,x){=}_{A(y)\times B(y)}({\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^A(p,{\mathrm{𝗉𝗋}}_{1}x),{\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^B(p,{\mathrm{𝗉𝗋}}_{2}x)).$$

Proof.

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

${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{A\times B}(p,x)$ $\equiv x$

${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^A(p,{\mathrm{𝗉𝗋}}_{1}x)$ $\equiv {\mathrm{𝗉𝗋}}_{1}x$

${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^B(p,{\mathrm{𝗉𝗋}}_{2}x)$ $\equiv {\mathrm{𝗉𝗋}}_{2}x.$

Thus, it remains to show $x=({\mathrm{𝗉𝗋}}_{1}x,{\mathrm{𝗉𝗋}}_{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 $\mathrm{𝖺𝗉}$ 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({\mathrm{𝗉𝗋}}_{1}x),h({\mathrm{𝗉𝗋}}_{2}x))$.

Theorem 2.6.5.

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

$$f\left({\mathrm{𝗉𝖺𝗂𝗋}}^{\mathrm{=}}(p,q)\right){=}_{(f(x)=f(y))}{\mathrm{𝗉𝖺𝗂𝗋}}^{\mathrm{=}}(g\left(p\right),h\left(q\right)).$$

Proof.

Note first that the above equation is well-typed. On the one hand, since ${\mathrm{𝗉𝖺𝗂𝗋}}^{\mathrm{=}}(p,q):x=y$ we have $f\left({\mathrm{𝗉𝖺𝗂𝗋}}^{\mathrm{=}}(p,q)\right):f(x)=f(y)$. On the other hand, since ${\mathrm{𝗉𝗋}}_1(f(x))\equiv g({\mathrm{𝗉𝗋}}_{1}x)$ and ${\mathrm{𝗉𝗋}}_2(f(x))\equiv h({\mathrm{𝗉𝗋}}_{2}x)$, we also have ${\mathrm{𝗉𝖺𝗂𝗋}}^{\mathrm{=}}(g\left(p\right),h\left(q\right)):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