preface.tex

\chapter*{Preface}
\label{cha:preface}

% Uncomment this if you think Preface should appear in TOC
%\addcontentsline{toc}{chapter}{Preface}
\subsection*{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.

\begin{multicols}{\OPTprefacecols}{
\begin{itemize}
\item[] Peter Aczel
\item[] Benedikt Ahrens
\item[] Thorsten Altenkirch
\item[] Steve Awodey
\item[] Bruno Barras
\item[] Andrej Bauer
\item[] Yves Bertot
\item[] Marc Bezem
\item[] Thierry Coquand
\item[] Eric Finster
\item[] Daniel Grayson
\item[] Hugo Herbelin
\item[] Andr\'e Joyal
\item[] Dan Licata
\item[] Peter Lumsdaine
\item[] Assia Mahboubi
\item[] Per Martin-L\"of
\item[] Sergey Melikhov
\item[] Alvaro Pelayo
\item[] Andrew Polonsky
\item[] Michael Shulman
\item[] Matthieu Sozeau
\item[] Bas Spitters
\item[] Benno van den Berg
\item[] Vladimir Voevodsky
\item[] Michael Warren
\item[] Noam Zeilberger
\end{itemize}
}
\end{multicols}

\noindent There were also the following students, whose participation was no less valuable.

\begin{multicols}{\OPTprefacecols}{
\begin{itemize}
\item[] Carlo Angiuli
\item[] Anthony Bordg
\item[] Guillaume Brunerie
\item[] Chris Kapulkin
\item[] Egbert Rijke
\item[] Kristina Sojakova
\end{itemize}
}
\end{multicols}

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

\begin{multicols}{\OPTprefacecols}{
\begin{itemize}
\item[] Jeremy Avigad
\item[] Cyril Cohen
\item[] Robert Constable
\item[] Pierre-Louis Curien
\item[] Peter Dybjer
\item[] Mart{\'\i}n Escard{\'o}
\item[] Kuen-Bang Hou
\item[] Nicola Gambino
\item[] Richard Garner
\item[] Georges Gonthier
\item[] Thomas Hales
\item[] Robert Harper
\item[] Martin Hofmann
\item[] Pieter Hofstra
\item[] Joachim Kock
\item[] Nicolai Kraus
\item[] Nuo Li
\item[] Zhaohui Luo
\item[] Michael Nahas
\item[] Erik Palmgren
\item[] Emily Riehl
\item[] Dana Scott
\item[] Philip Scott
\item[] Sergei Soloviev
\end{itemize}
}
\end{multicols}

\subsection*{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 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. 

\mentalpause

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.

\bigskip

\begin{flushright}
The Univalent Foundations Program\\
Institute for Advanced Study\\
Princeton, April 2013
\end{flushright}

%%%%%%%%%%%%% end of scope of local macros
% Local Variables:
% TeX-master: "hott-online"
% End: