Links

Introductory videos, talks, and blog posts

• A series of introductory talks on the Univalent Foundations Program were given at the IAS in December 2010. The talks can be viewed here, and among them are the following talks:
  1. Steve Awodey, “Constructive type theory and homotopy”.
  2. Andrew Appel, “Introduction to the Coq proof assistant”.
  3. Vladimir Voevodsky, “Univalent foundations of mathematics”.
• A sequence of introductory postings at the n-Category Café by Mike Shulman: I, II, III, IV, V, VI.
• A sequence of introductory blog postings by Bob Harper at his blog Existential Type: I, II, III.
• A talk presenting the univalent foundation by Thierry Coquand relying on the following development in Agda due to Nils Anders Danielsson.
• Mike Shulman gave a seminar on HoTT at UCSD, here are the slides.
• Mike Shulman gave a minicourse at Swansea, here are the slides.
• Steve Awodey gave a talk on HoTT and Univalent Foundations at CMU, here are the slides.
• Peter Aczel gave a talk on the Univalence Axiom at the Third European Set Theory Conference in Edinburgh, here are the slides.
• Egbert Rijke and Bas Spitters gave a series of lectures at RU Nijmegen, here are the slides: (HITs), (reals)
• Here is the page with video’s of the seminars given during the special year at the IAS.
• Here is video of a lecture by André Joyal at MSRI in April 2014.
• A course given by Bob Harper with videos and notes.
• A mailing list for the spring 2014 HoTT Book reading group at MIT, which allows you to add yourself and links to archives.
• The 2022 HoTTEST Summer School page has links to a youtube playlist consisting of all the lectures for the summer school and to a github repository with all the lecture notes and exercises.

Mailing lists and other discussion forums

• The homotopy type theory Zulip server is a discussion forum for anything and everything about homotopy type theory.
• The homotopy type theory google group is a mailing list for general research-level discussion.  It is not very active.
• The hott-cafe google group is for those who may feel intimidated by the other list.  It is also not very active.
• There is an IRC channel ##hott on https://libera.chat/.  It is also not very active.

Web pages and other resources

• For some years there was a homotopy type theory wiki hosted at the nLab server.  This has now been deprecated in favor of direct contributions to the main nLab.
• An archived copy of the Wiki for the 2012-2013 Univalent Foundations program at the Institute for Advanced Study.
• Here is an nLab page on HoTT with many resources.
• Andrej Bauer’s blog, with Coq tutorials and GitHub repository.
• Vladimir Voevodsky’s Univalent Foundations page has many talks, notes, preprints, and other resources from 2014 and before.
• Egber Rijke’s textbook Introduction to Homotopy Type Theory

To add something to these lists, just leave a reply below.  Note that your comment may be deleted after your suggestion has been incorporated above.