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 "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!).

• 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 May 17 '21 at 0:16