Introduction to Homotopy Type Theory

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.

• 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.

'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