# Links

Here are some resources:

- 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”.

- Vladimir Voevodsky’s Univalent Foundations page, with many talks, notes, preprints, and other resources.
- A sequence of introductory postings at the n-Category Café by Mike Shulman: I, II, III, IV, V, VI.
- Andrej Bauer’s blog, with Coq tutorials and GitHub repository.
- 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’s nLab pages on the internal logic of a 2-topos.
- Here is a very good nLab page on HoTT with many resources.
- 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 Wiki for the Univalent Foundations program at the Institute for Advanced Study.
- Here is the page with video’s of the seminars given during the special year at the IAS.
- 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.)
- Here is video of a lecture by André Joyal at MSRI in April 2014.

To add something to this list, just leave a reply below.

### Like this:

Like Loading...

Another reference: Jason Gross is running a reading group at MIT on the HoTT Book spring 2014. The mailing list for the group is at http://mailman.mit.edu/mailman/listinfo/hott-reading-group, which allows you to add yourself and links to archives.

The link to Vladimir’s talk in the first bullet point above seems to have changed to http://video.ias.edu/univalent/voevodsky

A lecture by Robert Harper: http://www.cs.cmu.edu/~rwh/courses/hott/

All 26 lectures with videos and notes are available at the above-mentioned URL. More than 15,000 views so far, with more than 5000 hours of streaming.