What I was saying about fill for the aligning algorithm is also wrong = =E2=80=94 I wasn=E2=80=99t thinking that the type of the filling was also d= egenerate, but of course it is here. So that might work too.

However, even if there can be a universe of regular types that is clos= ed under glue types, there=E2=80=99s still a problem with using those glue = types to show that that universe is itself regularly fibrant, I think? If y= ou define comp U [phi -> i.T] B to be Glue [phi -> T(1),...] B then no matter how nice the equivalence is (eg the = identity) when i doesn=E2=80=99t occur in T, the type will not equal B =E2= =80=94 that would be an extra equation about the Glue type constructor itse= lf. Does that seem right?

-Dan

On Sep 16, 2019, at 1:09 PM, Jasper Hugunin <jasperh@cs.washington.edu> wrote:

Hi Dan,

Of course. I'm thinking primarily of composition for Glue given in the= CCHM paper you linked, reproduced below.
As you know, the single potential issue is that we need pres of a dege= nerate filling problem and function to be reflexivity. I claim that this ho= lds by regularity of composition in T and A, partly as a consequence of the= fact that regularity of composition implies regularity of filling (that fill of a degenerate system is refl), = which certainly holds for fill defined by connections (and I believe also h= olds for fill as defined in ABCFHL).

(a)
Given i |- B =3D Glue [ phi |-> (T, f) ] A, with psi, i |- b : B an= d b0 : B(i0)[ psi |-> b(i0) ], we want to compute b1 =3D comp^i B [ psi = |-> b ] b0 : B(i1)[ psi |-> b(i1) ].
We set a :=3D unglue b and a0 :=3D unglue b0.
Set delta :=3D forall i. phi.
Then we take:
a1' :=3D comp^i A [ psi |-> a ] a0
delta |- t1' :=3D comp^i T [ psi |-> b ] b0
delta |- omega :=3D pres^i f [ psi |-> b ] b0
phi(i1) |- (t, alpha) :=3D equiv f(i1) [ delta |-> (t1', omega), ps= i |-> (b(i1), refl a1') ] a1'
a1 :=3D hcomp^j A(i1) [ phi(i1) |-> alpha j, psi |-> a(i1) ] a1'= (note that in the regular setting the psi face is redundant)
b1 :=3D glue [ phi(i1) |-> t1 ] a1

With given i |- f : T -> A, with psi, i |- b : T and b0 : T(i0)[ ps= i |-> b(i0) ], we define
pres^i f [ psi |-> b ] b0 =3D <j> comp^i A [ psi |-> f b, = j =3D 1 |-> f (fill^i T [ psi |-> b ] b0) ] (f(i0) b0).

(b)
Now consider the regular case, where phi, T, f, and A are independent = of i. We want that b1 =3D b0.
We have that a is independent of i, and delta =3D phi.

First consider delta (=3D phi) |- pres^i f [ psi |-> b ] b0. (This = is the explanation of your first dash)
Note that if comp^i A is regular, then fill^i A [ psi |-> b ] b0 = =3D b
This is <j> comp^i A [ psi |-> f b, j =3D 1 |-> f (fill^i = T [ psi |-> t ] t0) ] (f t0) =3D <j> comp^i A [ psi |-> f b, j = =3D 1 |-> f t0 ] (f t0) =3D <j> f t0.
Thus pres of a degenerate filling problem and function is reflexivity.=

