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:
- 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.
- 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. - 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:
- 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.
- 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.
- 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?
Homotopy Type Theory 
I just thought I’d clarify the Observational Type Theory position and ask what the situation is here.
In OTT, propositional equality of sets and values is defined to ensure that provably equal canonical sets have an effective isomorphism between them which allows us to ensure canonicity. This canonicity result in no way relies on proof irrelevance, but only on consistency. As it happens, OTT permits only direct structural explanations of set equality (e.g., equal Pi types have equal domains and for equal elements of those domains, equal ranges) so the isomorphisms induced never do any real rearrangement of values. Proof irrelevance (and run-time erasability) become feasible as a consequence of that latter choice, but are not essential to the construction. Our Agda model delivers canonicity but Agda does not treat all the equality proofs as definitionally equal.
One could very well imagine a different choice, where the structural proofs of equality were supplemented by nontrivial isos. Proof irrelevance and erasure would, of course, be the price to pay for this choice, but it is at least plausible that the essence of the isomorphism construction (and its canonicity) would survive. Someone should have a go!
Meanwhile, do I understand correctly that this more 2-dimensional NuPRL than 2-dimensional Coq and takes the same positions in the usual trade-offs between so-called extensional and intensional type theories? What is decidably-checkable “evidence” for a proposition? A typing derivation for a term, or just a term? Given that OTT shows that an extensional propositional equality can be achieved without losing canonicity or decidable type-checking (effectively reifying as terms the derivations which hide behind the equality reflection rule in NuPRL), we should be surprised if 2DTT is not susceptible to a similar treatment. So thank you for giving me something to stare at!
First, a clarification question on your clarification: do you disagree with my statement (in the related work) that “OTT also exploits uniqueness of identity proofs, and is thus not immediately compatible with higher-dimensional structure”? What I had in mind when I wrote that was (1) OTT uses heterogeneous equality, which in the higher dimensional case would at least need to be revised to depend on the reason the types are equal (or just treated as a macro for a homogeneous equation that inserts the appropriate subst). and (2) the coherence term {s || Q : S = T} would need to be adjusted accordingly. Because of this, proof-irrelevance (at least propositionally) seems to me to be baked into the basic setup of OTT, as described in your PLPV paper. The “immediately” was my wiggle room for doing something different, like you describe here. When you say “proof irrelevance” above, do you mean propositional (the presence of a term Id p q whenever p q : Id M N) or definitional?
We make no claims of decidability in this paper. The essence of the 2-dimensional restriction is that we posit UIP at that level, which likely makes type checking undecidable because it involves proof search. But this is an artifact of the 2-dimensional restriction that we’re exploring; in the fully higher-dimensional case, nothing is ever cut off, and it is plausible that type checking would again be decidable. In any case I consider it a minor issue; type checking is grotesquely infeasible even when decidable, and it’s just not relevant to any mathematical practice, as more than two decades of experience has shown.
This is exciting! I won’t have time to read the paper carefully for quite a while, but it’s great to see progress towards “the computational meaning of univalence”. I like how this takes to its logical conclusion the claim that univalence is just giving “the correct meaning” to “equality” on the universe.
I suspect that the answer to your final question may be no (that is, the desired models are not precluded) in the case of 2-dimensional type theory (groupoids are fairly strict objects), but possibly yes in the case of higher groupoids or homotopy types. Or, at least, it might be that we don’t yet know how to construct models of higher groupoids that are sufficiently strict. But since at the moment we know very few models of univalence for sure, I’m not sure that it’s yet possible to answer the question definitively either way. I haven’t thought very deeply about models of univalence myself; maybe someone else can say more. I can certainly say that having some aspects of univalence hold definitionally would be nice for purposes of doing homotopy theory in type theory!
Does the inversion of logical priority between the groupoid structure of types and the J-elimination rule mean that in order to generalize to the un-truncated case, one would have to make fully explicit the structure of a weak ω-groupoid?
Yes, the full higher-dimensional case would require some sort of (coinductive?) formulation of the complete hierarchy of dimensions. Dan tells me that Altenkirch is working on something like this, which is encouraging and possibly relevant to our approach. If this can be achieved, then I would argue that our formulation is the correct one, since it admits a computational interpretation of univalence. At any rate it seemed worth trying out as an alternative to setups that take J as a primitive notion.
That’s certainly a strong argument. I have to say I would be sad to lose the nice way in which the simple J-rule, being a special case of the general notion of inductive family, automatically produces all the structure of a higher groupoid (or homotopy type). What would happen if you added a separate Id type-former to your theory, with the usual J-elimination rule? I presume you wouldn’t be able to prove that it was the same as your judgmental notion of equivalence? I feel like that would make for an untidy theory once we add dependent types and inductive families.
I agree that the way that J generates all the structure of a higher groupoid is nice, but I wouldn’t be so sad about losing that once we have a nice type-theoretic definition of a higher groupoid…
Regarding your other question, in the paper, we show that we can define an identity type from the equivalence judgement, which satisfies J. If you added a separate Id type former, with just refl and J, then I think you *would* be able to show that it is equivalent to the one that internalizes equivalence. The reason is that any two types that satisfy refl and J (and the computation rule) are weakly equivalent. Here’s the proof in Agda:
data Id {A : Set} (a : A) : A -> Set where
Refl : Id a a
jay : {A : Set} (C : (x y : A) -> Id x y -> Set)
-> {M N : A} -> (P : Id M N)
-> ((x : A) -> C x x Refl)
-> C M N P
jay _ Refl b = b _
resp : {A B : Set} (f : A -> B)
-> {M N : A} -> (P : Id M N)
-> Id (f M) (f N)
resp f p = jay (\ x y _ -> Id (f x) (f y)) p (\ _ -> Refl)
data Id' {A : Set} (a : A) : A -> Set where
Refl' : Id' a a
jay' : {A : Set} (C : (x y : A) -> Id' x y -> Set)
-> {M N : A} -> (P : Id' M N)
-> ((x : A) -> C x x Refl')
-> C M N P
jay' _ Refl' b = b _
module WEq {A : Set} where
f : {x y : A} -> Id x y -> Id' x y
f = λ p → jay (λ x y _ → Id' x y) p (λ _ → Refl')
g : {x y : A} -> Id' x y -> Id x y
g = λ p' → jay' (λ x y _ → Id x y) p' (λ _ → Refl)
α : {x y : A} (p : Id x y) -> Id (g (f p)) p
α = λ p → jay (λ x y p' → Id (g (f p')) p') p (λ _ → Refl)
β : {x y : A} (p : Id' x y) -> Id (f (g p)) p
β = λ p' → jay' (λ x y p → Id (f (g p)) p) p' (λ _ → Refl)
η : {x y : A} (p : Id x y) -> Id (resp f (α p)) (β (f p))
η = λ p → jay (λ x y p' → Id (resp f (α p')) (β (f p'))) p (\ _ -> Refl)
Of course, people have been looking for a “nice” definition of higher groupoid for years; I haven’t seen any one yet which I think is halfway as nice as J. If someone does come up with a really nice definition of higher groupoid using type theory, I think it will be of great interest to many people who don’t care about type theory as such. I spent a while once trying to write down a nice coinductive definition of higher groupoids, but eventually I admitted defeat.
Also, yes, surely any two types with the same elimination rule will be equivalent. But what I was thinking is that your proof of J for your defined identity types goes by induction on the structure of all types in the theory, correct? So any time you add a new type-former, you’d need to prove that you can extend the definition of J to types formed in that way. I don’t see how to do that for the standard identity-type-former. So I guess what I’m saying is that it’s not clear to me that once you add ordinary identity types, your defined identity types will still satisfy J.