2.3 Type families are fibrations

Since dependently typed functions are essential in type theoryPlanetmathPlanetmath, 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 f:(x:A)B(x) and p:x=y, then f(x):B(x) and f(y):B(y) are elements of distinct types, so that a priori we cannot even ask whether they are equal. The missing ingredient is that p itself gives us a way to relate the types B(x) and B(y).

Lemma 2.3.1 (Transport).

Suppose that P is a type family over A and that p:x=Ay. Then there is a function p*:P(x)P(y).

First proof.

Let D:(x,y:A)(p:x=y)𝒰 be the type family defined by


Then we have the function


so that the inductionMathworldPlanetmath principle gives us 𝗂𝗇𝖽=A(D,d,x,y,p):P(x)P(y) for p:x=y, which we define to be p*. ∎

Second proof.

By induction, it suffices to assume p is 𝗋𝖾𝖿𝗅x. But in this case, we can take (𝗋𝖾𝖿𝗅x)*:P(x)P(x) to be the identity function. ∎

Sometimes, it is necessary to notate the type family P in which the transport operationMathworldPlanetmath happens. In this case, we may write


Recall that a type family P over a type A can be seen as a property of elements of A, which holds at x in A if P(x) is inhabited. Then the transportation lemma says that P respects equality, in the sense that if x is equal to y, then P(x) holds if and only if P(y) holds. In fact, we will see later on that if x=y then actually P(x) and P(y) are equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmath.

Topologically, the transportation lemma can be viewed as a “path lifting” operation in a fibrationMathworldPlanetmath. We think of a type family P:A𝒰 as a fibration with base space A, with P(x) being the fiber over x, and with (x:A)P(x) being the total space of the fibration, with first projection (x:A)P(x)A. The defining property of a fibration is that given a path p:x=y in the base space A and a point u:P(x) in the fiber over x, we may lift the path p to a path in the total space starting at u. The point p*(u) 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 P:AU be a type family over A and assume we have u:P(x) for some x:A. Then for any p:x=y, we have


in (x:A)P(x).


Left to the reader. We will prove a more general theoremMathworldPlanetmath 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.

Remark 2.3.3.

Although we may think of a type family P:AU as like a fibration, it is generally not a good idea to say things like “the fibration P:AU”, since this sounds like we are talking about a fibration with base U and total space A. To repeat, when a type family P:AU is regarded as a fibration, the base is A and the total space is (x:A)P(x).

We may also occasionally use other topological terminology when speaking about type families. For instance, we may refer to a dependent function f:(x:A)P(x) as a sectionPlanetmathPlanetmathPlanetmath of the fibration P, and we may say that something happens fiberwise if it happens for each P(x). For instance, a section f:(x:A)P(x) shows that P 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 f:(x:A)P(x) and a path p:x=Ay, we ought to be able to apply f to p and obtain a path in the total space of P which “lies over” p, as shown below.



We can obtain such a thing from Lemma 2.2.1 (http://planetmath.org/22functionsarefunctors#Thmprelem1). Given f:(x:A)P(x), we can define a non-dependent function f:A(x:A)P(x) by setting f(x):(x,f(x)), and then consider f(p):f(x)=f(y). However, it is not obvious from the type of such a path that it lies over a specific path in A (in this case, p), which is sometimes important.

The solution is to use the transport lemma. Since there is a canonical path from u:P(x) to p*(u):P(y) which (at least intuitively) lies over p, any path from u to v:P(y) lying over p should factor through this path, essentially uniquely, by a path from p*(u) to v lying entirely in the fiber P(y). Thus, up to equivalence, it makes sense to define “a path from u to v lying over p:x=y” to mean a path p*(u)=v in P(y). And, indeed, we can show that dependent functions produce such paths.

Lemma 2.3.4 (Dependent map).

Suppose f:(x:A)P(x); then we have a map

First proof.

Let D:(x,y:A)(p:x=y)𝒰 be the type family defined by


Then D(x,x,𝗋𝖾𝖿𝗅x) is (𝗋𝖾𝖿𝗅x)*(f(x))=f(x). But since (𝗋𝖾𝖿𝗅x)*(f(x))f(x), we get that D(x,x,𝗋𝖾𝖿𝗅x)(f(x)=f(x)). Thus, we find the function


and now path induction gives us 𝖺𝗉𝖽f(p):p*(f(x))=f(y) for each p:x=y. ∎

Second proof.

By induction, it suffices to assume p is 𝗋𝖾𝖿𝗅x. But in this case, the desired equation is (𝗋𝖾𝖿𝗅x)*(f(x))f(x), 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 f:AB is just the special case of a dependently typed function f:(x:A)P(x) when P is a constant type family, P(x):B. In this case, 𝖺𝗉𝖽f and 𝖺𝗉f are closely related, because of the following lemma:

Lemma 2.3.5.

If P:AU is defined by P(x):B for a fixed B:U, then for any x,y:A and p:x=y and b:B we have a path

First proof.

Fix a b:B, and let D:(x,y:A)(p:x=y)𝒰 be the type family defined by


Then D(x,x,𝗋𝖾𝖿𝗅x) is (𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍P(𝗋𝖾𝖿𝗅x,b)=b), which is judgmentally equal to (b=b) by the computation rule for transporting. Thus, we have the function


Now path induction gives us an element of (x,y:A)(p:x=y)(𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍P(p,b)=b), as desired. ∎

Second proof.

By induction, it suffices to assume y is x and p is 𝗋𝖾𝖿𝗅x. But 𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍P(𝗋𝖾𝖿𝗅x,b)b, so in this case what we have to prove is b=b, and we have 𝗋𝖾𝖿𝗅b for this. ∎

Thus, by concatenating with 𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍𝖼𝗈𝗇𝗌𝗍pB(b), for any x,y:A and p:x=y and f:AB we obtain functions

(f(x)=f(y)) (p*(f(x))=f(y))  and (2.3.6)
(p*(f(x))=f(y)) (f(x)=f(y)). (2.3.7)

In fact, these functions are inversePlanetmathPlanetmathPlanetmathPlanetmath equivalences (in the sense to be introduced in §2.4 (http://planetmath.org/24homotopiesandequivalences)), and they relate 𝖺𝗉f(p) to 𝖺𝗉𝖽f(p).

Lemma 2.3.8.

For f:AB and p:x=Ay, we have

First proof.

Let D:(x,y:A)(p:x=y)𝒰 be the type family defined by


Thus, we have


But by definition, all three paths appearing in this type are 𝗋𝖾𝖿𝗅f(x), so we have


Thus, path induction gives us an element of (x,y:A)(p:x=y)D(x,y,p), which is what we wanted. ∎

Second proof.

By induction, it suffices to assume y is x and p is 𝗋𝖾𝖿𝗅x. In this case, what we have to prove is 𝗋𝖾𝖿𝗅f(x)=𝗋𝖾𝖿𝗅f(x)\centerdot𝗋𝖾𝖿𝗅f(x), which is true judgmentally. ∎

Because the types of 𝖺𝗉𝖽f and 𝖺𝗉f 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).

Lemma 2.3.9.

Given P:AU with p:x=Ay and q:y=Az while u:P(x), we have

Lemma 2.3.10.

For a function f:AB and a type family P:BU, and any p:x=Ay and u:P(f(x)), we have

Lemma 2.3.11.

For P,Q:AU and a family of functions f:(x:A)P(x)Q(x), and any p:x=Ay and u:P(x), we have

Title 2.3 Type families are fibrations