In CCHM, my understanding is that composition for Glu=
e [ phi |-> (T, f) ] A is actually regular, and reduces to composition i=
n T on (forall=C2=A0i. phi), assuming composition is regular for A and T.

The regularity does seem to fail in ABCFHL, as you pointed out=
Anders, but is perhaps repairable.

What Carlo tol=
d me was that the problem is getting composition for Glue [ phi |-> (T, =
f) ] A which is regular, reduces to composition in T on (forall i. phi), *a=
nd* reduces to composition in A when (T, f) =3D (A, equivRefl).

W=
e get the first two but not the third in CCHM.

The=
problem as Carlo explained it was that given a square of types i, j |- A a=
nd a point a : A (i0) (j0), we can prove Path (coe^i A o coe^j A) (coe^j A =
o coe^i A) (coercing around the square in right then up vs up then right), =
and (assuming regularity for A), we can take this to be degenerate when A i=
s degenerate=C2=A0in i, or give a different path which is degenerate when A=
is degenerate in j, but constructing a path which is degenerate when A is =
degenerate in i or j is elusive.

I have an idea fo=
r how to add new terms/operations (a sort of generalization of comp)=C2=A0s=
uch that such a path is constructible, but I haven't yet checked that t=
here is a univalent universe with these more general operations.

=
I also don't understand the negative results from Andrew well=C2=A0enou=
gh to tell if they rule out such an approach.

The =
idea is to add terms witnessing that for every square x, y |- A x y=C2=A0we=
have Path (coe^i (A i i)) ((coe^i (A i 0)) o (coe^i (A 1 i))) which is deg=
enerate when A is degenerate in x OR y, plus similar terms for higher cubes=
, since once you need dimensions one and two you probably need dimension n,=
and a similar thing for hcomp, or you can do coe and hcomp together in jus=
t comp.

Composing two of these paths then gives the needed proof =
that coercing around the square either way is equal, in a degenerate fashio=
n if A is degenerate in x or y.

=C2=A0

Best regards=
,

- Jasper Hugunin

On Sun, Sep 15, 2019 at 7:55 AM Andrew Sw=
an <wakelin.swan@gmail.com=
> wrote:

--You might have already seen this, but I have a paper on some r= elated issues at=C2=A0https://arxiv.org/abs/1808.00920 . In that paper I didn'= ;t look at the original version of regularity, but a more recent version (&= quot;all monomorphisms are cofibrations")=C2=A0that fits better with t= he general framework of Orton and Pitts. In that case it is definitely equa= lity of objects that causes problems.Best,An= drew--

On Friday, 13 September 2019 08:10:42 UTC+2, Jasper Hugunin wr= ote:Hell= o all,I've been trying to understand better wh= y composition 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. T= hat Glue [ phi |-> equivRefl A ] A reduces to A (a sort of regularity co= ndition for the Glue type constructor itself)2. That equiv^i (re= fl A) reduces to equivRefl AI'm curious as to which (or both= ) of these parts was the issue, or if regularity for the universe was suppo= sed to follow from a different argument.Context:<= /div>I've been studying and using CCHM cubical type theory re= cently, and often finding myself wishing that J computed strictly.If I understand correctly, early implementations of ctt did have strict J= for Path types, and this was justified by a "regularity" conditi= on on the composition operation, but as discussed in=C2=A0this thread on the HoTT mailing list, t= he definition of composition for the universe was found to not satisfy regu= larity. I don't remember seeing the regularity condition defi= ned anywhere, but my understanding is that it requires that composition in = a degenerate line of types, with the system of constraints giving the sides= of the box also degenerate in that direction, reduces to just the bottom o= f the box. This seems to be closed under the usual type formers, plus Glue,= but not the universe with 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 redu= cing 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 ht= tps://groups.google.com/d/msgid/HomotopyTypeTheory/16b3b92f-069b-468c-94f8-= f3859e152338%40googlegroups.com.

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-a9XATMbfyyp00M8kqiEoFyj7X= sxahMa3AdzXth_%3DLbTiA%40mail.gmail.com.

--00000000000052080b05929f26e3--