Several current proof assistants, such as Agda and Epigram, provide *uniqueness of identity proofs (UIP)*: any two proofs of the same propositional equality are themselves propositionally equal. Homotopy type theory generalizes this picture to account for higher-dimensional types, where UIP does not hold–e.g. a universe (type of types), where equality is taken to be isomorphism, and there can be many different isomorphisms between two types. On the other hand, Coq does not provide uniqueness of identity proofs (but nor does it allow you to define higher-dimensional types that contract it, except by adding axioms).

What determines whether UIP holds? The answer lies in two elimination rules for identity types, called `J` and `K`. ` J` is the fundamental elimination rule for identity types, present in all (intensional) dependent type theories. Here is a statement of `J`, in Agda notation, writing `Id x y` for the identity (propositional equality) type, and `Refl` for reflexivity.

J : (A : Set) (C : (x y : A) -> Id x y -> Set) -> ((x : A) -> C x x Refl) -> (M N : A) (P : Id M N) -> C M N P J A C b M .M Refl = b M

`J` reads like an induction principle: `C` is a predicate on on two propositionally equal terms. If you can give a branch `b` that, for each `x`, covers the case where the two terms are both `x` and related by reflexivity, then `C` holds for any two propositionally equal terms.

`J` certainly seems to say that the only proof of `Id` is reflexivity—it reduces a goal that talks about an arbitrary proof to one that just covers the case of reflexivity. So, you would expect UIP to be a consequence, right? After all, by analogy, the induction principle for natural numbers tells you that the only natural numbers are zero and successor of a nat.

Here’s where things get confusing: UIP is *not* a consequence of `J`, as shown by the first higher-dimensional interpretation of type theory, Hofmann and Streicher’s groupoid interpretation. This gives a model of type theory that validates `J`, but in which UIP does not hold. UIP can be added as an extra axiom, such as Streicher’s K:

K : (A : Set) (M : A) (C : Id M M -> Set) -> C Refl -> (loop : Id M M) -> C loop

`K` says that to prove a predicate about `Id M M`, it suffices to cover the case for reflexivity. From this, you can prove that any `p : Id M M` is equal to reflexivity, and from that you can prove that any `p q : Id M N` are propositionally equal (by reducing one to reflexivity using `J`). An alternative to adding this axiom is to allow the kind of dependent pattern matching present in Agda and Epigram, which allow you to define K.

So what is `J` really saying? And why is it valid in homotopy type theory? **When there are more proofs of propositional equality than just reflexivity, why can you show something about all of them by just covering the case for reflexivity?**

Find out after the cut!

Continue reading