Book cover — Escher-inspired spiral staircase ascending into an infinite mathematical tower

Brouwer, Martin-Löf, Voevodsky

Adventures in the Univalent Universe
Types, Paths, and the Self-Referential Nature of Mathematical Identity

"If Gödel, Escher, Bach made you fall in love with mathematics,
this book will take you deeper."

Download free PDF Buy the eBook Buy the hardcover

What is this book?

Homotopy Type Theory is one of the deepest ideas in contemporary mathematics — a unification of logic, topology, and computation in which proofs are paths and types are spaces. This book makes that revolution vivid and accessible without sacrificing rigour.

Like Gödel, Escher, Bach, it is structured as a series of dialogues between characters — Achilles and the Tortoise, joined at critical moments by the Crab, the Mole, and the enigmatic Mu — whose conversations unfold the mathematics one level at a time. Each chapter is indexed by its homotopy level (−2, −1, 0, 1, 2, …, ∞), and the structure of each chapter mirrors its own mathematical content.

The book is a strange loop: it teaches the theory it is written in, using the form it describes. Each dialogue challenge is formalized in Cubical Agda — one file per challenge, with key theorems proved, not merely stated.

The Hidden Acrostic

The first letter of each of the seventeen main chapter titles spells a message — a homage to the acrostic hidden inside Gödel, Escher, Bach. Look at the amber letters.

· The Unique Point (Prelude, h = −2)

T he Foundations in Crisis (h = −1)

H abitat of Types (h = 0)

E qual by Construction (h = 1)

P aths of Dependence (h = 2)

A ll Proofs Are Paths (h = 3)

T he Topology of Continuity (h = 4)

H omotopy and the Fundamental Group (h = 5)

I nfinite Tower: ∞-Groupoids (h = 6)

S paces and Types, Unified (h = 7)

T he Hierarchy of Homotopy Levels (h = 8)

H omotopy Equivalence (h = 9)

E quality by Equivalence: The Univalence Axiom (h = 10)

P ower of Univalence (h = 11)

R uled by Their Paths: Higher Inductive Types (h = 12)

O rbiting the Circle (h = 13)

O rder from Truncation (h = 14)

F oundations, Constructive (h = 15)

· The Type of All Types (Finale, h = ∞)

See all chapters with descriptions →

A Taste of the Dialogue

From Chapter 6 — Infinite Tower: ∞-Groupoids. The setting: before dawn, at the base of a lighthouse. The lamp has not been extinguished.

The lamp beam crosses the base window every fourteen seconds. Through the exterior glass, two pale salt-stain streaks are visible — both descending from the same crack, both ending at the same iron drainage ring. They did not take the same route through the stone.

Achilles: I've been thinking about paths. I have a type A — think of it as a space — and two points a and b. And I have two paths between them. Both go from a to b. Are they the same path?

Tortoise: What would "the same" mean to you?

Achilles: In a set, equality is binary. But we're not in a set. We're in a type — and types behave like spaces. So perhaps "the same" means there is a continuous deformation from one path to the other.

Crab (holding up one finger): A 2-path H is an inhabitant of the identity type of the identity type. We have applied the identity type constructor one level higher. One floor up.

Achilles: So to say that two paths are "the same," I must provide a witness whose sameness is itself a type-theoretic object — a 2-path.

Crab: Yes. And the first floor of the tower has non-trivial content.

Three Mathematicians, One Universe

L. E. J. Brouwer

1881 – 1966

Founder of mathematical intuitionism. Brouwer insisted that mathematical objects must be mentally constructed — not merely shown to be non-contradictory. A proof that something exists must exhibit it.

The constructive, the intuitive, the philosophical

Per Martin-Löf

1942 –

Swedish logician and philosopher. His intuitionistic type theory gave Brouwer's programme a precise formal syntax — turning the idea of "proof as construction" into a full-scale foundation for mathematics.

The architectural, the judgemental, the generative

Vladimir Voevodsky

1966 – 2017

Fields medallist and one of the architects of motivic cohomology. Voevodsky's Univalence Axiom — the insight that equivalent types are equal — became the foundation of Homotopy Type Theory.

The formal, the foundational, the computational

Each dialogue challenge is formalized in Cubical Agda — one file per challenge, with key theorems proved, not merely stated. Companion code uses {-# OPTIONS --cubical --safe #-} throughout. Univalence is a theorem, not an axiom. Higher Inductive Types are defined natively, with path constructors.