You didn't exactly ask "what background do I need to learn HoTT", but since that's the question some other people are answering, I'll address that too. The subject as a whole is quite wide, and if to understand it all and its applications deeply would require significant background in homotopy theory, higher category theory, topos theory, and type theory. However, none of that is necessarily required at the beginning, and indeed learning HoTT may help you get a handle on those other subjects at the same time or later on.

The book Homotopy type theory was written with the intent of assuming as few prerequisites as possible, not even basic algebraic topology or type theory, although it does assume some mathematical maturity and perhaps more category theory than would be ideal. If you don't have any exposure to category theory, I would recommend doing a bit of reading there; some good introductory books are Awodey's Category theory and Leinster's Basic category theory. But other than that, I would suggest diving into the HoTT Book and see how you find it. The first chapter of the HoTT Book is an introduction to type theory, intended to stand on its own; it's necessarily brief and only covers the basics necessary for the rest of the book, so you may want to supplement it with other readings, but unfortunately really good introductions to type theory are hard to find.

The HoTT Book is only about one particular facet of the subject, namely developing mathematics internally to HoTT. If you want to learn about semantics, for instance, you'll have to go elsewhere, and eventually need more background in abstract homotopy theory and higher category theory. May's book is not an unreasonable place to go after Hatcher; particularly because May uses the modern language of category theory (which Hatcher seems unaccountably allergic to), which is also at the basis of HoTT. Beware that Concise lives up to its name and requires a lot of the reader. The sequel More concise algebraic topology is mostly not hugely relevant for HoTT, but it does contain a good introduction to model categories, which you'll have to learn about eventually if you want to understand the semantics of HoTT.

Finally, as I mentioned in the comments, I also suggest availing yourself of the other resources linked at the homotopytypetheory.org web site, which include several video lectures and basic introductions written for people with differing backgrounds.


I've been watching Robert Harper's lectures on homotopy type theory and am finding them quite understandable. I have a bit of background in type theory and category theory, and that helps a bit, but I don't think it's necessary.