Why is regularity a problem in cubical type theory?
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).