Computational Aspects of Univalence

One of the results of this last year of CAU is about the symmetries of spheres in homotopy type theory med univalens (HoTT). These results are known in homotopy theory, and the idea of CAU is to find out how to obtain these in HoTT, aiming at computer verification. The sphere of dimension 1 is a circle. The sphere of dimension 2 is the boundary (surface) of a solid ball in 3D (indeed the circle is the boundary of a disk in 2D). This idea can be generalized to define the sphere of dimension n, denoted Sn. There is another, for HoTT more convenient definition of spheres of dimension n>1. For S2 this idea can be visualized by fixing two poles, North and South, and rotating a meridian, say, the one of Greenwich, by moving the point where the meridian of Greenwich crosses the equator along the equator. The equator is a circle, so this procedure explains how to obtain S2 from S1, and can be iterated to obtain each S3 from S2 (hard to visualise!), and so on. Symmetries are transformations that can be reversed and preserve the geometric shape of the object. For example, every rotation is a symmetry of the circle. Reflection is another symmetry of the circle. Symmetries can be composed to give other symmetries. Concerning rotations of the circle, it is clear that one need not rotate more than one full turn. Also, any rotation of the circle against the direction of the clock can always be achieved by a clockwise rotation as well. In HoTT with univalence, symmetries of the sphere Sn have type Sn=Sn. We have proved in HoTT that S1=S1 is equivalent to S1+S1. Here the left S1 in S1+S1 stands for all possible rotations, and the right S1 stands for all possible rotations followed by a reflection. However, Sn=Sn is not equivalent to Sn+Sn for n>1. For n>1, the symmetries of S2, S3, ... are much more complex. Nevertheless we have shown in HoTT that Sn=Sn always falls apart in two equivalent components, one with and one without reflection.

Rekrutteringseffekter: Robin Adams, postdoktor ved CAU 2016-2017, har gått over til fast stilling som lektor ved Chalmers, Göteborg. Håkon Gylterud, forsker ved CAU 2017-2019, har fått en innstegstilling som 1. amanuensis ved Universitetet i Bergen. Kristian Alfsvåg, stipendiat ved CAU 2015-2019, har fått fast stilling som lektor ved NLA Høgskolen i Bergen. Internasjonalt forskningssamarbeid har økt betraktelig takket være CAU og prosjektet Homotopy Type Theory and Univalent Foundations ved Senter for Grunnforskning (DNVA, Oslo, 18/19), ledet av Bezem og Dundas. Tverrfaglig forskningssamarbeid har blitt videreført og styrket, og har ført til nye prosjektsøknader.

In this project we study the computational aspects of the Univalence Axiom (UA) and the role of univalence in K-theory. UA is a new axiom in homotopy type theory, recently proposed by Voevodsky. Type theory is a logical formalism originally developed as a foundation of mathematics, and very useful for the mechanical verification of mathematical proofs. The latter is important for the independent verification of complicated mathematical results. Type theory has good computational properties: carefully designed proofs can be executed as algorithms on a computer. To preserve this, new axioms should also be given a computational interpretation. This is the first objective of our project. Homotopy theory is a branch of algebraic topology studying so-called homotopies, the deformations of one function into another. This gives rise to a notion of homotopy equivalence of spaces, and the homotopy type of a space is its class modulo homotopy equivalence. Homotopy type theory emerged in recent years as a surprising interdisciplinary connection between computer science, logic and mathematics. The fundamental innovation is the interpretation of a type as a topological space, instead of as a set, which has been the traditional interpretation. The new connection is a happy marriage: type theory is valid under the interpretation of a type as a homotopy type. Both sides benefit from the connection. In type theory, the new interpretation introduces a new concept of equality, namely that of homotopies and homotopy equivalence. This gave rise to the new Univalence Axiom and other innovations, such as higher inductive types. In homotopy theory one gets a new methodology for building the theory from (new) first principles, called the "synthetic" approach. This comes with new insights and new possibilities, such as computing with formal proofs. Therefore our second main objective is to apply this new methodology to coherence and K-theory.