Let’s say we have a function , and also , from which we can form the type . 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 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 for a type family . The problem is that even if , the types and can still be different. Luckily, the path can give us a function . This is called the transport of the path . If we need to specify explicitly, we may also write this as .
Notice that we can also look at . Thinking about types as propositions, it would make sense to say that together, these show that is equivalent to . 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.
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 and , but its global structure is different. The circles are the “fibers” and the sphere is the “bundle” of the fiber bundle. The map is the fibration. Ah! So when we say that the type family is a fibration with base space , we mean that we can think of as the fibers, with the total space . The fibration itself is then . So for the Hopf fibration, would be the sphere, and would be the map taking each point of the sphere to a circle. The collection of all these circles is , 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 in the base space , and a point in the fiber above the starting point , i.e. , then we can lift to a path in the total space starting at . 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 is called the section of the fibration . 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 is a section of . Ideally, we want this to lift a path 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 which connects the end of the transported path to the correct point. The function that specifies this path in from our function is called . While this function has a different type from ap, it satisfies the expected consistency relations with it.