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