\input zb-basic
\input zb-ioport
\iteman{io-port 05900213}
\itemau{Voevodsky, Vladimir}
\itemti{Univalent foundations of mathematics.}
\itemso{Beklemishev, Lev D. (ed.) et al., Logic, language, information and computation. 18th international workshop, WoLLIC 2011, Philadelphia, PA, USA, May 18--20, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-20919-2/pbk). Lecture Notes in Computer Science 6642. Lecture Notes in Artificial Intelligence, 4 (2011).}
\itemab
Summary: Over the last two years deep and unexpected connections have been discovered between constructive type theories and classical homotopy theory. These connections open a way to construct new foundations of mathematics alternative to the ZFC. These foundations promise to resolve several seemingly unconnected problems-provide a support for categorical and higher categorical arguments directly on the level of the language, make formalizations of usual mathematics much more concise and much better adapted to the use with existing proof assistants such as Coq and finally to provide a uniform way to approach constructive and ``classical'' mathematics. I will try to describe the basic construction of a model of constructive type theories which underlies these innovations and provide some demonstration on how this model is used to develop mathematics in Coq.
\itemrv{~}
\itemcc{}
\itemut{}
\itemli{doi:10.1007/978-3-642-20920-8\_4}
\end