Why is regularity a problem in cubical type theory? 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 &quot;normalizing the path, reduce to $a$ if $i \notin FV(A)$&quot;. 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!).
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 &quot;decidability of degeneracies&quot; 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 &amp; 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).