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.