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

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!

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.

• 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 '16 at 21:04