What is meant by a computational interpretation of univalence?

Question

In homotopy type theory the univalence axiom implies function extensionality.

Suppose we have a recursive set we are not sure is empty (e.g. the set of even integers$\geq 4$ that are not a sum of two primes). Then via characteristic functions this becomes a claim about two functions $\mathbb{N}\to \mathbf{2}$ being equal.

I would not expect a machine to settle this. Then what do people mean when they talk about a computational interpretation of univalence?

Answer 1

Roughly speaking, a type theory is computationally adequate if there is an algorithm that evaluates a term belonging to any type into a "normal form" of that type. The simplest form of this is when dealing with closed terms (not involving any variables or hypotheses) belonging to a "base" type such as $\mathbb{N}$ or $\mathbf{2}$, in which case the normal forms really are the obvious "canonical forms" such as numerals $s(s(s(\dots(s(0))))):\mathbb{N}$ or booleans ${\rm t}, {\rm f}:\mathbf{2}$. Thus, this aspect of computational adequacy (called canonicity) says that if you define a particular natural number without using any assumptions, the computer can (at least in principle) tell you exactly which natural number you've defined.

Things get subtler when you talk about terms belonging to higher types such as a function-type $\mathbb{N}\to \mathbf{2}$. In general, the canonical forms of a type are those obtained from its introduction rule, which in the case of a function-type means a $\lambda$-abstraction. So canonicity implies that any function $\mathbb{N}\to \mathbf{2}$ can be evaluated to a $\lambda$-abstraction; but, unlike the situation for numerals in $\mathbb{N}$, it could still be the case that two syntactically-distinct $\lambda$-abstractions define extensionally equal functions. So computational adequacy doesn't give an algorithm for deciding whether two functions are equal, which as you noted would be impossible.

As Reid pointed out in the comments, it's important to distinguish here between propositions, which are types, hence elements of a universe type $\mathcal{U}$, and booleans, which are elements of the type $\mathbf{2}$. Since $\mathbf{2}$ is a base type, any closed term of type $\mathbf{2}$ does evaluate, in a computationally adequate theory, to $\rm t$ or $\rm f$. But $\mathcal{U}$ is a higher type, and as with functions two propositions can be syntactically distinct and yet extensionally equal (have the same truth value). Thus, evaluating a proposition to a "canonical form" doesn't tell you whether that proposition is true or false -- unless you've proven that that proposition is decidable, in which case it can be represented by an element of $\mathbf{2}$. (Of course, in classical mathematics the Law of Excluded Middle asserts that every proposition is decidable -- and this is why LEM is a non-computational axiom.)

Even subtler than this is what happens when you ask for computational adequality for open terms (those involving free variables and assumptions). This is a stronger property than canonicity, called normalization, and in this case the "normal forms" that terms are evaluated to may not be obtained from the introduction rule of their type; they could also be obtained from the elimination rule of the type of a free variable (a "neutral" term). For instance, in the context of a free variable $f:\mathbb{N}\to\mathbb{N}$, we have a term $f(0):\mathbb{N}$, which cannot be normalized any further, even though it is not a numeral.

None of this is specific to univalence. The problem of giving a computational interpretation of univalence means to specify a type theory in which univalence is true (either as an axiom or as a theorem) and which is computationally adequate in one or more of these senses. With regard to the discusion in the comments, this implies that the univalence term $\rm ua$ cannot appear in a normalized closed term of base type, since any such term must be a canonical form such as a numeral; but it could still appear in a normalized closed term of higher type, or in a normalized open term. (This requires, of course, that there be some kind of "computation rules" that apply to $\rm ua$ enabling it to be reduced away in at least some cases, in contrast to how in Book HoTT computation "get stuck" when it encounters the bare axiom $\rm ua$.) This is not quite the same as giving a model of type theory in which everything computes, although practically and historically the two are often intertwined.

Finally, just to note the current status of computational interpretations of univalence, canonicity for one form of cubical type theory was proven in 2016 by Simon Huber, while normalization for a different form of cubical type theory was proven in 2021 by Sterling and Angiuli.