Preface


IAS Special Year on Univalent Foundations

A Special Year on Univalent Foundations of Mathematics was held in 2012-13 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.

{multicols}

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 Martin-Lö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.

{multicols}

3

  • Carlo Angiuli

  • Anthony Bordg

  • Guillaume Brunerie

  • Chris Kapulkin

  • Egbert Rijke

  • Kristina Sojakova

In addition, there were the following short- and long-term visitors, including student visitors, whose contributions to the Special Year were also essential.

{multicols}

3

  • Jeremy Avigad

  • Cyril Cohen

  • Robert Constable

  • Pierre-Louis Curien

  • Peter Dybjer

  • Martín Escardó

  • Kuen-Bang 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 complementMathworldPlanetmath 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 presentationMathworldPlanetmathPlanetmath you find before you — a remarkable inversionMathworldPlanetmathPlanetmath of the usual state of affairs in formalized mathematics.

Each of the above-named 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 2013-11-09 2:13:51
Last modified on 2013-11-09 2:13:51
Owner PMBookProject (1000683)
Last modified by PMBookProject (1000683)
Numerical id 1
Author PMBookProject (1000683)
Entry type Application
Classification msc 03B15