# HoTT book: the LaTeX source behind the free textbook on informal homotopy type theory

> The Homotopy Type Theory book exists as a single Git repository of TeX files with a Makefile, twelve build targets and an errata pipeline. This is how the PDF you have read is produced, and what it costs to build it yourself.

**HoTT/book** — A textbook on informal homotopy type theory

- Repository: https://github.com/HoTT/book
- Stars: 2,172 · Forks: 380
- Language: TeX
- License: not declared
- Published: 2026-10-06 · Updated: 2026-10-06 · Language: en
- Canonical page: https://hysenlabs.com/projects/hott-book

## A book repository, not a software project

There is no package manager here, no test suite in any conventional sense, and no build that produces a library. GitHub reports TeX as the primary language because the entire content is LaTeX. The repository description is nine words long, a textbook on informal homotopy type theory, and the README adds that it belongs to the Univalent Foundations of Mathematics project that ran at the Institute for Advanced Study across 2012 and 2013.

That framing matters for expectations. GitHub records exactly one release, tagged `first-edition`, titled Homotopy Type Theory, Univalent Foundations of Mathematics, First Edition, published on 2023-05-24. A book that has been out for years does not get tagged every time a paragraph is fixed, so the release list tells you almost nothing about current work. The repository itself is the better signal, and it holds 82 open issues against roughly 2,100 stars, which for a text of this size is a healthy amount of reader-reported friction about typographical errors and unclear passages.

The last push was on 2026-06-18. That is recent enough that the tree reflects current thinking, and recent enough that errata are still arriving.

One structural detail is worth noticing because it explains how the book stays consistent across every edition: the top-level file list contains separate chapter sources such as `introduction.tex`, `basics.tex`, `homotopy.tex`, `equivalences.tex`, `induction.tex`, `logic.tex`, `hlevels.tex`, `hits.tex`, `categories.tex`, `formal.tex` and `back.tex`. The names describe a deliberate progression from foundations toward higher categorical structure, and a shared `macros.tex` keeps notation identical everywhere. When a symbol changes, it changes once.

## Twelve make targets, one per print format

The Makefile is the centre of the project, and the target list is long because print and screen demand different things. The online edition is the default choice, with colour and green links so that cross-references are visible on a screen:

```bash
make hott-online.pdf
make hott-ebook.pdf
make hott-arxiv.pdf
```

Three ebook variants exist at different page widths, narrow, default and wide, all built for readers with small margins. Then there is the home-printing pair, one for letter paper and one for A4, each of which also produces a two-page colour cover:

```bash
make hott-letter.pdf cover-letter.pdf
make hott-a4.pdf cover-a4.pdf
```

Two more produce exercise-only volumes in black and white with one exercise per page, which is how the book is used in a classroom where students work through the problems separately. The bound trade edition for the Lulu print run is its own target with its own two covers:

```bash
make hott-a4-exercises.pdf
make hott-ustrade.pdf cover-lulu-hardcover.pdf cover-lulu-paperback.pdf
make exercise_solutions.pdf
make errata.pdf
```

That last one deserves attention. `errata.pdf` is a first-class build target, and the tree contains `errata.tex` alongside shell helpers named `check-errata` and `filter-errata`. For a published book, making the correction list something you can compile and distribute is a more honest arrangement than quietly fixing a PDF nobody can replace.

## Why version.tex has to exist before anything compiles

The one genuinely surprising requirement is that you cannot simply run LaTeX. The book is complex enough that a generated file has to be present first, and the README explains why: `version.tex` is generated on the fly, which is why `make` is listed as a requirement alongside LaTeX itself.

The workaround is documented for people without make, which on a Mac means anyone who skipped the Xcode command line tools. Create `version.tex` by hand and put the following in it, substituting your own name for the placeholder:

```tex
\newcommand{\OPTversion}{Joe-Hacker-version}
```

Then compile with whatever LaTeX workflow you normally use, since the main entry files are all named `hott-XXX.tex`. The README's closing remark on this path is blunt, that you really should have make.

The generated file exists so that a build can record who compiled it and when. For a text maintained by many contributors over several years, stamping every PDF with the build identity is a reasonable practice, and it is also the reason the first `make` invocation takes noticeably longer than later ones.

Once `version.tex` exists, the note at the end of the compilation section applies: you no longer need `make` for every edit, and can run the usual LaTeX cycle from your editor directly.

## TeX prerequisites, including the BasicTeX package list

