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:
- Steve Awodey, “Constructive type theory and homotopy”.
- Andrew Appel, “Introduction to the Coq proof assistant”.
- 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.
Mailing lists and other discussion forums
- The homotopy type theory google group is a mailing list for general research-level discussion.
- The hott-cafe google group is for those who may feel intimidated by the other list.
- There is an IRC channel
##hotton irc://chat.freenode.net open to anyone for real-time conversation. (For more information on IRC, see freenode.net. A browser-based client is available here.)
Web pages and other resources
- Of course, there is the homotopy type theory wiki (hosted at the nLab server).
- Here is the Wiki for the Univalent Foundations program at the Institute for Advanced Study.
- Here is a very good nLab page on HoTT with many resources.
- Andrej Bauer’s blog, with Coq tutorials and GitHub repository.
- Vladimir Voevodsky’s Univalent Foundations page, with many talks, notes, preprints, and other resources.
- Mike Shulman’s nLab pages on the internal logic of a 2-topos.
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.
