Title: Univalent Foundations

Speaker: Daniel R. Grayson (Illinois)

Time: 14:45-15:20 (GMT+0), 2021.08.12

Abstract:

Homotopy type theory, together with the partition of types into levels and the univalence axiom developed by Voevodsky, provides both a new logical foundation for mathematics, called Univalent Foundations, and a formal language usable with computers for checking the proofs mathematicians make. As a foundation, it replaces set theory with a framework where propositions and sets are defined in terms of a more primitive notion called {\em type} -- in this framework the notion of symmetry arises at the most basic level -- from the logic. As a formal language, it encodes the axioms of mathematics and the rules of logic simultaneously, and it promises to make the extraction of algorithms and values from constructive proofs easy. As a mathematical topic, it offers an intriguing range of open problems at all levels of accessibility. I will give an intuitive introduction to these recent developments.