This might help you to read the HoTT Book, a reference to keep in your pocket.

All cheatsheets:

• Direct link: hott-all.pdf

Separately:

• Basics (Chapter 2):

  • Direct link: hott-basics.pdf

  

• Sets and logic (Chapter 3):

  • Direct link: hott-logic.pdf

  

• Equivalences (Chapter 4):

  • Direct link: hott-equivalences.pdf

  

• Categories (Chapter 9): (missing some references)

  • Direct link: hott-categories.pdf

  

• Formal type theory (Appendix):

  • Direct link: hott-formal.pdf

  

• A fairly new version of LaTeX. Texlive 2012 is confirmed to work. You might need to install some packages; see hott.sty for packages that are used by the book.

BasicTeX, which is a minimalistic version of MacTeX, is confirmed to work once the following packages have been installed: tlmgr, install, braket, comment, courier, enumitem, helvetic, mathpazo, nextpage, ntheorem, palatino, rsfs, stmaryrd, symbol, titlesec, wallpaper, wasy, wasysym, xstring, zapfding, gitinfo2.

• If you have make utility and latexmk just run make in the root directory of this repository.

This work is licensed under the same license of the HoTT book, i.e.:

• Creative Commons Attribution-ShareAlike 3.0 Unported License.

• HoTT book from the website homotopytypetheory.org.

    @Book{hottbook,
      author =    {The {Univalent Foundations Program}},
      title =     {Homotopy Type Theory: Univalent Foundations of Mathematics},
      publisher = {\url{https://homotopytypetheory.org/book}},
      address =   {Institute for Advanced Study},
      year =      2013}

• The LaTeX sources: HoTT/book