2.3 Type families are fibrations
Since dependently typed functions are essential in type theory, we will also need a version of Lemma 2.2.1 (http://planetmath.org/22functionsarefunctors#Thmprelem1) for these. However, this is not quite so simple to state, because if and , then and are elements of distinct types, so that a priori we cannot even ask whether they are equal. The missing ingredient is that itself gives us a way to relate the types and .
Lemma 2.3.1 (Transport).
Suppose that is a type family over and that . Then there is a function .
Let be the type family defined by
Then we have the function
so that the induction principle gives us for , which we define to be . ∎
By induction, it suffices to assume is . But in this case, we can take to be the identity function. ∎
Sometimes, it is necessary to notate the type family in which the transport operation happens. In this case, we may write
Recall that a type family over a type can be seen as a property of elements of , which holds at in if is inhabited. Then the transportation lemma says that respects equality, in the sense that if is equal to , then holds if and only if holds. In fact, we will see later on that if then actually and are equivalent.
Topologically, the transportation lemma can be viewed as a “path lifting” operation in a fibration. We think of a type family as a fibration with base space , with being the fiber over , and with being the total space of the fibration, with first projection . The defining property of a fibration is that given a path in the base space and a point in the fiber over , we may lift the path to a path in the total space starting at . The point can be thought of as the other endpoint of this lifted path. We can also define the path itself in type theory:
Lemma 2.3.2 (Path lifting property).
Let be a type family over and assume we have for some . Then for any , we have
Left to the reader. We will prove a more general theorem in §2.7 (http://planetmath.org/27sigmatypes). ∎
In classical homotopy theory, a fibration is defined as a map for which there exist liftings of paths; while in contrast, we have just shown that in type theory, every type family comes with a specified “path-lifting function”. This accords with the philosophy of constructive mathematics, according to which we cannot show that something exists except by exhibiting it.
Although we may think of a type family as like a fibration, it is generally not a good idea to say things like “the fibration ”, since this sounds like we are talking about a fibration with base and total space . To repeat, when a type family is regarded as a fibration, the base is and the total space is .
We may also occasionally use other topological terminology when speaking about type families. For instance, we may refer to a dependent function as a section of the fibration , and we may say that something happens fiberwise if it happens for each . For instance, a section shows that is “fiberwise inhabited”.
Now we can prove the dependent version of Lemma 2.2.1 (http://planetmath.org/22functionsarefunctors#Thmprelem1). The topological intuition is that given and a path , we ought to be able to apply to and obtain a path in the total space of which “lies over” , as shown below.
We can obtain such a thing from Lemma 2.2.1 (http://planetmath.org/22functionsarefunctors#Thmprelem1). Given , we can define a non-dependent function by setting , and then consider . However, it is not obvious from the type of such a path that it lies over a specific path in (in this case, ), which is sometimes important.
The solution is to use the transport lemma. Since there is a canonical path from to which (at least intuitively) lies over , any path from to lying over should factor through this path, essentially uniquely, by a path from to lying entirely in the fiber . Thus, up to equivalence, it makes sense to define “a path from to lying over ” to mean a path in . And, indeed, we can show that dependent functions produce such paths.
Lemma 2.3.4 (Dependent map).
Suppose ; then we have a map
Let be the type family defined by
Then is . But since , we get that . Thus, we find the function
and now path induction gives us for each . ∎
By induction, it suffices to assume is . But in this case, the desired equation is , which holds judgmentally. ∎
We will refer generally to paths which “lie over other paths” in this sense as dependent paths. They will play an increasingly important role starting in http://planetmath.org/node/87579Chapter 6. In §2.5 (http://planetmath.org/25thehighergroupoidstructureoftypeformers) we will see that for a few particular kinds of type families, there are equivalent ways to represent the notion of dependent paths that are sometimes more convenient.
Now recall from §1.4 (http://planetmath.org/14dependentfunctiontypes) that a non-dependently typed function is just the special case of a dependently typed function when is a constant type family, . In this case, and are closely related, because of the following lemma:
If is defined by for a fixed , then for any and and we have a path
Fix a , and let be the type family defined by
Then is , which is judgmentally equal to by the computation rule for transporting. Thus, we have the function
Now path induction gives us an element of as desired. ∎
By induction, it suffices to assume is and is . But , so in this case what we have to prove is , and we have for this. ∎
Thus, by concatenating with , for any and and we obtain functions
In fact, these functions are inverse equivalences (in the sense to be introduced in §2.4 (http://planetmath.org/24homotopiesandequivalences)), and they relate to .
For and , we have
Let be the type family defined by
Thus, we have
But by definition, all three paths appearing in this type are , so we have
Thus, path induction gives us an element of , which is what we wanted. ∎
By induction, it suffices to assume is and is . In this case, what we have to prove is , which is true judgmentally. ∎
Because the types of and are different, it is often clearer to use different notations for them.
At this point, we hope the reader is starting to get a feel for proofs by induction on identity types. From now on we stop giving both styles of proofs, allowing ourselves to use whatever is most clear and convenient (and often the second, more concise one). Here are a few other useful lemmas about transport; we leave it to the reader to give the proofs (in either style).
Given with and while , we have
For a function and a type family , and any and , we have
For and a family of functions , and any and , we have
|Title||2.3 Type families are fibrations|