Going back to composition of Glue,
a1' =3D a0
phi |- t1' =3D b0
phi |- omega =3D refl (f b0)
phi |- (t1, alpha) =3D (t1', omega) (since delta =3D phi, so we end up= in the delta face of equiv)
a1 =3D a1' (the only dependence on j is via (alpha j), but alpha =3D o= mega =3D refl, so this filling problem is degenerate)
b1 =3D glue [ phi |-> t1 ] a1 =3D glue [ phi |-> b0 ] a0 =3D glu= e [ phi |-> b0 ] (unglue b0) =3D b0 (by eta, see Figure 4 in CCHM)<= /div>

Thus this algorithm for composition of Glue is regular.
Other algorithms, such as the one in ABCFHL, may not be, but I am pron= e to believe that there exist regular algorithms in other settings includin= g Orton-Pitts and Cartesian cubes.

Best regards,
- Jasper Hugunin

On Mon, Sep 16, 2019 at 12:18 PM Lica= ta, Dan <dlicata@wesleyan.edu> wrote:
Hi Jasper,

It would help me follow the discussion if you could say a little more about= (a) which version of composition for Glue exactly you mean (because there = is at least the one in the CCHM paper and the =E2=80=9Caligned=E2=80=9D one= from Orton-Pitts, which are intensionally different, as well as other possible variations), and (b) include some of your reason= ing for why you think things are regular, to make it easier for me and othe= rs to reconstruct.

My current understanding is that

- For CCHM proper
https://arxiv.org/pdf/1611.02108.pdf the potential issue is with the = =E2=80=98pres=E2=80=99 path omega, which via the equiv operation ends up in= alpha, so the system in a1 may not be degenerate even if the input is.&nbs= p; Do you think this does work out to be degenerate?

- For the current version of ABCFHL https://github.com/dlicata335/cart-cube/blob/master/cart-cube.pdf which= uses aligning =E2=80=9Call the way at the outside=E2=80=9D, an issue is wi= th the adjust_com operation on page 20, which is later used for aligning (i= n that case beta is (forall i phi)).  The potential issue is that adjust_com uses a *filler*, not just a composition from 0 to= 1, so even if t doesn=E2=80=99t depend on z, the filling does, and the out= er com won=E2=80=99t cancel.  In CCHM, filling is defined using connec= tions, so it=E2=80=99s a little different, but I think there still has to be a dependence on z for it to even type check =E2=80=94 it s= hould come up because of the connection term that is substituted into the t= ype of the composition problem.  So I=E2=80=99d guess there is still a= problem in the aligned algorithm for CCHM.

However, it would be great if this is wrong and something does work!  =

-Dan

> On Sep 15, 2019, at 10:18 PM, Jasper Hugunin <jasperh@cs.washington.edu>= wrote:
>
> This doesn't seem right; as far as I can tell, composition for Glue ty= pes in CCHM preserves regularity and reduces to composition in A on phi. >
> - Jasper Hugunin
>
> On Sun, Sep 15, 2019 at 3:28 AM Anders Mortberg <anders.mortberg@math.su.se> wrote:
> Hi Jasper,
>
> Indeed, the problem is to construct an algorithm for comp (or even
> coe/transp) for Glue that reduces to the one of A when phi is true
> while still preserving regularity. It was pointed out independently by=
> Sattler and Orton around 2016 that one can factor out this step in our=
> algorithm in a separate lemma that is now called "alignment"= . This is
> Thm 6.13 in Orton-Pitts and discussed in a paragraph in the end of
> section 2.11 of ABCFHL. Unless I'm misremembering this is exactly
> where regularity for comp for Glue types break down. In this step we > do an additional comp/hcomp that inserts an additional forall i. phi > face making the comp/coe irregular.
>
> One could imagine there being a way to modify the algorithm to avoid > this, maybe by inlining the alignment step... But despite considerable=
> efforts no one has been able to figure this out and I think Swan's
> recent paper (
https://arxiv.org/abs/1808.00920v3) shows t= hat this is
> not even possible!
>
> Another approach would be to have weak Glue types that don't strictly<= br> > reduce to A when phi is true, but this causes problems for the
> composition in the universe and would be weird for cubical type
> theory...
>
> In light of Swan's negative results I think we need a completely new > approach if we ever hope to solve this problem. Luckily for you Andrew=
> Swan is starting as a postdoc over in Baker Hall in October, so he can=
> explain his counterexamples to you in person.
>
> Best,
> Anders
>
> On Sun, Sep 15, 2019 at 7:57 AM Jasper Hugunin
> <jas= perh@cs.washington.edu> wrote:
> >
> > Offline, Carlo Angiuli showed me that the difficulty was in part = 1, because of a subtlety I had been forgetting.
> >
> > Since types are *Kan* cubical sets, we need that the Kan operatio= ns agree 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 the answer is, it is clear that this was al= ready explained in the initial discussion.)
> >
> > Humbly,
> > - Jasper Hugunin
> >
> > On Fri, Sep 13, 2019 at 2:10 AM Jasper Hugunin <jasperh@cs.washington.edu<= /a>> wrote:
> >>
> >> Hello all,
> >>
> >> I've been trying to understand better why 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 pa= rts:
> >> 1. That Glue [ phi |-> equivRefl A ] A reduces to A (a sor= t of regularity condition for the Glue type constructor itself)
> >> 2. That equiv^i (refl A) reduces to equivRefl A
> >> I'm curious as to which (or both) of these parts was the issu= e, or if regularity for the universe was supposed to follow from a differen= t argument.
> >>
> >> Context:
> >> I've been studying and using CCHM cubical type theory recentl= y, and often finding myself wishing that J computed strictly.
> >> If I understand correctly, early implementations of ctt did h= ave strict J for Path types, and this was justified by a "regularity&q= uot; condition on the composition operation, but as discussed in this threa= d on the HoTT mailing list, the definition of composition for the universe was found to not satisfy regularity.
> >> I don't remember seeing the regularity condition defined anyw= here, but my understanding is that it requires that composition in a degene= rate line of types, with the system of constraints giving the sides of the = box also degenerate in that direction, reduces to just the bottom of the box. This seems to be closed under the usual typ= e formers, plus Glue, but not the universe with computation defined as in t= he CCHM paper (for trivial reasons and non-trivial reasons; it gets stuck a= t 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 Googl= e Groups "Homotopy Type Theory" group.
> > To unsubscribe from this group and stop receiving emails from it,= send an email to