MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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?

Thanks!

share|cite|improve this question
up vote 14 down vote accepted

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.

share|cite|improve this answer
3  
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. – Peter LeFanu Lumsdaine Feb 2 at 21:04

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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