Hi Dan,

Of course. I'm thinking pri=
marily of composition for Glue given in the CCHM paper you linked, reproduc=
ed below.

As you know, the single potential issue is that we need=
pres of a degenerate filling problem and function to be reflexivity. I cla=
im that this holds by regularity of composition in T and A, partly as a con=
sequence of the fact that regularity of composition implies regularity of f=
illing (that fill of a degenerate system is refl), which certainly holds fo=
r fill defined by connections (and I believe also holds for fill as defined=
in ABCFHL).

(a)

Given i |- B =3D Glue [=
phi |-> (T, f) ] A, with psi, i |- b : B and b0 : B(i0)[ psi |-> b(i=
0) ], 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=
9; :=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&=
#39;, omega), psi |-> (b(i1), refl=C2=A0a1') ] a1'

a1 =
:=3D hcomp^j A(i1) [ phi(i1) |-> alpha j, psi |-> a(i1) ] a1' (no=
te 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)[ psi |-> b(i0) ], we def=
ine

pres^i f [ psi |-> b ] b0 =3D <j> comp^i A [ psi |-&=
gt; f b, j =3D 1 |-> f (fill^i T [ psi |-> b ] b0) ] (f(i0) b0).

--

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-a_qUJdhOcQUznrY3JetHjQpCa= sCYHb1PR2hBPL0%2BMj1xg%40mail.gmail.com.

--000000000000be0d4f0592aea9bb--

(b)

Now consider the regular case, where phi=
, T, f, and A are independent of i. We want that b1 =3D b0.

We ha=
ve that a is independent of i, and delta =3D phi.

=
First consider delta (=3D phi) |- pres^i f [ psi |-> b ] b0. (This is th=
e explanation of your first dash)

Note that if comp^i A is regula=
r, 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 compositio=
n of Glue,

a1' =3D a0

phi |- t1' =3D b0b1 =3D glue [ phi |-> t1 ] a1 =3D glue [ phi |-> b0 ] a0 =3D glue [=
phi |-> b0 ] (unglue b0) =3D b0 (by eta, see Figure 4 in=C2=A0CCHM)

phi |- omega =3D refl=C2=A0(f b0)

phi |- (t1, alpha) =3D (=
t1', omega) (since delta =3D phi, so we end up in the delta face of equ=
iv)

a1 =3D a1' (the only dependence on j is via (alpha j), bu=
t alpha =3D omega =3D refl, so this filling problem is degenerate)

Thus this algorithm for composition of Glue is regula=
r.

Other algorithms, such as the one in ABCFHL, may not be, but I=
am prone to believe that there exist regular algorithms in other settings =
including Orton-Pitts and Cartesian cubes.

Best re=
gards,

- Jasper Hugunin

On Mon, Sep 16, 2019 at 12:18 PM Lic=
ata, 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 poss= ible variations), and (b) include some of your reasoning for why you think = things are regular, to make it easier for me and others to reconstruct.=C2= =A0

My current understanding is that

- For CCHM proper https://arxiv.org/pdf/1611.02108.pdf the p= otential 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 degenerat= e even if the input is.=C2=A0 Do you think this does work out to be degener= ate?=C2=A0

- For the current version of ABCFHL https://github.com/dlicata335/cart-cube/blob/master/cart-cube.pdf whic= h uses aligning =E2=80=9Call the way at the outside=E2=80=9D, an issue is w= ith the adjust_com operation on page 20, which is later used for aligning (= in that case beta is (forall i phi)).=C2=A0 The potential issue is that adj= ust_com uses a *filler*, not just a composition from 0 to 1, so even if t d= oesn=E2=80=99t depend on z, the filling does, and the outer com won=E2=80= =99t cancel.=C2=A0 In CCHM, filling is defined using connections, 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 should come up because of the c= onnection term that is substituted into the type of the composition problem= .=C2=A0 So I=E2=80=99d guess there is still a problem in the aligned algori= thm for CCHM.=C2=A0

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

-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 Glu= e types 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<= br> > where regularity for comp for Glue types break down. In this step we> do an additional comp/hcomp that inserts an additional forall i. phihttps://arxiv.org/abs/1808.00920v3) shows t= hat this is> 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 (

> not even possible!

>

> Another approach would be to have weak Glue types that don't stric= tly

> 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 n= ew

> 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 = issue, or if regularity for the universe was supposed to follow from a diff= erent argument.

> >>

> >> Context:

> >> I've been studying and using CCHM cubical type theory rec= ently, 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 = anywhere, but my understanding is that it requires that composition in a de= generate 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 th= e box. This seems to be closed under the usual type formers, plus Glue, but= not the universe with computation defined as in the CCHM paper (for trivia= l reasons and non-trivial reasons; it gets stuck at the start with Glue [ p= hi |-> 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 HomotopyTypeTheory+unsubscribe@googlegroups.c= om.

> > To view this discussion on the web visit h= ttps://groups.google.com/d/msgid/HomotopyTypeTheory/CAGTS-a9oS0CQDGKgj7ghCh= 8%2BZwAcAefiTg4JJVHemV3HUPcPEg%40mail.gmail.com.

>

> --

> You received this message because you are subscribed to the Google Gro= ups "Homotopy Type Theory" group.

> To unsubscribe from this group and stop receiving emails from it, send= an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.

> To view this discussion on the web visit https:= //groups.google.com/d/msgid/HomotopyTypeTheory/CAGTS-a8SZx8PiaD-9rq5QWffU75= Wz8myrXD1g5P3DCjSO%3DfvOQ%40mail.gmail.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-a_qUJdhOcQUznrY3JetHjQpCa= sCYHb1PR2hBPL0%2BMj1xg%40mail.gmail.com.

--000000000000be0d4f0592aea9bb--