Mdthbs

Martin Hofmann states in Extensional Concepts in Intensional Type Theory (§1.1 p.3) that:

It is important that definition equality is pervasive so if M and N are definitionally equal then P(M) is definitionally equal to P(N) whatever P is. In particular the proposition stating that M is propositionally equal to N is definitionally equal to the proposition that M is propositionally equal to itself.

What I don't get is how a proposition about equality of M and N propositionally can be definitionally equal to the proposition about propositional equality of M and M ?

Recall that (a few paragraphs above)

two objects are definitionally equal if after certain computation steps they evaluate
to identical results.

Assume throughout this post that $M$ and $N$ are definitionally equal. This means that there is a series of computation steps $M_0 leftrightarrow M_1 leftrightarrow ldots leftrightarrow M_n$ where I use $leftrightarrow$ do denote a computation step, and $M_0$ is the term $M$ and $M_n$ is the term $N$.

Any computation step can be applied in any context. This is part of the definition of computation rules for calculi used in logic (as opposed to calculi used to model programming languages with side effects). So if you stick $M_0$ in some context $P$, there is a series of computation steps $P(M_0) leftrightarrow P(M_1) leftrightarrow ldots leftrightarrow P(M_n)$. This means that $P(M_0)$ and $P(M_n)$ are definitionally equal, i.e. $P(M)$ and $P(N)$ are definitionally equal.

Apply this to a property $P(X)$ that expresses “$M$ is propositionally equal to $X$”, no matter how this is expressed in a particular calculus. $P(M)$ is definitionally equal to $P(N)$, i.e. a property that expresses “$M$ is propositionally equal to $M$” is definitionally equal to “$M$ is propositionally equal to $N$”.

Strictly speaking, there isn't necessarily a single proposition stating that $M$ is propositionally equal to $N$ — there may be ways to state this that are not definitionally equal (it depends on the exact calculus. If a calculus has multiple ways to express this, there can be two (or more) non-definitionally-equal propositions stating that $M$ is equal to itself, and then there are also multiple non-definitionally-equal propositions stating that $M$ is equal to $N$. But for each proposition stating that $M$ is equal to itself, that proposition is definitionally equal to a proposition stating that $M$ is equal to $N$, by applying the computation steps that rewrite $M$ to $N$.

Reasoning about equality can be difficult to follow. We tend to have an intuition that equality is just equality, dammit. It's a bit difficult to internalize that there are different concepts of equality, and worse, they coexist in the same theory. I think it helps if you use words other than “equality”. If two terms are written exactly in the same way (as strings or at least as abstract syntax trees), they're identical. As long as you're not reasoning about variable binding, you can extend that to terms that are identical except for variable names, i.e. terms that are alpha-equivalent. Beyond that, don't use the word “equal”. If there's a series of computation steps that leads from $M$ to $N$, say that $M$ and $N$ are computationally equivalent or rewritable to each other. They're not necessarily “equal”, but they're equivalent for a certain equivalence relation. Then it's obvious and not particularly confusing that there can be coarser equivalences between terms. For example, there's an equivalence relation between terms defined by “if you replace $M$ by $N$ in a true proposition, you get a proposition that's still true”. This is a form of observational or extensional equivalence of propositions. It can be called “observational equality” or “propositional equality”, but to form an intuition, don't call it that. And then it's not so shocking that if $N$ can be rewritten to $M$, then any proposition stating that $M$ is whatever-equivalent to $N$ can be rewritten to a proposition that states that $M$ is equivalent to itself.