Martin-Löf Extensional Type theory differs from its intensional counterpart in that it contains the so-called reflection rule that says that if $p : x = y$, then actually $x \equiv y$ (i.e. $x$ and $y$ are definitionally or judgementally equivalent). Its known that this causes strong normalization to fail and type-checking to be undecidable.

More to the point, it is known that it also trivializes higher paths in a type in the sense that for any $p, q: x = y$, $p \equiv q$. I wonder why is this so?

I heard this is because it implies that for any $p : x = x$, $p \equiv refl_x$. But I can't see why this is true. As far I can see, given any such $p$ the reflection rule only implies that $x \equiv x$, which is true anyway, since each term is definitionally equal to itself - with or without the rule. So how come we conclude that $p \equiv refl_x$? What am I missing?



The point is that the reflection rule makes $p = \mathsf{refl}_x$ a well-formed expression. This turns out to be incredibly dangerous: now we can prove it by induction on equality.

More precisely:

  1. In a context where $x$ and $y$ are variables of the same type $T$ and $p$ is a variable of type $x = y$, we have $x \equiv y$, so $p$ is also a variable of type $x = x$, and therefore $p = \mathsf{refl}_x$ is well formed.
  2. Thus $\prod_{x : T} \prod_{y : T} \prod_{p : x = y} p = \mathsf{refl}_x$ is also well formed.
  3. By induction on equality, we have: $$\left( \prod_{x : T} \mathsf{refl}_x = \mathsf{refl}_x \right) \to \left( \prod_{x : T} \prod_{y : T} \prod_{p : x = y} p = \mathsf{refl}_x \right)$$

Of course, we have $\mathsf{refl}_{\mathsf{refl}_x} : \mathsf{refl}_x = \mathsf{refl}_x$, so the claim follows.

  • 3
    $\begingroup$ It would be nice to find an early reference! The best I can find is Hofmann’s PhD thesis Extensional concepts in intensional type theory, which doesn’t state it explicitly anywhere (at least, not that I see on a quick skim), but uses it in the definition of the stripping map on p.91. (There he simply gives the proof term Refl(Refl(m)) for it; the unhelpfulness of this is a possibly-deliberate illustration of the undecidability of ETT.) I guess it goes back further, at least to Streicher’s Habilitationthesis, but my copy of that isn’t searchable, and on a quick skim, I’m coming up empty. $\endgroup$ – Peter LeFanu Lumsdaine Feb 2 '16 at 21:04

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

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