5
$\begingroup$

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.

$\endgroup$
3
  • 1
    $\begingroup$ It's worth pointing out that there is a new site on proof assistants which would be receptive of such a question, though it is in private beta at this time. $\endgroup$
    – Couchy
    Feb 11 at 18:43
  • $\begingroup$ Thanks, I have posted it there too! $\endgroup$ Feb 11 at 18:46
  • 1
    $\begingroup$ It's best not to duplicate questions, especially since this has already been answered, but future questions would be welcome. $\endgroup$
    – Couchy
    Feb 11 at 18:48

4 Answers 4

6
$\begingroup$

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 ^_^

$\endgroup$
5
  • $\begingroup$ Thanks, that is very helpful. I agree the homotopy picture is nice. But I would like to know why I should take the analogy seriously. If there is some fact about the nature of verifications that warrants us treating identity proofs like elements of a homotopy group, then I would like to know what that fact is - presumably, that's the fact that will justify the elimination rule in question. $\endgroup$ Feb 11 at 18:44
  • $\begingroup$ Depending on your tolerance for high-abstraction nonsense, you might take the analogy seriously because ML type theory is the internal language of $\infty$-topoi (see here). Since we also use $\infty$-topoi to model homotopy theory (see here), it makes sense that ML type theory would provide a natural syntax for reasoning about homotopy theory $\endgroup$ Feb 11 at 18:52
  • $\begingroup$ Thanks again. In general I'm fine with high-abstraction nonsense. But isn't there something funny about the fact that a question about the general rules for concrete verifications, and what concrete verifications can be produced concretely from other concrete verifications, should need to take detours through homotopy theory, topos theory, etc.? It's as if I have a problem with certain sorts of long division problems, and I'm being told something about higher category theory in reply, if you get my drift. $\endgroup$ Feb 11 at 19:05
  • $\begingroup$ That's a reasonable critique. I have an idea for a more concrete interpretation, but I'll write it up later today after I finish teaching. I will say that this machinery has existed for much longer than the homotopy-theoretic interpretation (since the early 70s, iirc, compared to the basics of HoTT, which started in the late 90s early 2000s, iirc) so people must have had a way to think about it without homotopy theory. $\endgroup$ Feb 11 at 20:41
  • $\begingroup$ @provocateur -- Ok, I got around to editing my answer $\endgroup$ Feb 12 at 1:11
5
$\begingroup$

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.

$\endgroup$
8
  • $\begingroup$ But the question is, why is $c$ as good as $r(a)$? $\endgroup$ Feb 11 at 18:02
  • $\begingroup$ @provocateur $c$ can be considered as good as $r(a)$ because it is already explicitly passed over, precisely. You would miss that if you didn't pass $c$. $\endgroup$ Feb 11 at 18:06
  • 1
    $\begingroup$ @OlivierRoche what does 'passed over' mean? $\endgroup$ Feb 11 at 18:13
  • $\begingroup$ @provocateur Sorry! I meant this : c can be considered as good as r(a) because it is already explicitly available, precisely. You would miss that if you didn't explicitly mention c. $\endgroup$ Feb 11 at 18:19
  • 2
    $\begingroup$ @provocateur Oh, I see! So in that paper Martin-Löf gives an $I$-elimination rule which lets you turn a propositional equality ($c:I(a,b)$) into a judgmental equality ($a = b$). In this case, I think you're right that the typing is ok. I think most modern ML type theories (in particular HoTT) do not include such a rule. $\endgroup$ Feb 11 at 19:47
4
$\begingroup$

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.

