Why the reflection rule trivializes higher paths in Martin-Löf Extensional Type theory?

Question

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!

Answer 1

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.