Introduction to Homotopy Type Theory: (Series Number 219 Cambridge Studies in Advanced Mathematics)

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.

Table of Contents:
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.

About the Author :
Egbert Rijke is Postdoctoral Research Fellow at Johns Hopkins University and is a pioneering figure in homotopy type theory. As one of the co-authors of the influential book 'Homotopy Type Theory: Univalent Foundations of Mathematics' (2013), he has played a pivotal role in shaping the field. He is also a founder and lead developer of the agda-unimath library, which stands as the largest library of formalized mathematics written in the Agda proof assistant.

Review :
'The mathematician's dream of identifying objects that are equivalent is a foundational axiom of Homotopy Type Theory, which combines Voevodsky's univalence axiom with a homotopical interpretation of Martin-Löf's dependent type theory. Rijke has produced a beautiful introduction that demystifies these univalence foundations, with a curated list of examples and exercises that enable newcomers to rapidly develop the intuitions necessary to learn how to write their own proofs, either on paper or with a computer proof assistant.' Emily Riehl, Johns Hopkins University 'The original HoTT Book was written at the IAS as an experiment - and reads like it. It is high time for a mature, uniform, pedagogical introduction to this revolutionary field, which combines homotopy theory, constructive type theory, and higher category theory. Egbert Rijke has given us just such a book.' Steve Awodey, Carnegie Mellon University 'Homotopy type theory is a new and rapidly changing field, and until now there have been no up-to-date textbooks accessible to students. Rijke, himself a major contributor to the subject, has produced an excellent book that starts from the basics, assuming no background in type theory, and leads up to the univalence axiom, higher inductive types, and the basic ideas of synthetic homotopy theory. This book should be valuable to anyone wanting to get involved in this new and exciting area.' Mike Shulman, University of San Diego '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