2.6 Cartesian product types
For any and , 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.
We need a function in the other direction:
By the induction rule for cartesian products, we may assume that and are both pairs, i.e. and for some and . In this case, what we want is a function
Now by induction for the cartesian product in its domain, we may assume given and . And by two path inductions, we may assume that and and both and are reflexivity. But in this case, we have and so we can take the output to also be reflexivity.
In one direction, let us start with . We first do a path induction on in order to assume that and is reflexivity. In this case, since and are defined by path induction, (2.6.1) takes to the pair . Now by induction on , we may assume , so that this is . Thus, (2.6.3) takes it by definition to , which (under our current assumptions) is .
In the other direction, if we start with , then we first do induction on and to assume that they are pairs and , and then induction on to reduce it to a pair where and . Now by induction on and , we may assume they are reflexivities and , in which case (2.6.3) yields and then (2.6.1) returns us to . ∎
Note that a special case of this yields the propositional uniqueness principle for products: .
It can be helpful to view as a constructor or introduction rule for , analogous to the “pairing” constructor of itself, which introduces the pair given and . From this perspective, the two components of (2.6.1):
and a propositional uniqueness principle:
We can also characterize the reflexivity, inverses, and composition of paths in componentwise:
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 , we abusively write for the type family defined by . Now given and , we can transport along to obtain an element of .
In the above situation, we have
By path induction, we may assume is reflexivity, in which case we have
Thus, it remains to show . 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 and functions and ; then we can define a function by .
In the above situation, given and and , we have
Note first that the above equation is well-typed. On the one hand, since we have . On the other hand, since and , we also have .
Now, by induction, we may assume and , in which case we have and . Thus, by path induction, we may assume and are reflexivity, in which case the desired equation holds judgmentally. ∎
|Title||2.6 Cartesian product types|