Programs · Proofs · Semantics · Homotopy
Lectures on
Type Theory
A continuous route from judgments and typed computation through dependent, categorical, homotopical, and higher-dimensional type theory.
Six connected routes
The book at a glance
- Part 1Typed Computation and Proof70 chapters
- Part 2Dependent Calculi and Their Extensions39 chapters
- Part 3Checking, Semantics, and Metatheory58 chapters
- Part 4Interaction, Probabilistic and Quantitative Semantics, and Quantum Computation19 chapters
- Part 5Homotopy Type Theory and Univalent Mathematics27 chapters
- Part 6Equality, Computed9 chapters
Ways into the text