3
$\begingroup$

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.

$\endgroup$

1 Answer 1

1
$\begingroup$

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.

$\endgroup$
2
  • 2
    $\begingroup$ I think this is not the complete story, because the paper also says that the computation rule is interpreted judgmentally. It seems to be written prior to the problems with regularity being noticed. So, the paper is making a distinction between "judgmental" and "definitional" equality for the computation rule. I'm not sure this is a universally/widely recognized distinction, though. $\endgroup$
    – Dan Doel
    Jul 12, 2022 at 20:49
  • $\begingroup$ @DanDoel yes, it is written prior to the problems with regularity being noticed. $\endgroup$
    – ice1000
    Jul 13, 2022 at 18:24

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.