Introduction to Homotopy Type Theory

An essential and up-to-date introduction to homotopy type theory with minimal prerequisites and over 200 exercises.

Egbert Rijke (Author)

9781108844161, Cambridge University Press

Hardback, published 6 November 2025

386 pages
22.9 x 15.2 x 2.2 cm, 0.734 kg

'The book of Egbert Rijke is a friendly introduction to Homotopy Type Theory (HoTT), a formal system for a new foundation of mathematics based on type theory, instead of set theory. Martin-Löf Type Theory (MLTT) is presented in the first part of the book, and HoTT in the second part by adding Voevodsky's univalence axiom and general inductive types. The last chapter is devoted to the construction and study of the logical circle. The development of HoTT can be traced back to the discovery of the topological interpretation of MLTT by Awodey-Warren and Voevodsky. But the fact that this interpretation is seldom discussed in the book can be surprising to the reader. But I confess that my understanding of HoTT was greatly improved by reading the book as it stands. It contains a set of well-chosen exercises. The logical circle in the last chapter is a revolutionary application.' André Joyal, Université du Québec à Montréal

This up-to-date introduction to type theory and homotopy type theory will be essential reading for advanced undergraduate and graduate students interested in the foundations and formalization of mathematics. The book begins with a thorough and self-contained introduction to dependent type theory. No prior knowledge of type theory is required. The second part gradually introduces the key concepts of homotopy type theory: equivalences, the fundamental theorem of identity types, truncation levels, and the univalence axiom. This prepares the reader to study a variety of subjects from a univalent point of view, including sets, groups, combinatorics, and well-founded trees. The final part introduces the idea of higher inductive type by discussing the circle and its universal cover. Each part is structured into bite-size chapters, each the length of a lecture, and over 200 exercises provide ample practice material.

Preface
Introduction
Part I. Martin-Löf's Dependent Type Theory: 1. Dependent type theory
2. Dependent function types
3. The natural numbers
4. More inductive types
5. Identity types
6. Universes
7. Modular arithmetic via the Curry-Howard interpretation
8. Decidability in elementary number theory
Part II. The Univalent Foundations of Mathematics: 9. Equivalences
10. Contractible types and contractible maps
11. The fundamental theorem of identity types
12. Propositions, sets, and the higher truncation levels
13. Function extensionality
14. Propositional truncations
15. Image factorizations
16. Finite types
17. The univalence axiom
18. Set quotients
19. Groups in univalent mathematics
20. General inductive types
Part III. The Circle: 21. The circle
22. The universal cover of the circle
References
Index.

Subject Areas: Mathematical foundations [PBC]