Colloquium Talk - Daniel Grayson (University of Illinois at Urbana-Champaign): "Homotopy Type Theory and Univalent Foundations"
This year the Center for Advanced Study is holding a special year on Homotopy Type Theory and Univalent Foundations, organized by Marc Bezem and Bjørn Dundas.
Homotopy type theory, with the partition of types into levels and the univalence axiom developed by Voevodsky, provides both a new logical foundation for mathematics (Univalent Foundations) and a formal language usable with computers for checking the proofs mathematicians make daily. As a foundation, it replaces set theory with a framework where propositions and sets are defined in terms of a more primitive notion called "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 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.
NB! Coffee/Tea/Biscuits from 14.00.