[[!redirects resources]] [[!redirects Resources]] # Introductory courses * [[Bob Harper]]'s [course](https://www.cs.cmu.edu/~rwh/courses/hott/) aimed at a Computer Science audience. * [[Martin Escardo]] [introduces](https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html) the univalent foundations using literate agda. * [[Andrej Bauer]]'s [course](https://github.com/andrejbauer/homotopy-type-theory-course) on homotopy theory and type theory. * [[Egbert Rijke]]'s [courses](http://www.andrew.cmu.edu/user/erijke/hott/) 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.](http://www.monoskop.org/Leon_Chwistek) * Joyal's [[Categorical Homotopy Type Theory]] # Other * CMU-HoTT Group's [[local activities]]. * [CMU blog](https://cmuhott.wordpress.com/) * [HoTTeST](http://uwo.ca/math/faculty/kapulkin/seminars/hottest.html) HoTT seminar