Here are some resources:
- A series of introductory talks on the Univalent Foundations Program were given at the IAS in December 2010. These can be viewed here:
- 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.
To add something to this list, just leave a reply below.
