github.com/HoTT/book ↗

About HoTT/book

This is a comprehensive textbook on homotopy type theory, an area of mathematics combining homotopy theory with type theory. The project emerged from the Univalent Foundations of Mathematics program at the Institute for Advanced Study in 2012-2013 and aims to present informal homotopy type theory to students and researchers. The work is written in TeX and available under a Creative Commons Attribution-ShareAlike license, with compiled versions distributed through the official homotopy type theory website and nightly builds on GitHub.

The book is designed for multiple formats and use cases. Readers can compile various PDF versions including formats optimized for online reading with colored text and green hyperlinks, ebook readers with adjusted margins and page widths, printed versions in letter and A4 sizes with and without color covers, an arXiv submission version, and special exercise formats. The project includes exercise solutions and an errata document. Compilation requires a modern LaTeX distribution like Texlive 2012 or later, along with numerous LaTeX packages and the make utility.

While not structured as a community-driven project, the maintainers welcome suggestions and improvements through pull requests and issues on GitHub. The repository emphasizes an inclusive and welcoming environment for readers of all backgrounds and experience levels, with discussions encouraged both on the project's issue tracker and in broader community forums like the HoTT Google group and Zulip chat.