Univalent foundations of mathematics

Abstract

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.