Univalent Foundations of Mathematics
Univalent Foundations of Mathematics

Chris Kapulkin , Princeton University
Fine Hall 314
The Univalent Foundations of Mathematics is a new foundational system, proposed by Vladimir Voevodsky, building on a recently discovered deep connection between logic (more precisely, type theory) and homotopy theory. Many logical methods can be then applied to problems from homotopy theory and, conversely, homotopytheoretic viewpoint is useful in understanding some logical constructions. In the talk, I will explain this connection and survey the main results of the Univalent Foundations program.