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.