The README is specific here, which saves a lot of guessing. TeX Live 2012 is confirmed to work, so anything substantially newer is safe. Some packages must be installed, and the README points at `main.tex` for the list, which is worth flagging: that file does not appear in the repository's top-level listing, where the entry points are the `hott-XXX.tex` variants. If you are resolving missing-package errors, expect to read the preamble of whichever file you are compiling.

For macOS users running the minimal BasicTeX distribution, a complete package list is given, and it is long enough to be the difference between a successful build and a slow afternoon of one-error-at-a-time fixes:

```bash
tlmgr install braket comment courier enumitem helvetic
tlmgr install mathpazo nextpage ntheorem palatino rsfs
tlmgr install stmaryrd symbol titlesec wallpaper wasy wasysym xstring zapfding
```

Fonts are part of the story here rather than a detail. Palatino and its math companion, mathpazo, along with the symbol packages and Zapf Dingbats, are what give the book its typography, so skipping them produces a technically valid PDF that looks nothing like the published edition.

The `make` utility is required for the reason given above, and the book is described as a fairly complex piece of LaTeX code, which is a fair warning about first-build time.

## Contributions, the errata pipeline and nightly builds

The README is unusually direct about the shape of contributions. This book is not a community project, but readers are welcome to suggest improvements, and the preferred route is a pull request. An issue is the fallback when there is no concrete proposal yet. Both trackers are reserved for the book itself; anything about homotopy type theory more generally is directed to the Google group or the Zulip instance instead, which keeps the issue tracker from filling up with mathematics discussion.

`CONTRIBUTING.md` holds the longer guidance, and `CONVENTIONS.txt` sits at the top level as the style reference. There is a `.travis.yml`, which dates the continuous integration setup to a period when Travis was the default choice for open source CI, and a `Makefile` that a CI run could target without special casing.

Distribution runs through the homotopytypetheory.org book page for compiled and printed versions, with nightly builds published on the GitHub wiki under Nightly Builds. That separation is deliberate: the stable first edition is the thing you cite, and the nightlies are how you see what changed today. For readers who want to know whether an erratum has been fixed, comparing against the nightly build is the direct answer.

The licence is Creative Commons Attribution-ShareAlike 3.0 Unported, stated in the README rather than in a licence file. That permits redistribution and adaptation including commercial reuse, with two conditions: credit the work, and license derivative work under the same terms.

## Conclusion

This repository is the right place to start if you want the homotopy type theory book as a buildable source rather than a downloaded PDF, and it is the wrong place to look for machine-checked proofs, since the word informal in the title is doing real work and the only formalization directory is a Coq introduction. Before cloning, check that you can install a recent TeX distribution: the README confirms TeX Live 2012 and BasicTeX with a named package list work, and everything else depends on that. The errata target is worth reading even if you never compile anything, because the first edition is officially released and its corrections live in the repository.

## FAQ

### How do I download a free PDF of the HoTT book?

Compiled and printed versions are linked from the book's website at homotopytypetheory.org, and nightly builds are published on the repository wiki under Nightly Builds. If you would rather compile it yourself, the Makefile has a target for the screen edition and another for the print editions.

### What does informal homotopy type theory mean, and is the book formally verified?

The book presents homotopy type theory in prose rather than as a mechanised development, which is why the title says informal. The repository contains one Coq-related directory, `coq_introduction/`, but the chapters themselves are LaTeX files such as `homotopy.tex` and `hlevels.tex` rather than proofs in a proof assistant. It is a textbook, not a library.

### How do I compile the book without make?

Create `version.tex` yourself and define the version command inside it, substituting your name for the placeholder. After that you can compile the `hott-XXX.tex` entry files with your normal LaTeX tools. The README notes that having make is still preferable, since it handles the version stamping automatically.

### What licence applies to the HoTT book?

The README states the work is licensed under Creative Commons Attribution-ShareAlike 3.0 Unported. That allows copying, redistribution and adaptation including commercially, provided you give credit and license any derivative under the same terms. Note that this is stated in the README rather than in a licence file at the repository root.

## Sources

- [HoTT/book on GitHub](https://github.com/HoTT/book)
- [Issues](https://github.com/HoTT/book/issues)
- [README](https://github.com/HoTT/book/blob/master/README.md)
- [Releases](https://github.com/HoTT/book/releases)

---

Hysen Labs editorial analysis, written from the project's own repository and release notes. Cite the canonical page: https://hysenlabs.com/projects/hott-book