Introductory books as preparation to read Voevodsky homotopy-theory (HoTT) book

Question

I would like to read Voevodsky HoTT book.

However, I lack a lot of the basics. I would need a few introductory books first that cover topics like groupoids, fibrations, W -types, Homotopy theory.

Any suggestions for references? (I am looking primary for books)

Please not that the book is written by many authors of equal importance. So more specific: 'The HoTT book written by the participants of the Special Year on Univalent Foundations at Institute for Advanced Study'.

Answer 1

Another way to look at those notions of groupoids and fibrations is that type theory tells you what they are. It does so by telling you what you can do with them.

For example with fibrations, you can transport points in the fibers along paths -- this is exactly the intention of the classical notion of fibrations. It is even more true for weak $\infty$-groupoids.

So instead of reading lots of 'background' material which explains you the classical versions of the terms that are used in the HoTT book, you maiy find it easier and quicker to learn what they are through the explanations that the book provides.

If you don't feel comfortable with the idea of learning what things are by learning what you can do with them, I'd suggest with starting to read about homotopy theory itself. Hatcher's Algebraic Topology is probably a reasonable starting point (which is freely available online).

Answer 2

You can take a look at Robert Harper's lectures: http://www.cs.cmu.edu/~rwh/courses/hott/ (There are lecture notes and video recordings) They require much less than you described to understand and covert HoTT.

Answer 3

I would really recommend Awodey's Category Theory, as his treatment is especially well-suited to understanding the connection between Martin-Lof type theory and locally Cartesian closed categories. Personally, I would be lost trying to understand the HoTT book (for which Voevodsky can be given nowhere near sole credit) without Awodey's coverage of typed lambda calculus.

As for the groupoid structure issue, you could either browse around nLab a bit to get the idea (specifically the authors seem to be construing HoTT types as Kan complexes/$\infty$-groupoids), or you could read the first couple chapters of Jacob Lurie's "Higher Topos Theory", which you can find on his web site. You don't need to know many deep things about homotopy or Kan complexes to read the HoTT book, but understanding the idea of a Kan complex makes the idea behind the identity types a lot more transparent.