Robin Adams: How to Compute with Univalence

Abstract

Type theory is a discipline founded on a remarkable and still (in my opinion) not well understood coincidence: the same syntax of types and terms can describe mathematical objects (sets and elements), logic (propositions and proofs) and computer science (specifications and programs).  Homotopy type theory (HoTT) adds a fourth interpretation: spaces and points.

The Univalence Axiom behaves beautifully under two of these interpretations.  In the homotopical interpretation, it says that universes are classifying spaces for homotopy types.  In the mathematical interpretation, it states that isomorphic structures can be identified, and it is exciting to have a rigorous formal system in which this is possible.

But it breaks the computational interpretation.  We don't know how to read an application of the univalence axiom as a program.  And we don't know what a program should do when given an application of the univalence axiom as input.  Perhaps it is simply impossible to give a computational interpretation, but some of us are not prepared to give up just yet. 

In this talk, I will present two attempts to give a computational interpretation to the univalence axiom.  The "conservative" approach is to try to write down a computation rule for the univalence axiom, and prove it has all the nice properties that our other computation rules satisfy.  This has successfully been done for higher-order propositional logic (a subsystem of HoTT), but not for the full HoTT (yet).  The "radical" approach is to change the definition of equality itself.

This is joint work with Marc Bezem (the conservative) and Andrew Polonsky (the radical).  I will assume no prior knowledge of type theory for this talk.