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!



Why the reflection rule trivializes higher paths in Martin-Löf Extensional Type theory?
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.


