Preface
IAS Special Year on Univalent Foundations
A Special Year on Univalent Foundations of Mathematics was held in 201213 at the Institute for Advanced Study, School of Mathematics, organized by Steve Awodey, Thierry Coquand, and Vladimir Voevodsky. The following people were the official participants.
3

Peter Aczel

Benedikt Ahrens

Thorsten Altenkirch

Steve Awodey

Bruno Barras

Andrej Bauer

Yves Bertot

Marc Bezem

Thierry Coquand

Eric Finster

Daniel Grayson

Hugo Herbelin

André Joyal

Dan Licata

Peter Lumsdaine

Assia Mahboubi

Per MartinLöf

Sergey Melikhov

Alvaro Pelayo

Andrew Polonsky

Michael Shulman

Matthieu Sozeau

Bas Spitters

Benno van den Berg

Vladimir Voevodsky

Michael Warren

Noam Zeilberger
There were also the following students, whose participation was no less valuable.
3

Carlo Angiuli

Anthony Bordg

Guillaume Brunerie

Chris Kapulkin

Egbert Rijke

Kristina Sojakova
In addition, there were the following short and longterm visitors, including student visitors, whose contributions to the Special Year were also essential.
3

Jeremy Avigad

Cyril Cohen

Robert Constable

PierreLouis Curien

Peter Dybjer

Martín Escardó

KuenBang Hou

Nicola Gambino

Richard Garner

Georges Gonthier

Thomas Hales

Robert Harper

Martin Hofmann

Pieter Hofstra

Joachim Kock

Nicolai Kraus

Nuo Li

Zhaohui Luo

Michael Nahas

Erik Palmgren

Emily Riehl

Dana Scott

Philip Scott

Sergei Soloviev
About this book
We did not set out to write a book. The present work has its origins in our collective attempts to develop a new style of “informal type theory” that can be read and understood by a human being, as a complement^{} to a formal proof that can be checked by a machine. Univalent foundations is closely tied to the idea of a foundation of mathematics that can be implemented in a computer proof assistant. Although such a formalization is not part of this book, much of the material presented here was actually done first in the fully formalized setting inside a proof assistant, and only later “unformalized” to arrive at the presentation^{} you find before you — a remarkable inversion^{} of the usual state of affairs in formalized mathematics.
Each of the abovenamed individuals contributed something to the Special Year — and so to this book — in the form of ideas, words, or deeds. The spirit of collaboration that prevailed throughout the year was truly extraordinary.
Special thanks are due to the Institute for Advanced Study, without which this book would obviously never have come to be. It proved to be an ideal setting for the creation of this new branch of mathematics: stimulating, congenial, and supportive. May some trace of this unique atmosphere linger in the pages of this book, and in the future development of this new field of study.
The Univalent Foundations Program
Institute for Advanced Study
Princeton, April 2013
Title  Preface 

Canonical name  Preface 
Date of creation  20131109 2:13:51 
Last modified on  20131109 2:13:51 
Owner  PMBookProject (1000683) 
Last modified by  PMBookProject (1000683) 
Numerical id  1 
Author  PMBookProject (1000683) 
Entry type  Application 
Classification  msc 03B15 