Centre for Advanced Study

at the Norwegian Academy of Science and Letters

Homotopy Type Theory and Univalent Foundations

Information

Former 2018/2019 Natural Sciences - Medicine - Mathematics

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
    Assistant Professor University of Birmingham 2018/2019
  • Alfsvåg, Kristian
    PhD Candidate University of Bergen (UiB) 2018/2019
  • Awodey, Steve
    Professor Carnegie Mellon University 2018/2019
  • Bordg, Anthony
    Postdoctoral Fellow University of Cambridge 2018/2019
  • Buchholtz, Ulrik
    Postdoctoral Fellow Technical University of Darmstadt 2018/2019
  • Coquand, Thierry
    Professor Chalmers University of Technology & University of Gothenburg 2018/2019
  • Dybjer, Peter
    Professor Chalmers University of Technology & University of Gothenburg 2018/2019
  • Grayson, Daniel R.
    Professor Em. University of Illinois at Urbana-Champaign 2018/2019
  • Hou (Favonia), Kuen-Bang
    Assistant Professor University of Minnesota 2018/2019
  • Huber, Simon
    Postdoctoral Fellow University of Gothenburg 2018/2019
  • Joyal, André
    Professor Em. Université du Québec à Montréal 2018/2019
  • Kapulkin, Chris
    Assistant Professor University of Western Ontario 2018/2019
  • Lumsdaine, Peter LeFanu
    Assistant Professor Stockholm University 2018/2019
  • North, Paige
    Assistant Professor Ohio State University 2018/2019
  • Piceghello, Stefano
    PhD Candidate University of Bergen (UiB) 2018/2019
  • Riehl, Emily
    Assistant Professor Johns Hopkins University 2018/2019
  • Rijke, Egbert
    Postdoctoral Fellow University of Illinois at Urbana-Champaign 2018/2019
  • Sattler, Christian
    Postdoctoral Fellow University of Gothenburg 2018/2019
  • van Doorn, Floris
    Postdoctoral Fellow Carnegie Mellon University 2018/2019

Previous events

News

Group leader

  • Marc Bezem

    Title Professor Institution University of Bergen (UiB) Year at CAS 2018/2019
  • Bjørn Ian Dundas

    Title Professor Institution University of Bergen (UiB) Year at CAS 1993/19952018/2019
LOGO