Lecture: Univalent Foundations of Mathematics
Vladimir Voevodsky
Abstract:
Set-theoretic approach to foundations of mathematics work well until one starts to think about categories since categories cannot be properly considered as sets with structures due to the required invariance of categorical constructions with respect to equivalences rather than isomorphisms of categories. On the other hand the underlying groupoids of categories are invariant (up to an equivalence) with respect to equivalences of categories. Hence, it is natural to think of categories as groupoids with structures. The same applies to higher categories. By Grothendieck's insight higher groupoids correspond to homotopy types which suggests that mathematics of all levels may be thought of as study of structures on homotopy types. Univalent foundations use the language of Martin-Lof type theories to directly work with structures on homotopy types without reducing them to sets.
