I've done some undergraduate level study of algebraic topology (most Hatcher's book) and the smallest amount of type theory in a foundations of mathematics course.

Homotopy type theory sounds amazing from the blurbs on the official website and wikipedia etc. I would really like to pursue HoTT, even as a self-taught subject, and I would appreciate any thoughts the community had?

I am reading Hatcher's section in his algebraic topology book on homotopy theory but where can I find out more? Is J.P. May's concise course a good source for this?

What is a good type theory reference/introduction?

Anything extra I could to do ease myself into HoTT?

Thank you for any suggestions!

  • 2
    $\begingroup$ A good approximation of what you need to know can usually be discovered by picking a book on HoTT that you want to read and looking at the preface/introduction. $\endgroup$
    – user98602
    Dec 14, 2014 at 4:06
  • 3
    $\begingroup$ I think that starting with the HoTT textbook is a good idea. It is really well-written. You can then gradually pick up prerequisites, as needed for the specific topics you are interested in. $\endgroup$ Dec 14, 2014 at 13:07
  • 2
    $\begingroup$ There are also some other shorter introductions linked from on the homotopy type theory web site, homotopytypetheory.org, including several video lectures and materials from a course given by Bob Harper. $\endgroup$ Dec 19, 2014 at 7:08
  • $\begingroup$ I think that Julian's answer is wrong, because his statement, "if you know Set Theory at a sufficient level, you would have enough knowledge to learn HoTT" is blatantly wrong. This is false. You need to know a lot more; prerequisites are probably in the htpy theory book (or ask @MikeShulman, he knows a lot about HoTT!). $\endgroup$
    – user122283
    Jan 2, 2015 at 20:49

2 Answers 2


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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.