Let be a type and a type family. Recall that the -type, or dependent pair type, is a generalization of the cartesian product type. Thus, we expect its higher groupoid structure to also be a generalization of the previous section. In particular, its paths should be pairs of paths, but it takes a little thought to give the correct types of these paths.
Suppose that we have a path in . Then we get . However, we cannot directly ask whether is identical to since they don’t have to be in the same type. But we can transport along the path , and this does give us an element of the same type as . By path induction, we do in fact obtain a path .
Recall from the discussion preceding Lemma 2.3.4 (http://planetmath.org/23typefamiliesarefibrations#Thmprelem3) that can be regarded as the type of paths from to which lie over the path in . Thus, we are saying that a path in the total space determines (and is determined by) a path in together with a path from to lying over , which seems sensible.
Note that if we have and such that , it does not follow that . All we can conclude is that there exists such that . This is a well-known source of confusion for newcomers to type theory, but it makes sense from a topological viewpoint: the existence of a path in the total space of a fibration between two points that happen to lie in the same fiber does not imply the existence of a path lying entirely within that fiber.
The next theorem states that we can also reverse this process. Since it is a direct generalization of Theorem 2.6.2 (http://planetmath.org/26cartesianproducttypes#Thmprethm1), we will be more concise.
Suppose that is a type family over a type and let . Then there is an equivalence
We define for any , a function
by path induction, with
We want to show that is an equivalence.
In the reverse direction, we define
by first inducting on and , which splits them into and respectively, so it suffices to show
Next, given a pair , we can use -induction to get and . Inducting on , we have , and it suffices to show . But , so inducting on reduces to the goal to , which we can prove with .
Next we show that is the identity for all , and , where has type
First, we break apart the pairs , , and by pair induction, as in the definition of , and then use two path inductions to reduce both components of to . Then it suffices to show that , which is true by definition.
Similarly, to show that is the identity for all , , and , we can do path induction on , and then induction to split , at which point it suffices to show that , which is true by definition.
Thus, has a quasi-inverse, and is therefore an equivalence. ∎
As we did in the case of cartesian products, we can deduce a propositional uniqueness principle as a special case.
For , we have .
We have , so by Theorem 2.7.2 (http://planetmath.org/27sigmatypes#Thmprethm1) it will suffice to exhibit a path . But both sides are judgmentally equal to . ∎
Like with binary cartesian products, we can think of the backward direction of Theorem 2.7.2 (http://planetmath.org/27sigmatypes#Thmprethm1) as an introduction form (), the forward direction as elimination forms ( and ), and the equivalence as giving a propositional computation rule and uniqueness principle for these.
Note that the lifted path of at defined in Lemma 2.3.2 (http://planetmath.org/23typefamiliesarefibrations#Thmprelem2) may be identified with the special case of the introduction form
This appears in the statement of action of transport on -types, which is also a generalization of the action for binary cartesian products:
Suppose we have type families
Then we can construct the type family over defined by
For any path and any we have
Immediate by path induction. ∎
We leave it to the reader to state and prove a generalization of Theorem 2.6.5 (http://planetmath.org/26cartesianproducttypes#Thmprethm3) (see http://planetmath.org/node/87638Exercise 2.7), and to characterize the reflexivity, inverses, and composition of -types componentwise.