In this text, I try to convey my excitement at the reading of the book published by the participants of last year's IAS program, under direction of Steve Awoodey, Thierry Coquand and Vladimir Voevodsky. As I write there (this is the title of this article), this remarkable work is at the crossroads of foundations of mathematics, topology and computer science. Indeed, the new foundational setup for mathematics provided by type theory may not only replace set theory; it is also at the heart of the systems for computer proof checking, and gave birth to a new kind of ``synthetic homotopy theory'' which is totally freed of the general topology framework.
Also remarkable is the way this book was produced: written collaboratively, using technology well known in open source software's development, then published under a Creative commons's license, and printed on demand.
This is not the only general audience paper on this subject, probably not the last one neither. Here are links to those I know of:
- Voevodsky's mathematical revolution, by Julie Rehmeyer (Scientific American)
- Penser types plutôt qu'ensembles, by Philippe Pajot (Science & Vie, October 2013)
- Voevodsky’s Univalence Axiom in Homotopy Type Theory, by Steve Awodey, Álvaro Pelayo, and Michael A. Warren (Notices of the AMS, September 2013)
