February 23
Dimitris Tsementzis,
Rutgers University
Univalent Foundations and Set Theory
The Univalent Foundations is a proposed foundation for mathematics that takes as primitive a notion of space (rather than a notion of set). I will introduce the basic concepts of the Univalent Foundations from first principles, and give an overview of a class of formal systems, called Homotopy Type Theories, that can be used to formalize these basic notions. I will then describe how to construct a model of set theory in the Univalent Foundations, explain the consequences of the construction, and discuss several open problems. In the process, I will demonstrate the implementation of everything I talk about in a proof assistant.