This entry collects links related to the forthcoming book
Introduction to Homotopy Type Theory,
Cambridge Studies in Advanced Mathematics,
Cambridge University Press
which introduces homotopy type theory in general and Martin-Löf's dependent type theory, the Univalent Foundations for Mathematics and synthetic homotopy theory in particular. The book is based on a course taught by Egbert Rijke at Carnegie Mellon University in the spring semester of 2018, and is expected to be published in 2021.
Resources:
pdf (2018 course notes) (221 pages)
pdf (2019 summer school notes) (134 pages)
The book contains three chapters:
The first chapter introduces the reader to Martin-Löf's dependent type theory. The fundamental concepts of type theory are explained without immediately jumping into the homotopy interpretation of type theory.
The second chapter is an exposition of Voevodsky‘s Univalent Foundations for Mathematics. In this chapter we gradually extend dependent type theory with function extensionality, propositional truncation, the univalence axiom, and the type theoretic replacement axiom.
The third chapter studies higher inductive types, and develops homotopy theory and concepts from higher category theory in type theory.
The main formalization of the book is in Agda.
Parts of the book have also been formalized in Coq.
Last revised on August 4, 2020 at 07:53:00. See the history of this page for a list of all contributions to it.