<p>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 <em>can</em> decide degeneracy)...</p>
<p>The real problem is competing reductions. If you have both the type-based reductions <em>and</em> the regularity rule, then the term <code>Transport(P, a)</code> 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.)</p>
<p>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).</p>

CC BY-SA 4.0
2021-05-17T00:16:05.530Z
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
ice1000
CC BY-SA 4.0
2021-05-17T03:17:08.867Z
Arend doesn't have enough reductions to satisfy canonicity or normalization.
Mike Shulman
CC BY-SA 4.0
2023-08-04T20:20:37.413Z
Could you please provide source for this "regularity law" problem definition? Is this question related? https://mathoverflow.net/a/393906/5203
uhbif19
CC BY-SA 4.0
2021-05-15T11:13:16.127Z
2021-05-15T11:18:18.547Z
2021-05-15T11:18:18.547Z
Jonathan Sterling
<p>In my current understanding, regularity in cubical type theory is the following definitional equality (I'm using <span class="math-container">$A~\textbf{type}$</span> to emphasize the fact that <span class="math-container">$i \notin FV(A)$</span>):</p>
<p><span class="math-container">$$
\cfrac{A~\textbf{type} \quad a:A}
{\text{transport}(\langle i \rangle A, a) \mapsto a}
$$</span></p>
<p>I am not sure how is <code>transport</code> specified here (does it have a standard formulation?). I just assume it to be a special case of <code>transp</code> in de Morgan cubical type theory and a special case of <code>coe</code> in Cartesian cubical type theory.</p>
<p>In Cubical Agda, this definitional equality doesn't hold. It's proved as <code>transportRefl</code> 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).</p>
<p>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 <code>coe</code>, and it's implemented as &quot;normalizing the path, reduce to <span class="math-container">$a$</span> if <span class="math-container">$i \notin FV(A)$</span>&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!).</p>

<type-theory><homotopy-type-theory>
Why is regularity a problem in cubical type theory?
ice1000
# Why is regularity a problem in cubical type theory?

(Asked by: username_0 on 2021-05-15)

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

**Tags:** type-theory, homotopy-type-theory


---

## 1 answers

### Answer by username_1 on 2021-05-15. Score: 16 | Accepted answer

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

> **Comments:**
> **username_0**: 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  
> **username_2**: Arend doesn't have enough reductions to satisfy canonicity or normalization.  
> **username_3**: Could you please provide source for this "regularity law" problem definition? Is this question related? https://mathoverflow.net/a/393906/5203  

---

