Homotopy Type Theory
and the
Univalent Foundations of Mathematics
Homotopy type theory refers to a new interpretation of Martin-Löf's constructive type theory into homotopy theory. Propositional equality between intensionally distinct terms is interpreted as homotopy. The interpretation makes use of methods from abstract homotopy theory such as Quillen model categories, as well as related methods from higher-dimensional category theory.
A survey article on homotopy type theory, containing references to some of the current literature, can be found here:
"Type theory and homotopy".
Univalent foundations refers to Vladimir Voevodsky's new program for a comprehensive, computational foundation for mathematics based on the homotopy interpretation of type theory. The type theoretic univalence axiom relates propositional equality with homotopy equivalence. The program is being implemented with the help of the automated proof assistant Coq.
More information on the Univalent Foundations Program can be found at Voevodsky's website here:
"Univalent foundations". (Or directly here.)
In 2012-13 there will be a year-long special program at the Institute for Advanced Study devoted to the Univalent Foundations Program. It is being co-organized by Steve Awodey, Thierry Coquand, and Vladimir Voevodsky.
More information about this special year can be found on the IAS website here:
"Univalent foundations at IAS".
A series of three 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".
In March 2011 there was a workshop on "The Homotopy Interpretation of Constructive Type Theory" at the Oberwolfach Mathematical Research Institute, co-organized by Steve Awodey, Richard Garner, Per Martin-Löf, and Vladimir Voevodsky. Some information can be found on the MFO website.
See the HomotopyTypeTheory.org website for more information.