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

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.)
• 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, 2021 at 0:16