23/07/2013, 16:00 — 17:00 — Room P3.10, Mathematics Building
Vladimir Voevodsky, Institute for Advanced Study
Univalent Foundations of Mathematics
I will outline the main ideas of the new approach to foundations of
practical mathematics which we call univalent foundations.
Mathematical objects and their equivalences form sets, groupoids or
higher groupoids. According to Grothendieck's idea higher groupoids
are the same as homotopy types. Therefore mathematics may be
considered as studying homotopy types and structures on them.
Homotopy type theories, the underlying formal deduction system of
the univalent foundations allows one to reason about such objects
directly.