Elimination rule for identity types in Martin-Lof Type Theory

Question

The rule for identity type elimination still mystifies me, and I have not been able to find anything that satisfies me in any book.

Consider, for example, the form of the rule on p. 112 of Thompson:

\begin{array}{c} c: I(A,a,b) \hskip 0.6 cm d:C(a,a,r(a)) \\ \hline J(c,d): C(a,b,c) \end{array}

If the rule were just: \begin{array}{c} c: I(A,a,b) \hskip 0.6 cm d:C(a,a) \\ \hline J(c,d): C(a,b) \end{array} then I would understand it completely - from a verification $c$ of $a=b$ and a verification $d$ of $C(a,a)$, one can construct a verification of $C(a,b)$, and that's what $J(c,d)$ encodes.

But how can I move from a verification $c$ of $a=b$ and a verification $d$ of $C(a,a,r(a))$, to a verification of $C(a,b,c)$? I don't even see the intuition behind it.

Answer 1

The idea is that we want to allow our theorems to depend not only on $a$ and $b$, but also on the particular proof of equality! Here I'm assuming $r(a) : I(a,a)$ is reflexivity.

It's tricky to reason about what this means, since it's consistent that the only proofs of type $I(A,a,b)$ are reflexivity (this is called axiom k). That is, it's possible that $c$ is always $r(a)$! In fact, many "natural" models have exactly this property! Models where this property fails are called "proof relevant", and the idea is that types $C(a,b,c)$ might depend on which particular proof $c : I(A,a,b)$ we're given!

It's extremely surprising that we can understand terms of type $C(a,b,c)$ just by understanding terms of type $C(a,a,r(a))$. More than most induction principles, this feels like we're getting something for free. So when it comes to being confused by this principle, you're in very good company! Lots of people (myself very much included) have struggled with this, and there's a lot of resources for trying to understand it (see here, for instance).

The most natural way to understand the dependence on $c$, at least in my mind, is through the homotopy theoretic interpretation. So let's take a moment to talk about that. Here types are geometric spaces, and terms $a : A$ are points in $A$. Now, in homotopy theory, when do we consider two points to be "the same"? Precisely when there's a path from $a$ to $b$ in $A$. But now it should be very clear that there are multiple possible paths from $a$ to $b$, and thus multiple possible proofs of $I(A,a,b)$.

So now say we have a proposition $C$ which depends on $a,b$ as well as the path $p : I(A,a,b)$. For instance, we might have

$$C(a,b,p) = \prod_{p : I(A,a,b)} \sum_{q : I(A,b,a)} p \cdot q = r(a)$$

