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 $f:{\prod }_{(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\mathrm{:}x{\mathrm{=}}_{A}y$. Then there is a function $p_{\mathrm{*}}\mathrm{:}P\mathit{}\mathrm{(}x\mathrm{)}\mathrm{\to }P\mathit{}\mathrm{(}y\mathrm{)}$.

First proof.

Let $D:{\prod }_{(x,y:A)}{\prod }_{(p:x=y)}𝒰$ be the type family defined by

$$D(x,y,p):\equiv P(x)\to P(y).$$

Then we have the function

$$d:\equiv \lambda x.{\mathrm{𝗂𝖽}}_{P(x)}:\prod _{x:A}D(x,x,{\mathrm{𝗋𝖾𝖿𝗅}}_x),$$

so that the induction principle gives us ${\mathrm{𝗂𝗇𝖽}}_{{=}_A}(D,d,x,y,p):P(x)\to P(y)$ for $p:x=y$, which we define to be $p_{*}$. ∎

Second proof.

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

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

$${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^P(p,\text{–}):P(x)\to P(y).$$

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 equivalent.

Topologically, the transportation lemma can be viewed as a “path lifting” operation in a fibration. We think of a type family $P:A\to 𝒰$ as a fibration with base space $A$, with $P(x)$ being the fiber over $x$, and with ${\sum }_{(x:A)}P(x)$ being the total space of the fibration, with first projection ${\sum }_{(x:A)}P(x)\to 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_{*}\left(u\right)$ 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\mathrm{:}A\mathrm{\to }\mathrm{U}$ be a type family over $A$ and assume we have $u\mathrm{:}P\mathit{}\mathrm{(}x\mathrm{)}$ for some $x\mathrm{:}A$. Then for any $p\mathrm{:}x\mathrm{=}y$, we have

$$\mathrm{𝗅𝗂𝖿𝗍}(u,p):(x,u)=(y,p_{*}\left(u\right))$$

in ${\mathrm{\sum }}_{\mathrm{(}x\mathrm{:}A\mathrm{)}}P\mathit{}\mathrm{(}x\mathrm{)}$.

Proof.

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.

Remark 2.3.3.

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

We may also occasionally use other topological terminology when speaking about type families. For instance, we may refer to a dependent function $f\mathrm{:}{\mathrm{\prod }}_{\mathrm{(}x\mathrm{:}A\mathrm{)}}P\mathit{}\mathrm{(}x\mathrm{)}$ as a section of the fibration $P$, and we may say that something happens fiberwise if it happens for each $P\mathit{}\mathrm{(}x\mathrm{)}$. For instance, a section $f\mathrm{:}{\mathrm{\prod }}_{\mathrm{(}x\mathrm{:}A\mathrm{)}}P\mathit{}\mathrm{(}x\mathrm{)}$ 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:{\prod }_{(x:A)}P(x)$ and a path $p:x{=}_{A}y$, 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.

HoTT_fig_2.3.1.png

We can obtain such a thing from Lemma 2.2.1 (http://planetmath.org/22functionsarefunctors#Thmprelem1). Given $f:{\prod }_{(x:A)}P(x)$, we can define a non-dependent function $f^{\prime }:A\to {\sum }_{(x:A)}P(x)$ by setting $f^{\prime }(x):\equiv (x,f(x))$, and then consider $f^{\prime }\left(p\right):f^{\prime }(x)=f^{\prime }(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_{*}\left(u\right):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_{*}\left(u\right)$ 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_{*}\left(u\right)=v$ in $P(y)$. And, indeed, we can show that dependent functions produce such paths.

Lemma 2.3.4 (Dependent map).

Suppose $f\mathrm{:}{\mathrm{\prod }}_{\mathrm{(}x\mathrm{:}A\mathrm{)}}P\mathit{}\mathrm{(}x\mathrm{)}$; then we have a map

$${\mathrm{𝖺𝗉𝖽}}_f:\prod _{p:x=y}\left(p_{*}\left(f(x)\right){=}_{P(y)}f(y)\right).$$

First proof.

Let $D:{\prod }_{(x,y:A)}{\prod }_{(p:x=y)}𝒰$ be the type family defined by

$$D(x,y,p):\equiv p_{*}\left(f(x)\right)=f(y).$$

Then $D(x,x,{\mathrm{𝗋𝖾𝖿𝗅}}_x)$ is ${({\mathrm{𝗋𝖾𝖿𝗅}}_x)}_{*}\left(f(x)\right)=f(x)$. But since ${({\mathrm{𝗋𝖾𝖿𝗅}}_x)}_{*}\left(f(x)\right)\equiv f(x)$, we get that $D(x,x,{\mathrm{𝗋𝖾𝖿𝗅}}_x)\equiv (f(x)=f(x))$. Thus, we find the function

$$d:\equiv \lambda x.{\mathrm{𝗋𝖾𝖿𝗅}}_{f(x)}:\prod _{x:A}D(x,x,{\mathrm{𝗋𝖾𝖿𝗅}}_x)$$

and now path induction gives us ${\mathrm{𝖺𝗉𝖽}}_f(p):p_{*}\left(f(x)\right)=f(y)$ for each $p:x=y$. ∎

Second proof.

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

Lemma 2.3.5.

If $P\mathrm{:}A\mathrm{\to }\mathrm{U}$ is defined by $P\mathrm{(}x\mathrm{)}\mathrm{:}\mathrm{\equiv }B$ for a fixed $B\mathrm{:}\mathrm{U}$, then for any $x\mathrm{,}y\mathrm{:}A$ and $p\mathrm{:}x\mathrm{=}y$ and $b\mathrm{:}B$ we have a path

$${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍𝖼𝗈𝗇𝗌𝗍}}_p^B(b):{\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^P(p,b)=b.$$

First proof.

Fix a $b:B$, and let $D:{\prod }_{(x,y:A)}{\prod }_{(p:x=y)}𝒰$ be the type family defined by

$$D(x,y,p):\equiv ({\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^P(p,b)=b).$$

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

$$d:\equiv \lambda x.{\mathrm{𝗋𝖾𝖿𝗅}}_b:\prod _{x:A}D(x,x,{\mathrm{𝗋𝖾𝖿𝗅}}_x).$$

Now path induction gives us an element of ${\prod }_{(x,y:A)}{\prod }_{(p:x=y)}({\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^P(p,b)=b),$ as desired. ∎

Second proof.

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

Thus, by concatenating with ${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍𝖼𝗈𝗇𝗌𝗍}}_p^B(b)$, for any $x,y:A$ and $p:x=y$ and $f:A\to B$ we obtain functions

$\left(f(x)=f(y)\right)$ $\to (p_{*}\left(f(x)\right)=f(y))\mathit{\hspace{1em}\hspace{1em}}\text{and}$ (2.3.6)

$(p_{*}\left(f(x)\right)=f(y))$ $\to (f(x)=f(y)).$ (2.3.7)

In fact, these functions are inverse equivalences (in the sense to be introduced in §2.4 (http://planetmath.org/24homotopiesandequivalences)), and they relate ${\mathrm{𝖺𝗉}}_f(p)$ to ${\mathrm{𝖺𝗉𝖽}}_f(p)$.

Lemma 2.3.8.

For $f\mathrm{:}A\mathrm{\to }B$ and $p\mathrm{:}x{\mathrm{=}}_{A}y$, we have

$${\mathrm{𝖺𝗉𝖽}}_f(p)={\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍𝖼𝗈𝗇𝗌𝗍}}_p^B(f(x)){\mathrm{𝖺𝗉}}_f(p).$$

First proof.

Let $D:{\prod }_{(x,y:A)}{\prod }_{(p:x=y)}𝒰$ be the type family defined by

$$D(x,y,p):\equiv ({\mathrm{𝖺𝗉𝖽}}_f(p)={\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍𝖼𝗈𝗇𝗌𝗍}}_p^B(f(x)){\mathrm{𝖺𝗉}}_f(p)).$$

Thus, we have

$$D(x,x,{\mathrm{𝗋𝖾𝖿𝗅}}_x)\equiv ({\mathrm{𝖺𝗉𝖽}}_f({\mathrm{𝗋𝖾𝖿𝗅}}_x)={\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍𝖼𝗈𝗇𝗌𝗍}}_{{\mathrm{𝗋𝖾𝖿𝗅}}_x}^B(f(x)){\mathrm{𝖺𝗉}}_f({\mathrm{𝗋𝖾𝖿𝗅}}_x)).$$

But by definition, all three paths appearing in this type are ${\mathrm{𝗋𝖾𝖿𝗅}}_{f(x)}$, so we have

$${\mathrm{𝗋𝖾𝖿𝗅}}_{{\mathrm{𝗋𝖾𝖿𝗅}}_{f(x)}}:D(x,x,{\mathrm{𝗋𝖾𝖿𝗅}}_x).$$

Thus, path induction gives us an element of ${\prod }_{(x,y:A)}{\prod }_{(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 ${\mathrm{𝗋𝖾𝖿𝗅}}_x$. In this case, what we have to prove is ${\mathrm{𝗋𝖾𝖿𝗅}}_{f(x)}={\mathrm{𝗋𝖾𝖿𝗅}}_{f(x)}{\mathrm{𝗋𝖾𝖿𝗅}}_{f(x)}$, which is true judgmentally. ∎

Because the types of ${\mathrm{𝖺𝗉𝖽}}_f$ and ${\mathrm{𝖺𝗉}}_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\mathrm{:}A\mathrm{\to }\mathrm{U}$ with $p\mathrm{:}x{\mathrm{=}}_{A}y$ and $q\mathrm{:}y{\mathrm{=}}_{A}z$ while $u\mathrm{:}P\mathit{}\mathrm{(}x\mathrm{)}$, we have

$$q_{*}\left(p_{*}\left(u\right)\right)={(pq)}_{*}\left(u\right).$$

Lemma 2.3.10.

For a function $f\mathrm{:}A\mathrm{\to }B$ and a type family $P\mathrm{:}B\mathrm{\to }\mathrm{U}$, and any $p\mathrm{:}x{\mathrm{=}}_{A}y$ and $u\mathrm{:}P\mathit{}\mathrm{(}f\mathit{}\mathrm{(}x\mathrm{)}\mathrm{)}$, we have

$${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{P\circ f}(p,u)={\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^P({\mathrm{𝖺𝗉}}_f(p),u).$$

Lemma 2.3.11.

For $P\mathrm{,}Q\mathrm{:}A\mathrm{\to }\mathrm{U}$ and a family of functions $f\mathrm{:}{\mathrm{\prod }}_{\mathrm{(}x\mathrm{:}A\mathrm{)}}P\mathit{}\mathrm{(}x\mathrm{)}\mathrm{\to }Q\mathit{}\mathrm{(}x\mathrm{)}$, and any $p\mathrm{:}x{\mathrm{=}}_{A}y$ and $u\mathrm{:}P\mathit{}\mathrm{(}x\mathrm{)}$, we have

$${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^Q(p,f_x(u))=f_y({\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^P(p,u)).$$

Title	2.3 Type families are fibrations