I agree with the problem of using Glue types for the compo=
sition operation in the universe.

--

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://gro= ups.google.com/d/msgid/HomotopyTypeTheory/CAGTS-a8E03C3BMEwi-T4qjet4EbCgneP= hR3Ffa1MepxNmtZoUA%40mail.gmail.com.

--0000000000004483a40592b14a31--

You could imagine an extra equation t=
hat Glue [ phi |-> (A, reflEquiv) ] A =3D A, but this is somehow unnatur=
al.

However, it is what I was postulating in step 1 of the initia=
l message of this thread.

(You then need comp Glue to respect thi=
s equation, which appears impossible.)

The way to get ar=
ound it is, in my opinion, to add a separate type former Box^i [ phi |->=
T ] A for phi |- A =3D T(i1), satisfying the laws phi |- Box^i [ phi |->=
; T ] A =3D T(i0) and regularity: Box^i [ phi |-> A ] A =3D A.

You then need comp Box to respect Box^i [ phi |-> A ] A =3D A, an=
d this is also apparently not possible in CCHM, but you now have the extra =
information that A is a line of types. (Using Box to turn an equivalence in=
to a line of types in the definition of comp Box is circular.)

I've developed a notion of (regular) n-dimensional composi=
tion, which I think might suffice to complete the argument.

If yo=
u call a notion of Box that satisfies Box^i [ phi |-> A ] A =3D A "=
regular Box's", then the problem can be reduced to saying that to =
give regular 1-dimensional composition of regular 1-dimensional boxes, you =
need some sort of "(doubly) regular 2-dimensional composition" fo=
r A, and in CCHM such we can only get this "2-dimensional composition&=
quot; which is regular in one direction or the other.

