Preface

The title of this book is deliberately plain. Type theory is not treated here as a collection of notations attached to logic, programming languages, category theory, and homotopy theory. It is one subject, and the subtitle names four views of the same constructions: programs that execute, proofs that justify them, semantic accounts that expose their models and limits, and homotopy that reveals the higher structure of equality.

The book is therefore one continuous course rather than a catalogue of type systems. It begins with typed computation and proof, builds dependent type theory from its judgments, and then develops implementation, metatheory, semantics, homotopical interpretation, and computational accounts of equality. Programming-language theory is one of the course’s principal spines, not a collection of detached applications. Rows, modules, objects, effects, resources, protocols, and analyses isolate problems that return in dependent form; elaboration, staging, compilation, and verified kernels test whether the theory controls complete transformations rather than isolated terms. Games, probabilistic and reversible programs, differential calculi, optics, and quantum programs continue the same test at the semantic level. Each development ends with the theorem or executable result appropriate to its exact calculus.

The intended reader knows ordinary programming languages and the mathematics of a bachelor’s degree: elementary logic, calculus, linear algebra, and perhaps a little abstract algebra. No familiarity with formal judgments, derivation trees, induction on rules, category theory, topology, or homotopy theory is assumed. Chapter 1 supplies the metalanguage. Category theory and topology are built when the mathematics first requires them.

The course is long because its subject is large. Brevity is not obtained by turning proofs into citations or definitions into slogans. A result needed in the main line is proved in the book whenever its proof can reasonably fit there. When a genuinely book-length theorem must be imported, the exact statement and hypotheses are recorded before it is used. The reader should normally be able to reconstruct an argument from the current and immediately preceding pages.

Four threads

Programs. A calculus is not understood merely because its typing rules have been listed. We calculate with its terms, follow evaluation, and, where the subject permits it, connect the formal development to an executable checker, elaborator, interpreter, compiler pass, or verified artifact. A typed translation states the relation it preserves and proves that claim at the source and target signatures actually used.

Proofs. The Curry–Howard correspondence begins the story but does not end it. The book proves safety, normalization, canonicity, principality, coherence, abstraction, and soundness results for exact signatures. It also constructs counterexamples when a desired theorem is false.

Semantics. Different questions call for operational models, logical relations, realizability, domain theory, category theory, and homotopy theory. Each semantic language is introduced through a calculation before it is used to establish a general theorem.

Homotopy. Identity types lead from equality proofs to paths, higher paths, equivalences, univalence, higher inductive types, and synthetic homotopy theory. The required topology is developed in the course; it is not assumed as an undeclared second prerequisite.

Eight principles of exposition

1. One exact syntax per calculus. Each representative calculus has one displayed signature and one substitution invariant. Named variables, $\alpha$-equivalence, and capture-avoiding substitution are fixed for the dependent spine in chapter 26. Explicit substitutions appear in chapter 54 as an object of study, not as a silent notation change.

2. The problem and first calculation come before the taxonomy. A new object is introduced because the preceding calculus cannot type a program, validate a proof, or support a construction. When the abstraction is difficult, its smallest useful instance is calculated first and the invariant feature is isolated before the general definition is stated. A failed nearby definition is shown only when it is tempting and explains a load-bearing clause. Alternatives are compared only after one working definition has been used.

3. Rules come before consequences. Every type former is presented by formation, introduction, elimination, and computation rules, followed when appropriate by a uniqueness rule. A new judgment is followed by a complete derivation, and no rule is used before it is stated.

4. The proof mechanism remains visible. Definitions, constructions, lemmas, theorems, and substantive remarks share one counter. Calculations display their decisive steps; inductions treat the rule families that carry the argument; long proofs are divided into lemmas with stated roles.

5. Complete premises appear somewhere. The main text uses the presupposition convention of convention 26.14; appendix A restores the full premises of the representative rule families. Compression is typographical, not logical.

6. Proofs are complete or marked. A genuinely repetitive argument may be delegated to a named exercise. A draft gap is printed as a red $\text{[TODO: proof]}$ rather than disguised as a proof sketch, and no later result may depend on it while it remains open.

7. Every extension is a delta. Once a base signature has been proved sound, each extension states exactly which rules it adds, removes, or replaces and which metatheorems must be repaired.

8. Optional mathematics remains optional. A starred development may deepen or extend the course, but no unstarred definition, proof, required example, or artifact depends on it. When the core needs a substantial part of an optional development, the shared foundation is extracted, the optional chapter is split, or the mature material is promoted; it is not copied. A short theorem may be reproved locally only when that proof improves the exposition. Every starred chapter names its direct starred prerequisites, so a reader can skip an optional route without discovering a hidden dependency later.

The compact page, the theorem–proof rhythm, and the expectation that the reader reproduce complete mathematical operations follow the lecture-text tradition represented by Ivanov and Winitzki.

Notation and metalanguage

The book has one global metalanguage even when a chapter retains standard notation from its literature. Substitution acts postfix: $E[u/x]$, $E[B/X]$, and $E[\theta ]$; right-action composition is written $\theta ;\eta$. Object-language application is juxtaposition $fa$, explicit type application is $t[A]$, meta-level operators use parentheses, and an evaluation context is filled as $E⟨e⟩$. Root contraction, compatible reduction, many-step reduction, and elaboration are respectively ${⇝}_0$, $⟶$, ${⟶}^{\ast }$, and $⇝$. Double brackets are reserved for semantic interpretation; syntax translations and erasures are named.

