'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
