In cubical type theory, can we insist that "constant" compositions are the identity?

Question

$\DeclareMathOperator{\comp}{comp}\DeclareMathOperator{\refl}{refl}\DeclareMathOperator{\transp}{transp}$I've been reading about Cubical Type Theory and playing around with the Agda implementation of it*. I'm wondering about whether one can add an additional equality judgement to composition operations that states that compositions over a constant system act like the identity (judgementally).

It seems to me that if we have a type $A$ and a system $[\varphi \mapsto u]$ which do not reference the variable $i$, we should be able to add the equality judgement $$\comp^iA\,[\varphi \rightarrow u]\,a_0=a_0$$ to cubical type theory without sacrificing the nice properties of the system (in particular: I think the system would still be strongly normalizing). This is certainly true propositionally and, far as I can tell, if all the terms here are closed, the left hand side will eventually compute to the right hand side using the existing equality judgements.

From my novice perspective, it seems like such a rule might be useful to giving path types computational behavior more like the identity types in Martin-Löf type theory - and I can't see any trouble with such a rule (even if it doesn't agree with the topological intuition for what $\comp$ does), but perhaps something does go wrong; I note that the CCHM paper lists as an open problem:

4. Is there a model where Path and Id coincide?

which (I think?) is referring to semantics rather than syntax - but which at least suggests that there's something non-trivial in adding the proposed judgement.

Is it consistent to add this judgement to cubical type theory? Are there any papers that discuss adding such a judgement to cubical type theory?

---

*In practical terms, this question arises from curiosity about Agda's inspect idiom - and the issue that using this idiom seems to lead to an abundance of transport operations that will only ever be evaluated on constant paths. In practice, it seems like one can often avoid this by either using the $\transp$ operation or inductively defining certain auxiliary functions to avoid dealing with paths at all - but I'm wondering whether a more mechanistic approach would work. There also might be added bonuses like having the based path inductor $J$ defined here satisfying $J\,P\,x\,\refl = x$ definitionally.

Answer 1

That is regularity. It is consistent, via a non constructive proof, for example taking an Orton-Pitts model (from Orton, Pitts, Axioms for Modelling Cubical Type Theory in a Topos) where cofibrations are all locally decidable monomorphisms. Using the law of excluded middle, every monomorphism is locally decidable, which implies that path types are identity types.

The paper that Mike Shulman mentioned, Swan Separating Path and Identity Types in Presheaf Model of Univalent Type Theory is about the difficulties constructing a model where this holds in constructive mathematics and certain realizability models. This suggests there might be some kind of issue with showing this type theory has "good computational properties" such as canonicity or even better strong normalisation. These properties are known now for cubical type theory (see e.g. Huber Canonicity for Cubical Type Theory or more recently Angiuli, Sterling, Normalization for Cubical Type Theory), but as far as I know so far none of them are known to apply to cubical type theory with regularity.