By default, $\mathrm{\Gamma }$ is a term context, $\mathrm{\Theta }$ a type or kind context, $\mathrm{\Delta }$ a linear or ordered context, $\mathrm{\Psi }$ a dimension or modal context, $\theta$ a finite substitution, $\eta$ a semantic valuation, $\sigma$ a runtime store, $\rho$ a record row, and $ϵ$ an effect row. A chapter that follows a different field standard says so at the point of first use. The complete semantic and reverse-glyph index is appendix C.

Architecture of the course

Part I develops typed programming and proof from simple types through polymorphism, modules, subtyping, effects, resources, concurrency, protocols, logical frameworks, extraction, and static analysis. Part II then fixes one intensional dependent base and develops universes, identity, data, recursion, realizability, rewriting, and dependent forms of resources, effects, objects, and control.

Part III begins at the trusted boundary with checking, normalization, elaboration and unification, tactics, reflection, metaprogramming, declaration checking, erasure, and execution. Its compiler sequence follows typed terms through partial evaluation, staging, equality evidence, intermediate languages, closure conversion, A-normal form, secure and parallel compilation, and realistic verified metatheory. Each pass fixes its source, target, and preservation or simulation claim.

The same part rebuilds the semantic machinery rather than assuming it: algebraic syntax, categorical logic, realizability, models, coherence, games, monoidal semantics, modalities, guarded domains, and parametricity. Their invariants differ, but their interfaces belong to one course.

Part IV applies that machinery to reversible computation, optics, probabilistic languages and logics, dependent probability, differential calculi and automatic differentiation, and three stages of quantum programming. Each chapter names its endpoint: safety, adequacy, full abstraction, transformation correctness, or artifact behavior.

Part IV constructs the required topology before interpreting types as $\mathrm{\infty }$-groupoids, builds a homotopical model of univalence before adopting the axiom, and then develops synthetic homotopy and univalent mathematics. Finally, part V compares strict, observational, cubical, and higher-observational approaches to computation with equality.

In the following map, an arrow from one part to another means that the core of the second part may use the core interface constructed in the first. It does not assert that every chapter in the first part is a prerequisite.

The map stops at part level; chapter titles and prerequisite notes carry the finer dependency information where the reader needs it. A proof-assistant route follows the core of part I, the dependent base through chapter 34, and the checking and declaration sequence beginning at chapter 48; chapter 140 is its optional artifact-level capstone. A language and compiler route follows abstraction, effects, resources, objects, and refinement into their dependent counterparts, then adds the transformation sequence from chapter 127 through chapter 139. A quantum-programming route adds linear and dependent-linear typing, symmetric monoidal semantics, reversible computation, and chapter 184–chapter 186; it assumes no quantum mechanics beyond the finite-dimensional linear algebra developed there. A univalent-foundations route adds the full development of part IV and then compares the computational equality systems of part V. These are routes through one course, not separate books with duplicated foundations.

How to read and work

Read with paper beside the book. Reproduce the displayed calculations, construct complete derivations, restore suppressed premises, and calculate judgmental normal forms before reading past them. When a proof is long, first write down the obstruction and the purpose of each lemma; the text is organized so that this outline can be checked locally.

The strongest local exercises follow the definition, rule, or calculation they test. Problems remain at the end only when their length or synthesis would interrupt that development. Each chapter with exercises closes with a seminar: a coherent sequence from calculations through proofs and counterexamples to synthesis or implementation, with a short suggested route for a first reading. The seminar is not a gate, and none of its problems is a prerequisite for later chapters. No exercise carries a theorem needed by the main line; such a result is stated and proved in the exposition.

A statement about underivability should be justified by a model, a normal-form argument, or an induction on derivations, never by failure to find a term. Every exercise carries an effort rating: one star marks a short local exercise, two stars a multi-step exercise or one requiring a non-obvious idea, and three stars a substantial construction, proof, synthesis, or implementation problem. The rating measures effort, not importance or optionality. Every exercise is answered in full and respects the same prerequisite boundary as the main text. Mathematical exercises have complete solutions in appendix B; practical projects have complete worked tutorials in appendix F.

A star on a chapter, section, or run-in title marks an advanced or optional branch, not a weaker proof standard. No unstarred development depends on a starred one. A starred development may depend on the core and on the direct starred prerequisites named in its compact prerequisite note; it may serve as a prerequisite only for another starred or terminal development. The title star and prerequisite note are the chapter-level dependency map. Stars on exercises have the separate meaning given above: they measure effort.

Sources, self-containment, and status

The breadth and system comparisons are informed by Angiuli and Gratzer [AG26]. The rule-first presentation of the dependent base draws on Palmgren, Nordström–Petersson–Smith, and Rijke [Pal14, NPS90, Rij25]. The homotopical development is checked against the HoTT Book and Rijke [Uni13, Rij25]. The semantic chapters use Hofmann and the categories-with-families literature [Hof97, CCD21].

The final part relies on the primary observational and cubical papers: Pujet–Tabareau for ${\mathrm{TT}}^{\mathrm{obs}}$, CCHM and ABCFHL for two cubical designs, and the AKS internal-parametricity calculus for the published core of H.O.T.T. [PT22, CCHM18, ABC^+21, ACKS24]. Sources establish provenance and check exact rules and theorems; citations are not substitutes for arguments that belong in the course. Differences of notation are resolved in favor of the single notation table in appendix C.

Red TODOs mark mathematical or editorial work still owed. Status-bounded developments distinguish published theorems, conditional consequences, semantic constructions, implemented behavior, and conjectures. The distinction is mathematical.