Abstract
Two central questions in the foundations of mathematics are: 'What is a proof?' and 'What does it mean to be equal?'
The answers to these questions vary enormously, both through time, but also from one culture to another. The modern mathematical proof may seem the most rigorous of all alternatives. Still, the ideal of well-documented, accountable knowledge, communicated with a proof certificate, is in no way reached. Typically, the validity of extremely complicated mathematical proofs is still supported only by the community's trust in peer review performed by a few acknowledged experts.
Since the modern society depends on mathematics, secure foundations are important. In the digital era we have powerful tools for verifying (and to some extent generating) formal mathematical proofs. The central challenge is finding a language that has sufficient expressive power, and at the same time can be mechanically processed in an efficient way. Homotopy type theory addresses exactly this challenge.
In this approach equality has a topological interpretation, yielding great flexibility. Our project aims at further exploring this novel foundation of mathematics, and apply it to verify some challenging mathematical theories.
End Report
We can report significant progress on four of the seven topics that had been singled out as the contexts of research questions in the field of HoTT-UF that were both highly relevant and challenging. We shall describe this progress in the following paragraphs.
1. Homotopy canonicity
Canonicity means that terms can be brought into a form that directly reflects their meaning.
When using axioms in type theory, like UA, canonicity is compromised. Voevodsky's Conjecture states that in the case of UA, canonicity can be recovered when liberalized according to the new interpretation of equality (`homotopy canonicity'). Fellows Sattler and Kapulkin, in discussion with others at CAS and elsewhere, have given a deep and difficult proof of Voevodsky’s Conjecture. A germ of the proof (right Kan extension as an exact functor from semisimplicial to simplicial sets) was planted in a discussion of Sattler with Kapulkin at CAS in December. The result was subsequently elaborated, and has been presented by Sattler during a later stay at CAS, in a series of five exciting lectures that each lasted several hours, involving lively discussions with fellows. This result is generally considered a breakthrough in the field, corrobating the validity of UA. A publication of this proof is in preparation.
2. Cubical semantics and cubical type theory
Cubical semantics provided the first constructive consistency proofs for univalent mathematics, but had the drawback that it was not known whether they were standard models, that is, models that validate the other principles that mathematicians normally assume. In fact, already before the year at CAS, Sattler had shown that many of the cubical models were non-standard. Thus there was the urgent question of constructing a model that at the same time was a standard model. Four fellows, Awodey, Coquand, Riehl and Sattler, were able to come up with a variant of the cubical semantics, based on so-called equivariant fibrations, and show that this model structure is standard. This is a very important result, using novel techniques that could have an impact on classical homotopy theory as well. It also constitutes the first proof of the consistency of the Law of the Excluded Middle in cubical type theory. A joint publication of this proof is in preparation.
3. Formalization
Formal verification of mathematics is an important rationale of univalent foundations. During the year, several fellows contributed with substantial verifications that found their way to the repositories of formalized mathematics, such as github.com/UniMath/UniMath. We just mention a few of them. Grayson, during his first stay, formalized building blocks of higher algebraic K-theory such as exact categories and the definition of binary direct sum in additive categories. During his second stay he formalized the induction principle of the circle as elaborated on paper by Bezem and Buchholtz. Various other formalizations have been carried out by fellows Piceghello, Alfsvåg, van Doorn and Huber.
4. The Symmetry Book
The Symmetry Book, joint work in progress freely available at github.com/UniMath/SymmetryBook, is an undergraduate textbook in the univalent style, taking advantage of the native support in HoTT for symmetry in the form of types x =A x, greatly leveraged by the Univalence Axiom. In its current stage, this book is definitely work in progress. Some five fellows, including Dundas as the main author, have been involved in the writing so far; others can be expected to contribute in a later stage. The first chapters of the book are currently (as we write) in use in a seminar at UiB given by Bezem, in order to test out the existing material in the classroom. Later chapters may well make incursions into more advanced territory. Completing the book is an important goal for the years to come, with the generous support from CAS in the form of an alumni grant and a budget for publication of the results of this year. Both are gratefully acknowledged.
Certainly, the existing collaborations, and the collaborations initiated during the stay at CAS, will continue to bear fruit. We will use the CAS Alumn Fellowship grant and the CAS publication grant, as well as the RCN grant for the project “Computational Aspects of Univalence” and possible future grants, for this very purpose.
Fellows
-
Ahrens, Benedikt
-
Alfsvåg, Kristian
-
Awodey, Steve
-
Bordg, Anthony
-
Buchholtz, Ulrik
-
Coquand, Thierry
-
Dybjer, Peter
-
Grayson, Daniel R.
-
Hou (Favonia), Kuen-Bang
-
Huber, Simon
-
Joyal, André
-
Kapulkin, Chris
-
Lumsdaine, Peter LeFanu
-
North, Paige
-
Piceghello, Stefano
-
Riehl, Emily
-
Rijke, Egbert
-
Sattler, Christian
-
van Doorn, Floris
Previous events
-
12 Jun - 14 Jun 2019(all day)Ingneiørenes Hus Møtesenter Ingneiørenes Hus Møtesenter
-
11 Jun - 14 Jun 2019(all day)Ingeniørenes Hus Møtesenter Ingeniørenes Hus Møtesenter
-
25 Apr 201910:15 - 12:00652, Georg Morgenstiernes Hus, University of Oslo 652, Georg Morgenstiernes Hus, University of Oslo
-
29 Mar 201913:15 - 14:309460, Ole-Johan Dahls hus, Univerity of Oslo 9460, Ole-Johan Dahls hus, Univerity of Oslo
-
28 Mar 201914:15 - 16:00B1120, Niels Henrik Abels hus, University of Oslo B1120, Niels Henrik Abels hus, University of Oslo
-
29 Nov 201814:30 - 15:30Rest area 10th floor, Niels Henrik Abels hus, University of Oslo Rest area 10th floor, Niels Henrik Abels hus, University of Oslo
-
27 Aug - 29 Aug 2018(all day)Turret room, CAS Turret room, CAS
News
-
Alumni Spotlight: Bjørn Ian Dundas
20.12.2021 -
CAS Alumnus granted 34.7 million Swedish Kronor for analysing proofs
07.10.2020 -
‘Our modern society depends on correct mathematics’
25.06.2019 -
Project Update: 'Homotopy Type Theory and Univalent Foundations'
21.01.2019 -
Meet the Project: 'Homotopy Type Theory and Univalent Foundations'
21.09.2018 -
2018/19 CAS Projects: Religion, Media and Time, and Mathematics
08.08.2018