2.3 -- An explanation of "Type families as fibrations" using diagrams (Part 1)

I'm often in need of diagrams for understanding abstract concepts. I perfectly understand why there's not a lot of diagram in HOTT book : it was made in a very short time to explain the theory in the doing.
Here I'll try to re-explain 2.3 using diagrams. I will stay very close to the book material.

 2.3 -- An explanation of "Type families as fibrations" using diagrams (Part 1)

Type families

A type family is the basis of the definition of a dependent pair. It's a function $P : A \rightarrow \mathcal{U}$ for a type $A$ and an universe $\mathcal{U}$. Using this function we can define the type of dependent pair $\sum_{x:A} P(x)$ with the basic construction $(a,b)$ taking an element $a: A$ and an element $b: P(a)$. As $b$ in the pair depends on the first component, it's called a dependent pair.

Here we can display the type family $P$ using this diagram :

where to each element we have associated a whole type.

Elements of type $\sum_{a:A} P(a)$ can be displayed as pairings preserving those yellow arrows :

Fibrations

Before explaining why such a type family is a fibration,  I'll recall what is a fibration through the most trivial example.

Take an onto morphism between vector spaces $f : X \rightarrow Y$, we can define the mapping $g$ over $Y$ by setting $g(y) = f^{(-1)}(x) = \{ x \in X ~|~ f(x) = y \}$. Each $g(y)$ is called the fiber over $y$. All fibers are affine subspace of $Y$ with the same direction $Ker(f)$.

The space $Y$ is called the base space of $f$ because the defining element of each fiber lives there. The space $X$ is called the total space because its the disjoint union of all the fibers.

Now, let's take a path from $y$ to $y'$ in $Y$. I.e. a continuous mapping $p : [0,1] \rightarrow Y$ such that $p(0) = y$ and $p(1) = y'$. Note that this is a trivial case of homotopy between two constants functions.
Taking a starting point $u$ in the fiber over $y$. We can try to lift this path in a path $p_*$ in the total space $X$ by walking through fibers starting in $u$ and by mimicking the path $p$. If such a map is guaranteed to exists we say that $f$ is a fibration.

Here we can explicitly define this map. Take $E$ to be such that $Ker f \oplus E = X$ and $u \in E$. The map $f_{|E}$ is an isomorphism from $E$ to $Y$. We can set $p_* = f_{|E}^{-1} p$. We have $p_*(0) = f_{|E}^{-1}(y) = u$ and $p_*$ is continuous because it's the compound of a linear, hence continuous, map and the continuous map $p$. Note that $p_*(1) = f_{|E|}^{-1}(y')$ and $f(p_*(1)) = y'$ so $p_*(1)$ in the fiber over $y'$.

This situation is depicted here :

(What we have described here is the structure of a trivial vector bundle.)
 

Type family as fibration

Looking back at the type family $P : A \rightarrow \mathcal{U}$ we can see that $P(x)$ looks just like a fiber with base point $x$. So we could think of $A$ as a base space. The total space is the union of all fibers, therefore it would be here $\sum_{x:A} P(x)$. We don't really have a candidate for a fibration but it doesn't prevent us from looking at the fibration defining property in this setting.

One of the most important fact of homotopy theory is that given two elements $x, y : A$, a proof $p : x = y$ of equality between those two elements can be interpreted as a path from $x$ to $y$.

The fibration property would ensure that given $u : P(x)$ we could define a path $p'$ starting at $(x,u)$ in the total space $\sum_{a:A} P(a)$. There's no way of knowing in which fibers would this path walk, but what is certain is that its ending point has to be of the form $(y, v)$ with $v : P(y)$.

If we sum it up, what we want to construct is a function $transport_p : P(x) \rightarrow P(y)$. We can construct it by path induction by assuming that $p \equiv refl_x$ and thus $x \equiv y$. The function we want in this case has to go from $P(x)$ to itself, therefore we can set it to be $id_{P(x)}$ and we are done.

We note $p_*(u) = transport_p(u)$. And it is depicted here : .

To get back the full fibration property we need to show that $p$ itself can be lifted to a path $lift(p,u) : (x,u) =_{\sum_{a:A} P(a)} (y,p_*(u))$. By path induction, we can assume that $p \equiv refl_x$ and that $x \equiv y$. Then we need to build a path $(x,u) = (x,u)$ as $p_* = id$ in this case. We can take $refl_{(x,u)}$ and it concludes the proof.

Here this path is depicted between the boxed elements of $\sum_{x:A} P(x)$ :