10
$\begingroup$

In my current understanding, regularity in cubical type theory is the following definitional equality (I'm using $A~\textbf{type}$ to emphasize the fact that $i \notin FV(A)$):

$$ \cfrac{A~\textbf{type} \quad a:A} {\text{transport}(\langle i \rangle A, a) \mapsto a} $$

I am not sure how is transport specified here (does it have a standard formulation?). I just assume it to be a special case of transp in de Morgan cubical type theory and a special case of coe in Cartesian cubical type theory.

In Cubical Agda, this definitional equality doesn't hold. It's proved as transportRefl in the cubical library. I'm not sure how it works in Cartesian cubical type theory, but I guess it is also a long-standing problem (Jon Sterling said he solved it a while ago, but it's on Twitter, which is not a reliable source of academic information).

I don't quite get the difficulty -- it seems like a problem in the model. In Arend's type theory, regularity is a part of the definition of coe, and it's implemented as "normalizing the path, reduce to $a$ if $i \notin FV(A)$". Why can't we do this in cubical type theory? We already have eta laws for functions where we need FV checks, so this is not a problem implementation-wise (or is it? Please tell me!).

$\endgroup$
13
$\begingroup$

The difficulty is in making such a reduction compatible with all the other reductions involving transport/coe. From one perspective it is a “confluence” problem. It is unfortunate that in the community, so much was said about "decidability of degeneracies" that we began to give the impression that this was the hard part of the algorithm (since as you say, in syntax you can decide degeneracy)...

The real problem is competing reductions. If you have both the type-based reductions and the regularity rule, then the term Transport(P, a) can reduce in potentially many different ways. It is necessary to ensure that the type-based reductions satisfy the regularity law, then. The problem in cubical type theory was that the type-based reductions do not satisfy the regularity law (actually, most of them do satisfy it, but ones involving the glue type do not). So the difficulty with regularity was to find new versions of these type-based reductions that preserve regularity, and I personally believe this cannot be done without extending the language of cofibrations beyond what appears in the CCHM or ABCFHL papers. (If you add further cofibrations, it is trivial to correct the reductions for CCHM & ABCFHL --- but my ideas in this direction do not seem possible to implement.)

The reason that Arend doesn't seem to have this problem is that Arend doesn't support the other reductions... So in principle it is possible to have a sound type theory that supports the regularity reduction for paths by simply deleting the other reductions that might conflict with it (but I do not want to make a claim about Arend's soundness).

$\endgroup$
4
  • $\begingroup$ Does the problem also happen to XTT? IMO the reduction rules of $coe$ in XTT is simpler than full-blown CTT (no Glue) and maybe regularity could be easier $\endgroup$ – ice1000 May 17 at 0:16
  • $\begingroup$ Also, if it is proven to be confluent, why not implement the Arend approach? $\endgroup$ – ice1000 May 17 at 0:29
  • 1
    $\begingroup$ Arend doesn't have enough reductions to satisfy canonicity or normalization. $\endgroup$ – Mike Shulman May 17 at 3:17
  • $\begingroup$ I am aware of the problem, but IMO the already implemented rules still make sense $\endgroup$ – ice1000 May 17 at 5:55

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.