# What do functions do to paths?

Let’s say we have a function $f : A \rightarrow B$, and also $x, y : A$, from which we can form the type $x=_Ay$. If we have a witness of this equality, i.e. a path, what should our function do to it? Intuitively, we would like to be able to say that we can create a witness for $f(x) =_B f(y)$ i.e. applying the same function to both sides of an equality should take you to another equality. Or in other words, functions should be truth-preserving. Another way of thinking about it is that functions should be continuous: they preserve paths. Using path induction, we can show that this is indeed the case.

Slightly more complicated is the case where we have a dependent function $f : \prod_{x : A}B(x)$ for a type family $B : A \rightarrow \mathcal U$. The problem is that even if $p : x=_A y$, the types $B(x)$ and $B(y)$ can still be different. Luckily, the path $p : x=_Ay$ can give us a function $p_*: B(x) \rightarrow B(y)$. This is called the transport of the path $p$. If we need to specify $B$ explicitly, we may also write this as $\mathsf{transport}^B(p, -) : B(x) \rightarrow B(y)$.

Notice that we can also look at $p_*^{-1} : B(y) \rightarrow B(x)$. Thinking about types as propositions, it would make sense to say that together, these show that $B(x)$ is equivalent to $B(y)$. This ends up being right in this case! But we need to also specify what properties the paths should have in an equivalence, which will require the notion of a homotopy, which will come later!

So from a topological point of view, what is going on here? Something to do with fibrations, which are apparently a generalization of a fiber bundle. According to Hatcher, it’s a map which has the homotopy lifting property with respect to all spaces. I assume that Lemma 2.3.2 is essentially this property. I really want to wrap my head around this, some I’m going to dive into a specific example: the Hopf fibration.

oooh pretty..

The idea is that we can describe a 3-sphere in terms of circles and a sphere. Every point on the sphere corresponds to a circle. The video gives a good sense of what this correspondence is like, but how does this match with a 3-sphere? Well each of these circles is a circle on the 3-sphere. Locally, it just looks like the product space of $S_1$ and $S_2$, but its global structure is different. The circles are the “fibers” and the sphere is the “bundle” of the fiber bundle. The map $p : S_3 \rightarrow S_2$ is the fibration. Ah! So when we say that the type family $P : A \rightarrow \mathcal U$ is a fibration  with base space $A$, we mean that we can think of $P(x)$ as the fibers, with the total space $\sum_{x:A}P(x)$. The fibration itself is then $\mathsf{pr_1} : \sum_{x:A}P(x) \rightarrow A$. So for the Hopf fibration, $A$ would be the sphere, and $P : A \rightarrow \mathcal U$ would be the map taking each point of the sphere to a circle. The collection of all these circles is $\sum_{x:A}P(x)$, which we can map back down to the sphere with the first projection map. It’s starting to make sense!

To really be a fibration, we need it to have the Path Lifting property. If we have a path $p: x=y$ in the base space $A$, and a point in the fiber above the starting point $x$, i.e. $u : P(x)$, then we can lift $p$ to a path in the total space starting at $u$. It’s probably good to note that this is a constructive proof in HoTT.

Another term that I needed to look up was section. A dependent function $f : \prod_{x:A}P(x)$ is called the section of the fibration $P$. Basically, it’s just giving you a map from the base space to the total space – so a section will give you a collection of particular points from each fiber. Like a cross-section!

Anyway, we still need to show how to apply a dependent function. Our function $f:\prod_{x:A}P(X)$ is a section of $P$. Ideally, we want this to lift a path $p: x=y$ up to a path in the total space. To make sure that this happens, we will use the transport function to lift the path up, and then specify a path in $P(y)$ which connects the end of the transported path to the correct point. The function that specifies this path in $P(y)$ from our function $f$ is called $\mathsf{apd}_f : \prod_{p: x=y}\left(p_*(f(x)) =_{P(y)} f(y)\right)$. While this function has a different type from ap, it satisfies the expected consistency relations with it.