Links

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 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 ##hott on 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.)

Of course, there is the homotopy type theory wiki (hosted at the nLab server).
An archived copy of the Wiki for the 2012-2013 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.