Path Induction and the Path-Loop Space Fibration
As we continue our foray into the book, we begin to view types as spaces (or, “equivalently”, as omega groupoids). My goal for this section is to focus on the path induction rule and argue that it corresponds to the path-loop fibration.
More specifically, we can make an analogy between the path space over a space X and the type of all equivalences over a type A. The path space of X is homotopy equivalent to X, and I argue that path induction says “essentially the same thing” about the type of all equivalences over A. I aim to make this analogy as formal as possible, and then delve further into the material in chapter 2.
I would also like to go over some exercises. I’ve done a few, but if anyone wants to come up to the board and show off, then they are welcome!
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.