Canonicity for 2-Dimensional Type Theory | Homotopy Type Theory

Canonicity for 2-Dimensional Type Theory

A consequence of the univalence axiom is that isomorphic types are equivalent (propositionally equal), and therefore interchangable in any context (by the identity eliminaiton rule J). Type isomorphisms arise frequently in dependently typed programming, where types are often refined to describe their values more precisely. For example, the type list A can be refined to a type vec A n classifying vectors of length n. Then, when you forget the extra information, you get a type that is isomorphic to the original. For example, list A is isomorphic to Σ n:nat.vec A n (vectors of an existentially quantified length).

As an example of a context, consider a monoid structure on a type A, represented represented by the type family

Monoid A =
Σ (m : A → A → A).
Σ (u : A).
Σ (assoc : Π x y z. Id (m (m x y) z) (m (m x y) z)).
Σ (lunit : Π x. Id (m u x) u).
Σ (runit : Π x. Id (m x u) u). unit

Using the univalence axiom and identity elimination, we can lift the isomorphism between lists and vectors to one between Monoid (list A) and Monoid(Σ n:nat.vec A n). That is, we can automatically derive a monoid structure on vectors from one on lists (or vice versa):

subst Monoid (univalence listVecIso) : Monoid (list A) → Monoid(Σ n:nat.vec A n)


However, because univalence is an axiom, and subst is only defined for reflexivity, this is a stuck term—it doesn’t compute! This means that canonicity fails: there are closed terms of type nat that are not equal to a numeral. This precludes a standard computational interpretation of type theory as a programming language, with an operational semantics for closed terms obtained by orienting the β-like equalities. There is an open conjecture by Voevodsky that type theory with univalence enjoys canonicity up to equivalence (i.e., the operational semantics would be obtained by orienting equivalences, not just equalities).

In a new paper, Robert Harper and I show how to obtain canonicity for the special case of 2-dimensional type theory. The key idea is to reformulate type theory based on a judgemental, rather than propositional, account of equivalence:

1. We have a judgement Γ ⊢ α : M ≃ N : A representing an equivalence α between terms M and N of type A. The groupoid structure of each type is made explicit, by giving a type-directed definition of the equivalence judgement: equivalence of functions is function extensionality; equivalence of sets is isomorphism; etc. Identity (reflexivity), inverses (symmetry), and composition (transitivity) are also defined in a type-directed manner.
2. The functorial action of each type/term family is made explicit. We define
   map (usually called subst), which states that families of types respect equivalence, by induction on the family of types. And similarly for resp, which says that families of terms respect equivalence.
3. The identity type can be defined by internalizing this judgemental notion of equivalence, such that the identity elimination rule J is derivable from subst. (This is not true for standard formulations, where the groupoid structure is conversely derived from J.)

Using this formulation, subst Monoid (univalence listVecIso) (m,u,a,l,r) is not stuck: it computes! Specifically, it wraps m with pre- and post-compositions, coercing vectors to lists and back; it sends u to its image under the isomorphism; and it shows that the equations are preserved by collapsing inverses. Thus, we can run subst as a generic program. We formalize this as a canonicity result, which says that every closed term of type bool is equal to either true or false.

This formulation generalizes extensional 1-dimensional type theory, as in NuPRL, to the 2-dimensional case:

1. NuPRL contains a judgemental notion of equality, which is defined in a type-directed manner, subject to the constraint that equality is always an equivalence relation. In the two dimensional case, this generalizes to our judgemental notion of equivalence, which is subject to the constraint that it must always be groupoidal.
2. In NuPRL, the meaning of a judgement x:A ⊢ B type includes functionality: if M and N are equal elements of A, then B[M/x] and B[N/x] are equal types. Similarly, equal instances of an open term x:A ⊢ M : B are equal. For 2-dimensional type theory, functionality becomes functoriality, and the transport between equal instances has computational content; this is our map and resp.
3. In NuPRL, the identity type internalizes judgemental equality, and J is definable from functionality. In the two-dimensional case, this generalizes to an internalization of the 2-cell structure of equivalence, and J is definable from functoriality.

This analogy is key to our proof of canonicity, which generalizes the NuPRL semantics to groupoids, rather than equivalence relations.

Thus, another message of the paper is that higher-dimensional concepts can be integrated into extensional type theory. However, this has implications for strictness: in this formulation of 2-dimensional type theory, we take various equivalences that hold for the univalence axiom (e.g. those specifying the functorial action of the type constructors) and make them hold as definitional equalities. This feels right from a programming perspective, and lets us achieve a standard result of canonicity-up-to-equality. However, my main question for this blog’s audience is: does this preclude some of the models you are interested in?