Each chapter is indexed by its homotopy level. The first letters of the seventeen main chapters spell THE PATH IS THE PROOF — the book's hidden acrostic, a homage to Gödel, Escher, Bach.
| h-level | · | Title | In this chapter |
|---|---|---|---|
| −2 | · | The Unique Point (Prelude) | Contractibility: there is exactly one point, and every inhabitant is a path to it. The book's starting note, before the acrostic begins. |
| −1 | T | The Foundations in Crisis | Mere propositions: a type is either empty or a single point. The Tortoise and Achilles dig through the ruins of classical logic. |
| 0 | H | Habitat of Types | Sets in HoTT: types with no higher homotopy. A flat census of distinct concepts, no loops, no higher structure. |
| 1 | E | Equal by Construction: The Curry–Howard Correspondence | Groupoids: proofs as programs, propositions as types. The chapter is itself a loop — its final paragraph returns to its opening sentence. |
| 2 | P | Paths of Dependence | Dependent types: Π-types and Σ-types. Two staircases sharing a glass bridge — the chapter's structure is a 2-groupoid. |
| 3 | A | All Proofs Are Paths | The identity type. Every equality proof is a path in a space; two proofs of the same equality may themselves differ by a 2-path. |
| 4 | T | The Topology of Continuity | Fibrations, transport, and the dependent elimination rule J. How a path in the base lifts to the total space. |
| 5 | H | Homotopy and the Fundamental Group | The circle S¹ as a Higher Inductive Type. Winding numbers, covering spaces, van Kampen's theorem — all from type theory. |
| 6 | I | Infinite Tower: ∞-Groupoids | Paths between paths between paths. The lighthouse staircase winds upward past what the eye can follow. The first signal that the tower does not end. |
| 7 | S | Spaces and Types, Unified | The homotopy hypothesis: (∞,1)-categories and HoTT are the same thing, seen from different directions. A puddle that perfectly reflects the sky. |
| 8 | T | The Hierarchy of Homotopy Levels | The revelation. This chapter names and explains the h-level indexing system — after you have been using it for nine chapters. The hand holds the globe that reflects the hand. |
| 9 | H | Homotopy Equivalence | Equivalence of types: when two types have the same homotopy type. The mirror that creates two equal-but-distinct images. |
| 10 | E | Equality by Equivalence: The Univalence Axiom | Voevodsky's insight: equivalent types are equal. Univalence is the theorem that makes the strange loop close. |
| 11 | P | Power of Univalence | Function extensionality, structure identity principle, and the consequences of being able to transport theorems along equivalences. |
| 12 | R | Ruled by Their Paths: Higher Inductive Types | HITs: types defined not only by their points but by their paths. The circle, the interval, the suspension — topology synthesised from constructors. |
| 13 | O | Orbiting the Circle | π₁(S¹) = ℤ, proved entirely within HoTT. Winding numbers as elements of the fundamental group; the full calculation from first principles. |
| 14 | O | Order from Truncation | Propositional truncation and the h-level hierarchy as a deliberate tool. How to extract classical logic from constructive type theory. |
| 15 | F | Foundations, Constructive | HoTT as a foundation for mathematics: what it can replace, what it illuminates, and where it departs from both set theory and classical logic. |
| ∞ | · | The Type of All Types (Finale) | Universe polymorphism, the type of all types, and the stratified hierarchy that prevents paradox. The dragon bites its own tail — carefully. |
In Homotopy Type Theory, every type has a homotopy level — a measure of how much higher-dimensional structure it contains. A type at h-level −2 is contractible: all its points are connected by a unique path, and all paths are connected by a unique 2-path, and so on forever. A type at h-level −1 is a mere proposition: any two proofs are equal. A type at h-level 0 is a set: any two elements have at most one path between them.
As the level increases, the type is allowed richer and richer path structure. The natural numbers ℕ are a set (h-level 0). The circle S¹ lives at h-level 1. The type of all sets lives at h-level 1. The type of all 1-types lives at h-level 2. And so on, without bound.
Each chapter of this book is indexed by its h-level. The chapter's internal structure — the number of self-referential layers, the shape of its argument, the number of dialogue rounds — mirrors its index. Form enacts content.