What's the difference between a computation rule and a definitional equality?

Question

In http://www.cse.chalmers.se/~coquand/comp.pdf, Coquand said:

One important point is that we cannot hope this computation rule to be interpreted as a definitional equality, since reflexivity is not considered to be an introduction rule/constructor anymore in the present approach.

I used to equate definitional equality as a relation generated by "computation rule + α equality + η equality", but now I see experts saying that a computation rule "cannot be hoped to be interpreted as a definitional equality". So, what kind of computation rules are not definitional equalities? This sounds very mysterious to me.

Answer 1

I think what Coquand means by "computation rule" is the fact that we have $\mathbf{J}(A,a,P,p,a',\mathbf{refl}(A,a,a)) \cong p$ for some notion of equality $\cong$, where $$(A : \Box), (a : A), (P : \Pi x : A, a =_A x \to \Box), (p : P\ a\ (\mathbb{refl}(A,a,a)), a' : A, u : a =_A a' \vdash \mathbf{J}(A,a,P,p,a',u) : P\ a'\ u$$ corresponding to the eliminator of the inductively defined identity type (the one of standard MLTT or HoTT).

In the case of the inductively defined identity type, this is just the usual β-rule, hence the use of "computation rule", and $\cong$ can be taken to be definitional equality.

But in cubical type theory , the status of $\mathbf{J}$ and $\mathbf{refl}$ changes, as they are no longer primitive notions. This implies that while we get other definitional equalities, $\cong$ in the first equation can only be taken to hold for propositional instead of definitional equality.

So I guess the confusion comes from the fact that what Coquand calls "computation rule", and which is indeed a computation rule for the inductively defined equality, is not a computation rule in the cubical setting any more, and thus cannot be incorporated into definitional equality.