# 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:\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:% A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{% \prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x% :A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\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:x=_{A}y$. Then there is a function ${p}_{*}:P(x)\to P(y)$.

###### First proof.

Let $D:\mathchoice{\prod_{(x,y:A)}\,}{\mathchoice{{\textstyle\prod_{(x,y:A)}}}{% \prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{\mathchoice{{\textstyle% \prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{% \mathchoice{{\textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{% \prod_{(x,y:A)}}}\mathchoice{\prod_{(p:x=y)}\,}{\mathchoice{{\textstyle\prod_{% (p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}}{\mathchoice{{% \textstyle\prod_{(p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}% }{\mathchoice{{\textstyle\prod_{(p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{% \prod_{(p:x=y)}}}\mathcal{U}$ 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.\,\mathsf{id}_{P(x)}:\mathchoice{\prod_{x:A}\,}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(% x:A)}}{\prod_{(x:A)}}}D(x,x,\mathsf{refl}_{x}),$

so that the induction principle gives us $\mathsf{ind}_{=_{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 $\mathsf{refl}_{x}$. But in this case, we can take ${(\mathsf{refl}_{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

 $\mathsf{transport}^{P}(p,\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}):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\mathcal{U}$ as a fibration with base space $A$, with $P(x)$ being the fiber over $x$, and with $\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{% \sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)% }}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x% :A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}P(x)$ being the total space of the fibration, with first projection $\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{% \sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)% }}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x% :A)}}{\sum_{(x:A)}}{\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}_{*}\mathopen{}\left({u}\right)\mathclose{}$ 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:A\to\mathcal{U}$ 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

 $\mathsf{lift}(u,p):(x,u)=(y,{p}_{*}\mathopen{}\left({u}\right)\mathclose{})$

in $\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{% \sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)% }}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x% :A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}P(x)$.

###### 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:A\to\mathcal{U}$ as like a fibration, it is generally not a good idea to say things like “the fibration $P:A\to\mathcal{U}$”, since this sounds like we are talking about a fibration with base $\mathcal{U}$ and total space $A$. To repeat, when a type family $P:A\to\mathcal{U}$ is regarded as a fibration, the base is $A$ and the total space is $\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{% \sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)% }}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x% :A)}}{\sum_{(x:A)}}{\sum_{(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:\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:% A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{% \prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x% :A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}P(x)$ as a of the fibration $P$, and we may say that something happens fiberwise if it happens for each $P(x)$. For instance, a section $f:\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:% A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{% \prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x% :A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(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:\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:% A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{% \prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x% :A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\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.

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

###### Lemma 2.3.4 (Dependent map).

Suppose $f:\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:% A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{% \prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x% :A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}P(x)$; then we have a map

 $\mathsf{apd}_{f}:\mathchoice{\prod_{p:x=y}\,}{\mathchoice{{\textstyle\prod_{(p% :x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}}{\mathchoice{{% \textstyle\prod_{(p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}% }{\mathchoice{{\textstyle\prod_{(p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{% \prod_{(p:x=y)}}}\big{(}{p}_{*}\mathopen{}\left({f(x)}\right)\mathclose{}=_{P(% y)}f(y)\big{)}.$
###### First proof.

Let $D:\mathchoice{\prod_{(x,y:A)}\,}{\mathchoice{{\textstyle\prod_{(x,y:A)}}}{% \prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{\mathchoice{{\textstyle% \prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{% \mathchoice{{\textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{% \prod_{(x,y:A)}}}\mathchoice{\prod_{(p:x=y)}\,}{\mathchoice{{\textstyle\prod_{% (p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}}{\mathchoice{{% \textstyle\prod_{(p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}% }{\mathchoice{{\textstyle\prod_{(p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{% \prod_{(p:x=y)}}}\mathcal{U}$ be the type family defined by

 $D(x,y,p):\!\!\equiv{p}_{*}\mathopen{}\left({f(x)}\right)\mathclose{}=f(y).$

Then $D(x,x,\mathsf{refl}_{x})$ is ${(\mathsf{refl}_{x})}_{*}\mathopen{}\left({f(x)}\right)\mathclose{}=f(x)$. But since ${(\mathsf{refl}_{x})}_{*}\mathopen{}\left({f(x)}\right)\mathclose{}\equiv f(x)$, we get that $D(x,x,\mathsf{refl}_{x})\equiv(f(x)=f(x))$. Thus, we find the function

 $d:\!\!\equiv{\lambda}x.\,\mathsf{refl}_{f(x)}:\mathchoice{\prod_{x:A}\,}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(% x:A)}}{\prod_{(x:A)}}}D(x,x,\mathsf{refl}_{x})$

and now path induction gives us $\mathsf{apd}_{f}(p):{p}_{*}\mathopen{}\left({f(x)}\right)\mathclose{}=f(y)$ for each $p:x=y$. ∎

###### Second proof.

By induction, it suffices to assume $p$ is $\mathsf{refl}_{x}$. But in this case, the desired equation is ${(\mathsf{refl}_{x})}_{*}\mathopen{}\left({f(x)}\right)\mathclose{}\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:\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:% A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{% \prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x% :A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}P(x)$ when $P$ is a constant type family, $P(x):\!\!\equiv B$. In this case, $\mathsf{apd}_{f}$ and $\mathsf{ap}_{f}$ are closely related, because of the following lemma:

###### Lemma 2.3.5.

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

 $\mathsf{transportconst}^{B}_{p}(b):\mathsf{transport}^{P}(p,b)=b.$
###### First proof.

Fix a $b:B$, and let $D:\mathchoice{\prod_{(x,y:A)}\,}{\mathchoice{{\textstyle\prod_{(x,y:A)}}}{% \prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{\mathchoice{{\textstyle% \prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{% \mathchoice{{\textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{% \prod_{(x,y:A)}}}\mathchoice{\prod_{(p:x=y)}\,}{\mathchoice{{\textstyle\prod_{% (p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}}{\mathchoice{{% \textstyle\prod_{(p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}% }{\mathchoice{{\textstyle\prod_{(p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{% \prod_{(p:x=y)}}}\mathcal{U}$ be the type family defined by

 $D(x,y,p):\!\!\equiv(\mathsf{transport}^{P}(p,b)=b).$

Then $D(x,x,\mathsf{refl}_{x})$ is $(\mathsf{transport}^{P}(\mathsf{refl}_{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.\,\mathsf{refl}_{b}:\mathchoice{\prod_{x:A}\,}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(% x:A)}}{\prod_{(x:A)}}}D(x,x,\mathsf{refl}_{x}).$

Now path induction gives us an element of $\mathchoice{\prod_{(x,y:A)}\,}{\mathchoice{{\textstyle\prod_{(x,y:A)}}}{\prod_% {(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{\mathchoice{{\textstyle\prod_{(x% ,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{\mathchoice{{% \textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}% }\mathchoice{\prod_{(p:x=y)}\,}{\mathchoice{{\textstyle\prod_{(p:x=y)}}}{\prod% _{(p:x=y)}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}}{\mathchoice{{\textstyle\prod_{(% p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}}{\mathchoice{{% \textstyle\prod_{(p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}% }(\mathsf{transport}^{P}(p,b)=b),$ as desired. ∎

###### Second proof.

By induction, it suffices to assume $y$ is $x$ and $p$ is $\mathsf{refl}_{x}$. But $\mathsf{transport}^{P}(\mathsf{refl}_{x},b)\equiv b$, so in this case what we have to prove is $b=b$, and we have $\mathsf{refl}_{b}$ for this. ∎

Thus, by concatenating with $\mathsf{transportconst}^{B}_{p}(b)$, for any $x,y:A$ and $p:x=y$ and $f:A\to B$ we obtain functions

 $\displaystyle\big{(}f(x)=f(y)\big{)}$ $\displaystyle\to\big{(}{p}_{*}\mathopen{}\left({f(x)}\right)\mathclose{}=f(y)% \big{)}\qquad\text{and}$ (2.3.6) $\displaystyle\big{(}{p}_{*}\mathopen{}\left({f(x)}\right)\mathclose{}=f(y)\big% {)}$ $\displaystyle\to\big{(}f(x)=f(y)\big{)}.$ (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 $\mathsf{ap}_{f}(p)$ to $\mathsf{apd}_{f}(p)$.

###### Lemma 2.3.8.

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

 $\mathsf{apd}_{f}(p)=\mathsf{transportconst}^{B}_{p}(f(x))\mathchoice{\mathbin{% \raisebox{2.15pt}{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{% \centerdot}}}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{% \mathbin{\raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,}}}\mathsf{ap}_{f% }(p).$
###### First proof.

Let $D:\mathchoice{\prod_{(x,y:A)}\,}{\mathchoice{{\textstyle\prod_{(x,y:A)}}}{% \prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{\mathchoice{{\textstyle% \prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{% \mathchoice{{\textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{% \prod_{(x,y:A)}}}\mathchoice{\prod_{(p:x=y)}\,}{\mathchoice{{\textstyle\prod_{% (p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}}{\mathchoice{{% \textstyle\prod_{(p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}% }{\mathchoice{{\textstyle\prod_{(p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{% \prod_{(p:x=y)}}}\mathcal{U}$ be the type family defined by

 $D(x,y,p):\!\!\equiv\big{(}\mathsf{apd}_{f}(p)=\mathsf{transportconst}^{B}_{p}(% f(x))\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{% \mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{% \scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle% \,\centerdot\,}}}\mathsf{ap}_{f}(p)\big{)}.$

Thus, we have

 $D(x,x,\mathsf{refl}_{x})\equiv\big{(}\mathsf{apd}_{f}(\mathsf{refl}_{x})=% \mathsf{transportconst}^{B}_{\mathsf{refl}_{x}}(f(x))\mathchoice{\mathbin{% \raisebox{2.15pt}{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{% \centerdot}}}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{% \mathbin{\raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,}}}\mathsf{ap}_{f% }({\mathsf{refl}_{x}})\big{)}.$

But by definition, all three paths appearing in this type are $\mathsf{refl}_{f(x)}$, so we have

 $\mathsf{refl}_{\mathsf{refl}_{f(x)}}:D(x,x,\mathsf{refl}_{x}).$

Thus, path induction gives us an element of $\mathchoice{\prod_{(x,y:A)}\,}{\mathchoice{{\textstyle\prod_{(x,y:A)}}}{\prod_% {(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{\mathchoice{{\textstyle\prod_{(x% ,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}}{\mathchoice{{% \textstyle\prod_{(x,y:A)}}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}{\prod_{(x,y:A)}}% }\mathchoice{\prod_{(p:x=y)}\,}{\mathchoice{{\textstyle\prod_{(p:x=y)}}}{\prod% _{(p:x=y)}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}}{\mathchoice{{\textstyle\prod_{(% p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}}{\mathchoice{{% \textstyle\prod_{(p:x=y)}}}{\prod_{(p:x=y)}}{\prod_{(p:x=y)}}{\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 $\mathsf{refl}_{x}$. In this case, what we have to prove is $\mathsf{refl}_{f(x)}=\mathsf{refl}_{f(x)}\mathchoice{\mathbin{\raisebox{2.15pt% }{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}\mathsf{refl}_{f(x)}$, which is true judgmentally. ∎

Because the types of $\mathsf{apd}_{f}$ and $\mathsf{ap}_{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:A\to\mathcal{U}$ with $p:x=_{A}y$ and $q:y=_{A}z$ while $u:P(x)$, we have

 ${q}_{*}\mathopen{}\left({{p}_{*}\mathopen{}\left({u}\right)\mathclose{}}\right% )\mathclose{}={(p\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle% \centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1% .075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{% \scriptscriptstyle\,\centerdot\,}}}q)}_{*}\mathopen{}\left({u}\right)% \mathclose{}.$
###### Lemma 2.3.10.

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

 $\mathsf{transport}^{P\circ f}(p,u)=\mathsf{transport}^{P}(\mathsf{ap}_{f}(p),u).$
###### Lemma 2.3.11.

For $P,Q:A\to\mathcal{U}$ and a family of functions $f:\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:% A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{% \prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x% :A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}P(x)\to Q(x)$, and any $p:x=_{A}y$ and $u:P(x)$, we have

 $\mathsf{transport}^{Q}(p,f_{x}(u))=f_{y}(\mathsf{transport}^{P}(p,u)).$
Title 2.3 Type families are fibrations
\metatable