$\endgroup$
5
  • $\begingroup$ Thanks for this answer. Yes, I've seen the language of inductive types used to describe identity types. But it still seems weird to me. I get how all natural numbers can be generated from 0 and suc. But what exactly is the claim about identity proofs? They can all be generated from proofs of the form r(a) - how? I think a clear answer to that question would really settle things. $\endgroup$ Feb 11 at 18:37
  • $\begingroup$ Also, I'm curious about the 'other interpretations of what's underlying this inductive definition.' What did you have in mind? (The homotopy interpretation?) $\endgroup$ Feb 11 at 18:38
  • $\begingroup$ I don't know what reference you're reading, but the sort of 'standard model,' is that $r(a)$ is the only value of the identity type. So, if you have $c : I(A,a,b)$, it must have come from a context where someone knew that $a = b$ and they used $r(a)$ (or equivalently $r(b)$). Just like the standard explanation is that every ℕ must actually be built as a numeral. The famous alternate intrepretation is Homotopy Type Theory, where the same formal rule is saying that any proof for $r(a)$ can be continuously deformed into a proof for $c$. $\endgroup$
    – Dan Doel
    Feb 11 at 18:50
  • $\begingroup$ Dan, if $a$ and $b$ are distinct $\lambda$-terms which are nevertheless equal (e.g., they are $\beta$-equivalent), then I don't see how an element of $I(A,a,b)$ will have the form $r(a)$. Perhaps if I understood that, I would understand everything else. $\endgroup$ Feb 11 at 19:44
  • 3
    $\begingroup$ According to the 'standard' semantics, there just aren't any other elements for it to be. The only constructor of $I$ is $r$, so every value must be built out of it/reduce to it. If $a = b$, then the singular value must be built with $r$. If $a \neq b$, then there just are no values, and the 'every value ...' holds vacuously. It's just like every value of a Σ type being a pair, or there being no values of $⊥$, because there aren't any constructors. $\endgroup$
    – Dan Doel
    Feb 11 at 20:34
0
$\begingroup$

Upon reflecting on the very helpful comments here (especially those of AlexKruckman, OlivierRoche, HallaSurvivor and DanDoel), I wonder why the following doesn't get to the heart of the matter. This is too long for a comment, but I'd be interested in feedback. It is intended more in the spirit of a question than an answer; I'll select one of the other answers as the correct answer shortly.

In what follows, I'll use the standard notation of formulation rules, introduction rules, elimination rules, and equality (or computation) rules. (This terminology goes back to Martin-Lof.) Indeed, I'll largely be thinking of things from the point of view of Martin-Lof Type Theory (MLTT). Whether what follows also works from other points of view (e.g., HoTT) I don't know.

Consider first judgmental equalities - i.e., claims of the form $a=b: A$. For Martin-Lof, the idea behind $a=b:A$ is that $a$ and $b$ can be reduced to a common term (via $\beta \eta$ reduction.) Now, if $a$ and $b$ can be reduced to a common form in this way, then this can be proved with the equality rules. (The equality rules just give in effect the rules of $\beta$-reduction, and there is of course also a rule for $\eta$ reduction included in the equality rules.) Thus, using the fact that whenever $a:A$ we have $a=a:A$, it follows that if $a$ and $b$ can be reduced to a common term, then $a=b:A$ will be provable in MLTT. This is a type of decidability for true equality statements in MLTT.

Because of this, it suffices to only have elements of the form $r(c)$ occupying identity types $I(A,a,b)$. Why? Well, we can think of a proof of $a=b$ as a proof of $a=b:A$ via the equality (comptuation) rules in MLTT coupled with the canonical identity proof $r(a)$. Because the proof of $a=b:A$ already exists in our system, we can think of it as technically extrinsic to the element of $I(A,a,b)$ we are constructing, thinking of the proof of $a=b:A$ as just given by $r(a)$. (As an aside, it seems to me that it would suffice to only have elements of the form $r(c)$ occupying identity types where $c$ is already fully reduced, but that isn't the direction in which the treatment of identity in MLTT goes - perhaps it would make other things more complicated.)

The upshot of this is that we can think of $I(A,a,b)$ as in fact just consisting of $r(a)$. This then explains why we have:

\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}

The reason is that the $c$ in question can be nothing other than $r(a)$, and so really it is just an instance of the simpler principle:

\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}

I suppose my claim is what gets rid of the mystery here is the fact that if $a=b:A$, then $a$ and $b$ can be reduced to a common term, and so $a=b:A$ is provable in MLTT. Once one accepts that, the idea that $I(A,a,b)$ just consists of $r(a)$ makes sense, and the elimination rule for identity types is pretty straightforward.

But if this is what's going on, why have I never found a textbook or paper of any sort that puts the point this way?

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.