During the academic year 2012-13, the School of Mathematics conducted a special program on a new approach to the foundations of mathematics entitled Univalent Foundations of Mathematics. The program was co-organized by Professor Vladimir Voevodsky of the School and Members Steve Awodey of Carnegie Mellon University and Thierry Coquand of the University of Gothenburg, Sweden. There were approximately 25 participating members as well as many short term visitors.

This program provides an alternative to the commonly accepted approach to the foundations of mathematics based on Zermelo-Fraenkel set theory with the axiom of Choice. Univalent foundations are based instead on type theory which has recently experienced renewed interest due to its use in computer proof assistants, for which it is better suited than set theory due to its good computational properties. It was proposed by Professor Voevodsky in 2010. His vision was to remake the foundations so that pure mathematicians can take full advantage of computer assistants.

Two discoveries have led to the possibility of a new foundation on the basis of type theory. The first one is Grothendieck’s conjecture, proved by Mikhail Kapranov, Steklov Institute, and Voevodsky, which states that the “world” of infinity groupoids is the same as the world of homotopy types. The second one is a method of introducing equality in constructive type theories which goes back to Member Per Martin-Löf of Stockholm University. Two more factors played instrumental roles in making possible the univalent foundations as they are now: the work of Member Steve Awodey and his co-workers on the homotopy-theoretic interpretation of Martin-Löf identity types, which relates the two discoveries just mentioned and the existence of the proof assistant Coq, which is based on the Martin-Löf type theory.

Professor Voevodsky has worked on computer-based proof assistants since 2004 when the word “univalent” appeared in this context for the first time. Especially important was the 2009 course on programming languages taught by Andrew Appel in Princeton University’s computer science department in the fall of 2009 which was based on the use of Coq. The resulting conception of univalent foundations is a foundational system of type theory with an intrinsic homotopical character, augmented by principles of reasoning, such as Voevodsky’s new univalence axiom, that strengthen this interpretation and with an accompanying implementation in a computational proof assistant.

In the first term Professor Voevodsky lectured weekly on the subject of type systems. A working group devoted to the Coq system was organized by Member Andrej Bauer, University of Ljubljana, and focused on modifying the Coq proof assistant to be more useful for univalent foundations. Contributors to this effort were Members Hugo Herbelin, Assia Mahboubi, Matthieu Sozeau, all from the French National Institute for Research in Computer Science and Control. By the end of the first term, a working system was in place for use during term two.

Another working group was devoted to developing a systematic, informal style of type theory. This project, organized by School Member Peter Aczel of The University of Manchester, soon evolved into the large-scale project of writing a book in which the basics of univalent foundations and the results of the special year are developed in an exemplary informal style.

A third working group was devoted to formalizing homotopy theory in type theory. The main contributors to this effort were visiting student Guillaume Brunerie, École Normale Supérieure, Paris, and Members Daniel Licata, Carnegie Mellon University, Peter Lumsdaine, Dalhousie University and Michael Shulman of the University of California, San Diego.

directions of work had formed, each of which resulted in a noteworthy product. One was the development of basic homotopy theory in univalent foundations, including new type theoretic proofs and their formalization in the Coq system. Many homotopy groups of spheres were calculated and their proofs formalized, as were other classic results of homotopy theory. Another emphasis was the writing of the book on the univalent foundations by members of the School. This book, available free online at http://www.homotopytypetheory.org/book/ is a remarkable collaborative effort and should serve as a useful resource for teaching homotopy type theory and for disseminating the results of the special year. As a third area, work on a next generation proof assistant was started. Access http://uf-ias-2012.wikispaces.com/seminar for a list of all seminars and http://uf-ias-2012.wikispaces.com/Tutorials for all tutorials.