Types, Spaces, and Higher Groupoids
Last time we discussed fibrations of sets, spaces, and types. We noted that path induction allows us to prove that the type family of equalities over a given type A is “homotopy equivalent” to A.
This week, we will continue with this and discuss the groupoid structure of spaces (paths) and types (equalities). In doing so, we will establish the “interchange law” for 2-categories, and see that in the particular case of spaces and types that this allows us to prove that the composition law is commutative (up to a higher equivalence) for 2-paths and 2-equivalences that begin and end at the same point.
We shall also discuss how non-dependent functions between types give rise to functors on the associated groupoids of equivalences. This leads to the problem of what to do for dependent functions, and it turns out that fibrations give us a solution to this, and thus we will have come full circle.
Dustin Mulcahey earned his Ph.D. from the CUNY Graduate Center in 2012. He does research in the area of category theory, with a related interest in Haskell, and more recently, has organized the Homotopy Type Theory Reading Group.