Showing changes from revision #9 to #10: Added | Removed | Changed

Here are some resources.

Introductory courses

• Bob Harper?’s course . aimed at a Computer Science audience.

• Andrej Bauer’s [course] on homotopy theory and type theory. This page also contains links to the courses by Egbert Rijke and Martin Escardo? .introduces the univalent foundations using literate agda.

• Andrej Bauer’s course on homotopy theory and type theory.

• Egbert Rijke’s courses focuses on synthetic homotopy theory.

Books

• the HoTT book

• Leon Chwistek, The Theory of Constructive Types: Principles of Logic and Mathematics, Krakow: University Press, 1925, 98 pp. Extracted from the Annales de la Société Polonaise de Mathématique. (In DjVu format) Linked from this page, under Bibliography, On logic and mathematics.

• Joyal’s Categorical Homotopy Type Theory

Other

• CMU-HoTT Group’s local activities.

• CMU blog

• HoTTeST HoTT seminar