Anders Mortberg: "Cubical Methods in Homotopy Type Theory and Univalent Foundations"

7th of October, 2021. Part of the Topos Institute Colloquium. ----- Abstract: One of the aims of Homotopy Type Theory and Univalent Foundations (HoTT/UF) is to provide a practical foundation for computer formalization of mathematics by building on deep connections between type theory, homotopy theory and (higher) category theory. Some of the key inventions of HoTT/UF include Voevodsky's univalence axiom relating equality and equivalence of types, the internal stratification of types by the complexity of their equality, as well as higher inductive types which allow synthetic reasoning about spaces in type theory. In order to provide computational support for these notions various cubical type theories have been invented. In particular, the Agda proof assistant now has a cubical mode which makes it possible to work and compute directly with the concepts of HoTT/UF. In the talk I will discuss some of the mathematical ideas which motivate these developments, as well as show examples of how computer mechanization of mathematics looks like in Cubical Agda. I will not assume expert knowledge of HoTT/UF and key concepts will be introduced throughout the talk.