Just Kidding: Understanding Identity Elimination in Homotopy Type Theory | Homot...

Just Kidding: Understanding Identity Elimination in Homotopy Type Theory

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!

To answer this question, we can reformulate J as follows (due to Paulin-Mohring), which corresponds to thinking of A and M as parameters Id{A} M N, and N as the only (non-uniform) index:

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

This version holds one of the two terms, M, fixed throughout the rule. It is equivalent to the above (as long as you have function types around).

Next, we uncurry the predicate, and package the second term together with the propositional equality proof as follows:

  PathFrom : {A : Set} -> A -> Set
  PathFrom {A} M = Σ[ y ∶ A ] Id M y

  J : (A : Set) (M : A) (C : PathFrom M -> Set)
      -> C (M , Refl) 
      -> (P : PathFrom M) -> C P
  J A M C b (.M , Refl) = b

In homotopy type theory, a type is interpreted as a topological space, where an element of the type is interpreted as a point in the space, and an identity proof as paths between the corresponding points. The type PathFrom M is defined to be a Σ-type, pairing a point y with a path (propositional equality proof) from M to y. This version of J says that, to prove something about an arbitrary path from M, it suffices to consider the case where the other endpoint is M itself, and the path is reflexivity.

That is, the real force of J is to assert that PathFrom M is inductively defined, with generator (M , Refl). For example, you can prove that any inhabitant of PathFrom M is propositionally equal to (M , Refl), and therefore that any two inhabitants of PathFrom M are propositionally equal.

And this principle holds even when there are non-reflexivity paths. The interpretation of propositional equalities between paths (i.e. of propositional equalities between propositional equalities) is homotopy (continuous deformation). The intuition for why J holds but K does not is that a PathFrom M has one endpoint free, which gives you additional freedom in how you can deform the path. To deform (N , P) into (M , Refl), you move the endpoint N over to M, while deforming the P into reflexivity.

For example, picture a circle in a space, with a hole on the inside of the circle. You can’t deform the circle into the identity loop on a point, because the hole gets in the way. But if you unhook one of the endpoints, you can drag it to the other, avoiding the hole, while deforming the path between them into the identity. The circle could be thought of a circle : Id base base, which is not homotopic (propositionally equal) to Refl : Id base base, contradicting K. However, (base , circle) is deformable into (base , Refl) at type PathFrom base.

Indeed, when doing proofs using J, the place where a proof will break down is often in choosing a predicate C that makes sense for all of PathFrom M, when the theorem you want to prove talks about a specific second endpoint. Go ahead and try proving K from J, or try proving directly using J that the higher fundamental groups are abelian. Choosing such a predicate is analogous to generalizing a theorem statement in such a way that an induction goes through.

This idea that PathFrom M is inductively defined is a new tool that homotopy type theory provides for the study of homotopy theory. For example, as type theorists know, you can define the rest of the groupoid structure on paths (composition, inverses, and the corresponding composition, unit, and inverse laws) from it–this is the usual implementation of transitivity, symmetry, etc. using J.

On the other hand, this understanding of J provides some insight into a well-known, but, honestly, somewhat strange, type-theoretic fact: the standard induction principle that you read off from an inductive family definition tells you how an arbitrary element of the family is generated, but it doesn’t (obviously) tell you about how the specific instances are generated. For example, here’s the definition of Fin n (numbers less than n) and the corresponding J-like induction principle:

  data Fin : Nat -> Set where
    fz : ∀ {n} -> Fin (S n)
    fs : ∀ {n} -> Fin n -> Fin (S n)

  fin-elim : (C : (n : Nat) -> Fin n -> Set)
           -> (∀ n -> C (S n) fz)
           -> (∀ n (f : Fin n) -> C n f -> C (S n) (fs f))
           -> (n : Nat) (f : Fin n) -> C n f

The induction principle says that an arbitrary element of Fin n for an arbitrary n is either fz or fs. But it doesn’t directly tell you what to do with an element of say, Fin 0. For example, it’s tricky to prove that there are no inhabitants of Fin 0:

  no-fin-z : Fin 0 -> Void

To do so using the above eliminator, you need to use a “large elimination” (a type computed by recursion on a term):

  no-fin-z f = fin-elim Pred (\ _ -> ) (\ _ _ _ -> ) Z f where
    Pred : (n : Nat) -> Fin n -> Set
    Pred 0 f = Void
    Pred (S _) _ = Unit

That is, you define a predicate that works for an entirely general element of the family by saying “when the instance of the family is the one I’m interested in, do the right thing, and otherwise do something that’s easy to prove”. A related idea is that, in Martin-Lof type theory without a universe, you cannot prove that the successor function is injective, because to do so you need a large elimination.

On the other hand, dependent pattern matching, as in Agda, effectively gives you the K-like elimination rules for each inductive family. For example, you can prove the above by giving a function with no cases:

  no-fin-z/pm : Fin Z -> Void
  no-fin-z/pm ()

Indeed, dependent pattern matching can be reduced to an identity type with K; see Conor McBride’s thesis.

In sum, the J-like elimination rules leave open the question of what’s in each instance of the family. Sometimes, as with Fin, you can use them to answer this question, by computing with the indices. Other times, as with Id, you cannot. This is why J isn’t obviously nonsense in a type theory where there are more propositional equalities than just reflexivity; and the above intuition about deforming paths with a free endpoint is why it in fact makes sense.