An introductory course to Homotopy Type Theory
This repository contains a book for a first introduction course to Homotopy Type Theory, accompanied by formalization projects in several proof assistants, closely following the material in the book.
The course was taught by Egbert Rijke at Carnegie Mellon University during the spring semester of 2018, and was aimed at advanced undergraduate students and graduate students from the Mathematics, Philosophy, and Computer Science departments.
The course consisted of 27 one-hour lectures, in which we covered most of the following topics:
This repositories contains formalizations of the first half of the course in several proof assistants: currently Agda and Coq. These formalization projects are designed to follow the course notes as closely as possible, and they include solutions to the exercises. From the dual point of view, the course notes form an extensive documentation of the formalization projects, and it is my hope that people will find it helpful to have such a documentation with the formalization.
Formalization projects of this course in more proof assistants that support homotopy type theory might be added in the future.
The course notes that I took are evolving into an introductory textbook for students who want to learn homotopy type theory for the first time. They are currently subject to frequent change, so my recommendation would be to have a look at the 2018 course notes or the 2019 summer school notes instead. Those can be found in the pdfs
folder of this repository.
To compile the notes, run latexmk -pdf hott-intro.tex
.