FoMUS: Foundations of Mathematics: Univalent Foundations and Set Theory
Date: 18 – 23 July 2016
Convenors: Balthasar Grabmayr (Berlin, GER), Deborah Kant (Berlin, GER), Lukas Kühne (Bonn, GER), Deniz Sarikaya (Hamburg, GER), Mira Viehstädt (Hamburg, GER)
Zermelo-Fraenkel axioms are widely assumed to be the foundation of mathematics within the mathematical practice of set theory. However, an increasing number of researchers are currently working on the univalent foundations as an alternative foundation of mathematics. This relatively young approach is based on homotopy type theory, which is a link between Per Martin-Löf's intuitionistic type theory and the homotopy theory from topology.
The workshop was opened with an introduction to these two different foundational theories, with an emphasis on the less popular homotopy type theory, and then progressed into in-depth panel discussions and research talks.
In addition to presentations of mathematical results regarding HoTT and axiomatic set theories (as well as their relations), formal requirements of foundations of mathematics in general, their limitations and their naturality were examined. Recently, it has become increasingly important to formalise mathematics by computer-aided formal proof systems, such as Coq. With this in mind, it was investigated which foundation is most suitable for the changing needs of mathematical practice.