Offline, Carlo Angiuli showed me that the difficulty was i= n part 1, because of a subtlety I had been forgetting.

S= ince types are *Kan* cubical=C2=A0sets, we need that the Kan operations agr= ee as well as the sets.
So part 1 could be thought of as (Glue [ = phi |-> equivRefl A ] A, compGlue) =3D (A, compA), and getting that the = Kan operations to agree was/is difficult.
(Now that I know what t= he answer is, it is clear that this was already explained in the initial di= scussion.)

Humbly,
- Jasper Hugunin

On Fri, Sep 13, 2019 at 2:10 AM Jasper Hugunin <jasperh@cs.washington.edu> wrote:
Hello all,<= div>
I've been trying to understand better why compo= sition for the universe does not satisfy regularity.
Since comp^i= [ phi |-> E ] A is defined as (roughly) Glue [ phi |-> equiv^i E ] A= , I would expect regularity to follow from two parts:
1. That Glu= e [ phi |-> equivRefl A ] A reduces to A (a sort of regularity condition= for the Glue type constructor itself)
2. That equiv^i (refl A) r= educes to equivRefl A
I'm curious as to which (or both) of th= ese parts was the issue, or if regularity for the universe was supposed to = follow from a different argument.

Context:
I've been studying and using CCHM cubical type theory recently,= and often finding myself wishing that J computed strictly.
If I = understand correctly, early implementations of ctt did have strict J for Pa= th types, and this was justified by a "regularity" condition on t= he composition operation, but as discussed in=C2=A0this thread on the HoTT mailing list, the definition of composit= ion for the universe was found to not satisfy regularity.
I don&#= 39;t remember seeing the regularity condition defined anywhere, but my unde= rstanding is that it requires that composition in a degenerate line of type= s, with the system of constraints giving the sides of the box also degenera= te in that direction, reduces to just the bottom of the box. This seems to = be closed under the usual type formers, plus Glue, but not the universe wit= h computation defined as in=C2=A0the CCHM paper=C2=A0(for trivial = reasons and non-trivial reasons; it gets stuck at the start with Glue [ phi= |-> equiv^i refl ] A not reducing to anything).

Best regards,
- Jasper Hugunin

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://g= roups.google.com/d/msgid/HomotopyTypeTheory/CAGTS-a9oS0CQDGKgj7ghCh8%2BZwAc= AefiTg4JJVHemV3HUPcPEg%40mail.gmail.com.
--00000000000069daeb05929129da--