where homotopy theoretically we interpet $p \cdot q$ as the concatenation of the paths $p$ and $q$ (I'll not formally define it, though).

The magical thing (called "path induction" in this context) is that to prove the above claim for every $a,b,p$, it suffices to prove it for $a,a,r(a)$! Again, I agree that it's far from obvious that this should work. But here's a homotopy theoretic justification:

One can show that the space of paths one one endpoint fixed and one endpoint free is contractible, in the sense that, for any two such paths (which are now points in the space of all paths) there is a path between them (in the space of all paths). In the type theoretic interpretation, this is saying that for any two proofs $p,q : \sum_{b : A} I(A,a,b)$ there is a proof of $I \left ( \sum_{b : A} I(A,a,b), p, q \right )$. But this is good, because it means that every such proof is equal to $(a,r(a)) : \sum_{b : A} I(A,a,b)$. And we know that we can substitute equal things, so once we've proven $C(a, (a,r(a))$ we can substitute to get a proof of $C(a, (b,c))$ (where I've silently uncurried $C$. Obviously this isn't an issue).

---

Edit:

In the comments you bring up a reasonable point, that bringing in homotopy theory seems like some heavy duty machinery for something comparatively simple. Here's a (possibly anachronistic) view of how this might have been developed and understood in a pre-HoTT world.

First, remember that we use elimination rules in order to define functions. For instance, the elimination rule for $\mathbb{N}$ exactly says that we can define functions on $\mathbb{N}$ by recursion. So, if we want to be able to define functions out of an identity type $I(A,a,b)$, then we need the elimination rule to give us something of the form $J : C(a,b,p)$, where of course $p : I(A,a,b)$. That way we know where to send a given proof of equality $p$.

Now, you might say "if $r(a)$ is the only proof, can't we leave it as an implicit argument?" and while we probably could, it's fairly standard to not.

For instance, we define the type $\mathbf{1}$, which we want to think of as having exactly one inhabitant, $\star : \mathbf{1}$. But the way we encode that is with an elimination rule called singleton induction:

$$ \frac{{}}{\star : \mathbf{1}}\ \ (\mathbf{1} \text{ intro}) \quad \quad \frac{c : C(\star) \quad x : \mathbf{1}}{\mathtt{ind}_\mathbf{1}(C,c,x) : C(x)}\ \ (\mathbf{1} \text{ elim}) $$

It's then a theorem in the type theory that $\prod_{x : \mathbf{1}} x=\star$, so we don't need to specify uniqueness in the metalanguage. This is because our elimination rule says that the value of a function on $\mathbf{1}$ is completely determined by its action on $\star$.

Of course, our approach to the identity type is entirely analogous. Even if we're thinking of $I(A,a,b)$ as being either empty or uniquely inhabited, it's "more hygenic" in a sense to leave that as a theorem in the type theory, rather than try to force it in the metalanguage. This leads us to do exactly what we did with singleton induction. Since we want the entire type to be generated by $r(a)$, we define introduction and elimination rules:

$$ \frac{a : A}{r(a) : I(A,a,a)}\ \ (I\text{ intro}) \quad \quad \frac{c : C(a,a,r(a)) \quad p : I(A,a,b)}{\mathtt{ind}_{I}(C,c,p) : C(a,b,p)}\ \ (I\text{ elim}) $$

these are entirely analogous to the rules for singletons, and indeed we can prove inside the theory that

$$\prod_{(b,p) : \sum_{b : A} I(A,a,b)} (b,p) = (a,r(a))$$

I wasn't there, but I suspect it came as a surprise when people first realized that there are models of this type theory where the identity type can have more than one element.

---

I hope this helps ^_^

Answer 2

The core idea is that the identity type/family is inductively generated by the reflexive proof $r(a)$. $J$ is the induction principle.

So, just like we can prove $P(n)$ for an arbitrary natural number $n$ by establishing $P$ for the generating cases, $P(0)$ and $P(m) ⇒ P(\mathsf{suc}\ m)$, the point of $J$ is that we can prove predicates depending on identity proofs by establishing that they hold for the generators, of which there is only one. The unusual part about $I$ is that the entire family $I(A,a,b)$ is generated by a case where $a = b$.

Traditionally, the explanation behind this is that if $c : I(A,a,b)$, then actually $a$ and $b$ are the same, and $c$ is just $r(a)$, because there aren't any other things that $c$ could be. However, it's now pretty well known that there are other interpretations of what's underlying this inductive definition.

Answer 3

Your proposed rule would say: if $c$ proves that $a = b$, then "$b$ is as good as $a$" in the sense that in future constructions, we can replace $a$ by $b$.

The full rule is more general: if $c$ proves that $a = b$, then "$b$ is as good as $a$ and $c$ is as good as $r(a)$" in the sense that in future constructions, we can replace $a$ by $b$ and the "reflexivity" proof of $a = a$ by the proof $c$ that $a = b$.

This allows us to construct elements of types which rely on a proof that $a = b$ by just handling the case of the canonical "reflexivity" proof that $a = a$.

---

You ask about the intuition behind this rule. One intuition is that if $a$ and $b$ are equal, then a proof that $a$ and $b$ are equal is just proving the equality of two equal things, so it's essentially just reflexivity.

There's also a homotopical intuition: We can think of identity between objects in type theory as being like homotopy equivalence. If $a$ and $b$ are equivalent, i.e. there is a path $c$ from $a$ to $b$, then there is a homotopy from the identity path $r$ at $a$ to the path $c$, by keeping one endpoint fixed at $a$ and moving the other endpoint to $b$ along the path $c$.

Others probably have different perspectives. At the end of the day, this is just a rule in a formal system - one can try to give intuitive explanations of why the rule should be included in the system, but it's not possible to say precisely "how" we get something of type $C(a,b,c)$ from something of type $C(a,a,r(a))$. Answering this question would amount to proving the rule instead of including it as an axiom.