Definition of extensional and propositional equality in Martin-Lof extensional type theory

Question

Martin Hofmann states in Extensional Concepts in Intensional Type Theory (§1.1 p.[4-5]) that:

A similar situation occurs in extensional Martin-Lof type theory where propositional and definitional equality are forcefully identified by the equality reflection rule

$\frac{\Gamma \vdash P:Id_\sigma(M,N)}{\Gamma \vdash M=N: \sigma}\text{(Id-DefEq)}$

Does the above mean that we purposefully drop the proof that M and N are equal and just consider them to be equal definitionally (like a presumption)?

Then it goes on and says:

This rule makes definitional equality extensional and undecidable.

How does it become extensional and what does it mean by becoming extensional in the first place?

And then it states:

Moreover, type checking becomes undecidable because $Refl(M):Id_\sigma (M,N)$ holds iff $M$ and $N$ are definitionally equal.

Why would $Refl(M)$ hold only if $M$ and $N$ are definitionally equal? And why would it make it undecidable?

Answer 1

what does it mean by becoming extensional in the first place?

The axiom of extensionality relates to what it means for two functions to be equal. Specifically, extensionality says:

• $f = g \iff \forall x \ldotp f(x) = g(x)$

That is, functions are equal if they map equal inputs to equal outputs. By this definition, quicksort and mergesort are equal, even if they don't have the same implementations, because they behave the same as functions.

How does it become extensional

What's missing is the rule of definitional equality for functions. It usually looks like this:

$\frac{\Gamma, (x : U) \vdash (f x) = (g x):V}{\Gamma \vdash f = g: (x : U) \to V}\text{(Fun-DefEq)}$

That is, two functions are definitionally equal when they produce equal results when applied to an abstract variable. This is similar in spirit to the way we typecheck polymorphic functions: you make sure it holds for all values by making sure it holds for an abstract value.

We get extensionality when we combine the two: if two functions always produce the same result, we should be able to find some equality proof $P$ such that $\Gamma,(x: U) \vdash P:Id_V(f x, g x)$ i.e. the proof that the two functions always produce the same result. But, if we combine this with the rule $\text{(Id-DefEq)}$, then any time two functions are extensionally equal (i.e. we can find the proof term $P$, then they are also definitionally equal.

This is in stark contrast to an intensional system, where two functions are equal if and only if their bodies are syntactically identical. So mergesort and quicksort are intensionally different, but extensionally the same.

The $\text{(Id-DefEq)}$ means that extensional equality is baked into the type system: if you have a type constructor $T : ((x : U) \to V) \to \mathsf{Set}$, then you can use a value of type $T\ f$ in a context expecting $T\ g$ if $f$ and $g$ map equal inputs to equal outputs. Again this is not true in an intensional system, where $f$ and $g$ might be incompatible if they're syntactically different.

Does the above mean that we purposefully drop the proof that M and N are equal and just consider them to be equal definitionally (like a presumption)?

It's even a bit stronger than that. It's saying that $M$ and $N$ are definitionally equal any time there exists some proof that they are propositionally equal. So on the one hand, if you have a propositional proof that two values are equal, you can forget that proof and say that they are definitionally equal. But on the other hand, if you are trying to prove that two values are definitionally equal (as a dependent type checking algorithm would), then you cannot say that they are not equal unless you are certain that no proof $P$ exists. This is why it is undecidable.