Of course (=
I haven't actually checked, but my intuition says that), once you have =
2-dimensional composition you will need n-dimensional composition, and then=
hopefully regular (n+m)-dimensional composition for A will suffice to defi=
ne regular n-dimensional composition of regular n-dimensional Box's.

<=
div>(I will write (i o j) for composition over j then over i, and (i =3D j)=
for composition over the diagonal (i =3D j). Then we want a path from (i o=
j) to (j o i) which is degenerate if T is degenerate in i OR j.

Below I'll put an explanation of my idea of regu=
lar n-dimensional composition (returning an (n-1)-dimensional cube), since =
it feels unfair to say "I know how to do this" and hide "how=
to do this".

Unfortunately, it is quite complex; read at yo=
ur own peril.

I don't yet know how to intellig=
ibly=C2=A0describe n-dimensional composition for Glue and Box.

Fo=
r now I'll just say that they should be essentially the same as in the =
1-dimensional case, but with extra faces in the equiv and final hcomp steps=
corresponding to faces in the result.

=3D=3D=3D=
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D

In CCHM,=
the basic Kan operation is (comp^i A [ phi |-> a ] a0 : A(i1) [ phi |-&=
gt; a(i1) ]) for i |- A with phi, i |- a : A and a0 : A(i0) [ phi |-> a(=
i0) ].

Regularity for this operation means that if A and a ar=
e independent of i, then comp^i A [ phi |-> a ] a0 =3D a0.

We =
have regular composition for Glue types, but we don't have comp^i (Glue=
[ phi |-> (A, equivRefl) ] A) =3D comp^i A.

Simplifying thing=
s a little, we can take hcom^i U [ phi |-> T ] A =3D Box^i [ phi |-> =
T(i :=3D ~ i) ] A to be a new type former, and give that a regular composit=
ion=C2=A0operation.

Here the thing blocking us from getting comp^=
i (Box^j [ phi |-> A ] A) =3D comp^i A is that, given=C2=A0i, j |- T wit=
h phi, i, j |- t : T and t0 : T(i0)(j0)[ phi |-> t(i0)(j0) ],

=
we need a Path T(i1)(j1) (comp^i T(j1) [ phi |-> t(j1) ] (comp^j T(i0) [=
phi |-> t(i0) ] t0)) (comp^j T(i1) [ phi |-> t(i1) ] (comp^i T(j0) [=
phi |-> t(j0) ] t0)) which is refl if T is degenerate in i OR j.

<=
div>This path plays the role that pres does in composition for Glue.=

We can't construct such a doubly regular path, but we ca=
n postulate it as a new operation our types have to have, as a sort of regu=
lar composition over two dimensions simultaneously. Write (i ?'[a] j) f=
or this, where a gives the location in the path.

However, my intu=
ition tells me that while this two-dimensional regular composition may be p=
reserved by all the usual type formers, optimistically including Glue and B=
ox, because the two-dimensional composition for Box will have to satisfy an=
additional law comp2^i^j (Box [ phi |-> A ] A) =3D comp2^i^j A, we will=
end up needing some sort of three-dimensional analogue.

Once we =
need dimensions 1 and 2, we will almost certainly need dimension n.

But what should the type of three dimensional regular com=
position be? There are six ways to compose along the edges of a cube, formi=
ng a hexagon that we wan't to fill, but hexagons don't fit nicely i=
nto cubical type theory.

Here, we remember that there is one more=
way to compose across a square: along the diagonal (comp^k T(i,j:=3Dk) [ p=
hi |-> t(i,j:=3Dk) ] t0), which agrees with composing either right then =
up or up then right when T is degenerate in i or j (with regularity).

=
Allowing diagonals, for each square we can give a path from the diagon=
al to going up then right, with swapping i and j giving a path to going rig=
ht then up. Then if both of these are degenerate when T is degenerate in i =
or j, their composition is also, so we recover a path between (i o j) and (=
j o i). And this formulation can be extended to higher dimensions straightf=
orwardly.

For each n-cube i_1, ..., i_n |- A, we h=
ave an n-dimensional regular composition operation which is a (n-1)-dimensi=
onal cube. Consider notation (i_1 ?[j_1] i_2 ?[j_2] ... ?[j_n-1] i_n) This =
is supposed to represent composition in an n-cube indexed by the i's, w=
here our position in the resulting (n-1)-cube is given by the j's. We h=
ave to describe the faces of this cube, which we describe by saying that ?[=
0] reduces to =3D and ?[1] reduces to o.

Thus for 2-dimensional A=
, we have a line (i =3D j) --- (i ?[a] j) --- (i o j), and for three dimens=
ional A, we have a square with four faces (i =3D j ?[a_2] k), (i o j ?[a_2]=
k), (i ?[a1] j =3D k) (i ?[a1] j o k), relating the four corners given by =
coercing over i then j then k, coercing over i then j and k simultaneously,=
coercing over i and j simultaneously then coercing over k, and coercing ov=
er i, j, and k simultaneously.

The point is that this gives a wel=
l-defined notion of cube.

We also have to define the regularity c=
ondition: what happens when A, a are degenerate in i_k? We require that (i_=
1 ... i_k-1 ?[j_k-1] i_k ?[j_k] i_k+1 ... i_n) is equal to (i_1 ... i_k-1 ?=
[j_k-1 v j_k] i_k+1 ... i_n), treating j_0 =3D j_n =3D 1.

Extendi=
ng this to =3D and o, if A, a are degenerate in i, then (i =3D j) and (i o =
j) reduce to (j).

On a two-dimensional cube, this says that (i ?[=
a] j) reduces to (j) when A, a are degenerate in i, and to (i) when A, a ar=
e degenerate in j.

(That this is all coherent is obvious to me, b=
ut I have no idea how to explain it well)

This all=
gives a notion of n-dimensional regular composition, which takes an n-cube=
type A and partial term phi, i1, ..., in |- a and=C2=A0a base point a0 : A=
(i_k :=3D 0)[ phi |-> a(i_k :=3D 0) ] and returns=C2=A0an (n-1)-cube in =
A(i_k :=3D 1) [ phi |-> everywhere a(i_k :=3D 1) ].

There are =
three classes of equations that this has to satisfy, two for the face maps =
j_k =3D 0 and j_k =3D 1 in the output, and one for when A, a are=C2=A0degen=
erate in i_k.

In the one-dimensional case, this is the same as th=
e specification of the usual regular comp.

Considering j_k to be =
formally extended with j_0 =3D j_n =3D 1, we get a "zero-dimensional&q=
uot; composition operation, which should be taken to be the identity. (I ha=
ve no idea what it would mean to let j_0 and j_n vary)

I am reaso=
nably confident that this operation is closed under usual type formers (Pi,=
Sg, Path, ...) by essentially the same argument as for 1-dimensional comp.=

I think I have worked out how to give a regular n-dimensional co=
mposition operation for Glue, by essentially the same argument as in CCHM, =
but with additional faces for j_k =3D 1 in the equiv and final hcomp steps.=

In this setting, we want Box to also be m-dimensi=
onal: j_1 ... j_n-1 |- Box^i1...^im _{j_1}..._{j_n-1} [ phi |-> T ] A fo=
r phi, i1, ..., im |- T, with phi |- A =3D T(i_k :=3D 1).

I think=
I have worked out how to give a regular n-dimensional composition operatio=
n for m-dimensional Box, using essentially the same argument as for Glue, b=
ut replacing pres with the composition of two paths given by (m+n)-dimensio=
nal regular composition.

To use Box as the regular n-dimensional =
composition operation for the universe, we need that (Box, comp Box) respec=
ts the equations for when j_k =3D 0, j_k =3D 1, or T is independent of j.

<= /div>

My hope is that, as in the (1, 1) dimensional case, using (m+n)-di=
mensional regular composition for pres will make this work.

<= /div>

I have sketched on paper that composition for Glue and Box are re=
gular, but that is already pushing the limits of my confidence in paper cal=
culations.

Checking that comp Box respects the equations that it =
needs to is another layer more=C2=A0complex, and I haven't managed to d=
o so on paper.

However, by analogy with the (1, 1) dimensional ca=
se, I am hopeful.

On Mon, Sep 16, 2019 at 3:01 PM Licata, Dan &=
lt;dlicata@wesleyan.edu> wro=
te:

Wow! I read that pretty closely and couldn=E2=80=99t find a problem. That i= s surprising to me. Will look more later.=C2=A0

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. =C2=A0

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?

-DanHi 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 ] a0delta |- t1' :=3D comp^i T [ psi |-> b ] b0delta |- omega :=3D pres^i f [ psi |-> b ] b0phi(i1) |- (t, alpha) :=3D equiv f(i1) [ delta |-> (t1', omega)= , psi |-> (b(i1), refl=C2=A0a1') ] a1'a1 :=3D hcomp^j A(i1) [ phi(i1) |-> alpha j, psi |-> a(i1) ] a1&= #39; (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 definepres^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 bThis 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 b0phi |- omega =3D refl=C2=A0(f b0)phi |- (t1, alpha) =3D (t1', omega) (since delta =3D phi, so we en= d up in the delta face of equiv)a1 =3D a1' (the only dependence on j is via (alpha j), but alpha = =3D omega =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=C2=A0CCHM)<= /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 <dlica= ta@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.=C2=A0

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.=C2= =A0 Do you think this does work out to be degenerate?=C2=A0

- 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)).=C2=A0 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.=C2=A0 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.=C2=A0 So I=E2=80=99d guess there is still a= problem in the aligned algorithm 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 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 HomotopyTypeTheory+unsubscribe@googlegroups.com.

> > To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAGTS-a9oS0CQDGKgj7ghC= h8%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-9rq5Q= WffU75Wz8myrXD1g5P3DCjSO%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://gro= ups.google.com/d/msgid/HomotopyTypeTheory/CAGTS-a8E03C3BMEwi-T4qjet4EbCgneP= hR3Ffa1MepxNmtZoUA%40mail.gmail.com.

--0000000000004483a40592b14a31--