2.6 Cartesian product types

Given types A and B, consider the cartesian productMathworldPlanetmath type AΓ—B. For any elements x,y:AΓ—B and a path p:x=AΓ—By, by functoriality we can extract paths 𝗉𝗋1(p):𝗉𝗋1(x)=A𝗉𝗋1(y) and 𝗉𝗋2(p):𝗉𝗋2(x)=B𝗉𝗋2(y). Thus, we have a function

(x=AΓ—By)β†’(𝗉𝗋1(x)=A𝗉𝗋1(y))Γ—(𝗉𝗋2(x)=B𝗉𝗋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 productPlanetmathPlanetmath groupoidPlanetmathPlanetmathPlanetmathPlanetmath are pairs of morphisms. Read homotopy-theoretically, this says that the paths in a product space are pairs of paths.


We need a function in the other direction:

(𝗉𝗋1(x)=A𝗉𝗋1(y))Γ—(𝗉𝗋2(x)=B𝗉𝗋2(y))β†’(x=AΓ—By). (2.6.3)

By the inductionMathworldPlanetmath rule for cartesian products, we may assume that x and y are both pairs, i.e.Β x≑(a,b) and y≑(aβ€²,bβ€²) for some a,aβ€²:A and b,bβ€²:B. In this case, what we want is a function


Now by induction for the cartesian product in its domain, we may assume given p:a=aβ€² and q:b=bβ€². And by two path inductions, we may assume that a≑aβ€² and b≑bβ€² and both p and q are reflexivityMathworldPlanetmath. But in this case, we have (a,b)≑(aβ€²,bβ€²) and so we can take the output to also be reflexivity.

It remains to prove thatΒ (2.6.3) is quasi-inversePlanetmathPlanetmath 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Γ—By. We first do a path induction on r in order to assume that x≑y and r is reflexivity. In this case, since 𝖺𝗉𝗉𝗋1 and 𝖺𝗉𝗉𝗋2 are defined by path induction,Β (2.6.1) takes r≑𝗋𝖾𝖿𝗅x to the pair (𝗋𝖾𝖿𝗅𝗉𝗋1⁒x,𝗋𝖾𝖿𝗅𝗉𝗋2⁒x). Now by induction on x, we may assume x≑(a,b), so that this is (𝗋𝖾𝖿𝗅a,𝗋𝖾𝖿𝗅b). Thus,Β (2.6.3) takes it by definition to 𝗋𝖾𝖿𝗅(a,b), which (under our current assumptionsPlanetmathPlanetmath) is r.

In the other direction, if we start with s:(𝗉𝗋1(x)=A𝗉𝗋1(y))Γ—(𝗉𝗋2(x)=B𝗉𝗋2(y)), then we first do induction on x and y to assume that they are pairs (a,b) and (aβ€²,bβ€²), and then induction on s:(a=Aaβ€²)Γ—(b=Bbβ€²) to reduce it to a pair (p,q) where p:a=aβ€² and q:b=bβ€². Now by induction on p and q, we may assume they are reflexivities 𝗋𝖾𝖿𝗅a and 𝗋𝖾𝖿𝗅b, in which caseΒ (2.6.3) yields 𝗋𝖾𝖿𝗅(a,b) and thenΒ (2.6.1) returns us to (𝗋𝖾𝖿𝗅a,𝗋𝖾𝖿𝗅b)≑(p,q)≑s. ∎

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


Note that a special case of this yields the propositional uniqueness principle for products: z=(𝗉𝗋1⁒(z),𝗉𝗋2⁒(z)).

It can be helpful to view 𝗉𝖺𝗂𝗋= as a constructor or introduction rule for x=y, analogous to the β€œpairing” constructor of AΓ—B itself, which introduces the pair (a,b) given a:A and b:B. From this perspective, the two components ofΒ (2.6.1):

𝖺𝗉𝗉𝗋1 :(x=y)β†’(𝗉𝗋1(x)=𝗉𝗋1(y))
𝖺𝗉𝗉𝗋2 :(x=y)β†’(𝗉𝗋2(x)=𝗉𝗋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:

𝖺𝗉𝗉𝗋1⁒(𝗉𝖺𝗂𝗋=⁒(p,q)) =p  for ⁒p:𝗉𝗋1⁒x=𝗉𝗋1⁒y
𝖺𝗉𝗉𝗋2⁒(𝗉𝖺𝗂𝗋=⁒(p,q)) =q  for ⁒q:𝗉𝗋2⁒x=𝗉𝗋2⁒y

and a propositional uniqueness principle:

r=𝗉𝖺𝗂𝗋=⁒(𝖺𝗉𝗉𝗋1⁒(r),𝖺𝗉𝗉𝗋2⁒(r))  for ⁒r:x=AΓ—By.

We can also characterize the reflexivity, inverses, and composition of paths in AΓ—B componentwise:

𝗋𝖾𝖿𝗅(z:AΓ—B) =𝗉𝖺𝗂𝗋=⁒(𝗋𝖾𝖿𝗅𝗉𝗋1⁒z,𝗋𝖾𝖿𝗅𝗉𝗋2⁒z)
p-1 =𝗉𝖺𝗂𝗋=⁒(𝖺𝗉𝗉𝗋1⁒(p)-1,𝖺𝗉𝗉𝗋2⁒(p)-1)
p⁒\centerdot⁒q =𝗉𝖺𝗂𝗋=⁒(𝖺𝗉𝗉𝗋1⁒(p)⁒\centerdot⁒𝖺𝗉𝗉𝗋1⁒(q),𝖺𝗉𝗉𝗋2⁒(p)⁒\centerdot⁒𝖺𝗉𝗉𝗋2⁒(q)).

The same is true for the rest of the higher groupoid structureMathworldPlanetmath 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→𝒰, we abusively write AΓ—B:Z→𝒰 for the type family defined by (AΓ—B)(z):≑A(z)Γ—B(z). Now given p:z=Zw and x:A⁒(z)Γ—B⁒(z), we can transport x along p to obtain an element of A⁒(w)Γ—B⁒(w).

Theorem 2.6.4.

In the above situation, we have


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

π—π—‹π–Ίπ—‡π—Œπ—‰π—ˆπ—‹π—AΓ—B⁒(p,x) ≑x
π—π—‹π–Ίπ—‡π—Œπ—‰π—ˆπ—‹π—A⁒(p,𝗉𝗋1⁒x) ≑𝗉𝗋1⁒x
π—π—‹π–Ίπ—‡π—Œπ—‰π—ˆπ—‹π—B⁒(p,𝗉𝗋2⁒x) ≑𝗉𝗋2⁒x.

Thus, it remains to show x=(𝗉𝗋1⁒x,𝗉𝗋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 𝖺𝗉 under cartesian products. Suppose given types A,B,Aβ€²,Bβ€² and functions g:Aβ†’Aβ€² and h:Bβ†’Bβ€²; then we can define a function f:AΓ—Bβ†’Aβ€²Γ—Bβ€² by f(x):≑(g(𝗉𝗋1x),h(𝗉𝗋2x)).

Theorem 2.6.5.

In the above situation, given x,y:AΓ—B and p:pr1⁒x=pr1⁒y and q:pr2⁒x=pr2⁒y, we have


Note first that the above equation is well-typed. On the one hand, since 𝗉𝖺𝗂𝗋=⁒(p,q):x=y we have f(𝗉𝖺𝗂𝗋=(p,q)):f(x)=f(y). On the other hand, since 𝗉𝗋1⁒(f⁒(x))≑g⁒(𝗉𝗋1⁒x) and 𝗉𝗋2⁒(f⁒(x))≑h⁒(𝗉𝗋2⁒x), we also have 𝗉𝖺𝗂𝗋=(g(p),h(q)):f(x)=f(y).

Now, by induction, we may assume x≑(a,b) and y≑(aβ€²,bβ€²), in which case we have p:a=aβ€² and q:b=bβ€². 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