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.


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )


Connecting to %s