From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Mon, 23 Oct 2017 21:10:56 -0700 (PDT) From: jas...@cs.washington.edu To: Homotopy Type Theory Message-Id: Subject: Definition of semantic composition in CCHM cubical type theory MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_12643_723249351.1508818256960" ------=_Part_12643_723249351.1508818256960 Content-Type: multipart/alternative; boundary="----=_Part_12644_1444359170.1508818256960" ------=_Part_12644_1444359170.1508818256960 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Hello, I've been reading through Cubical Type Theory: a constructive=20 interpretation of the univalence axiom=20 , trying to understand the model=20 constructed there. I got confused about a few details, and I hoped someone on this list could= =20 help clarify them. The semantic composition structure (p.19) takes as an argument =CF=81 =E2= =88=88 =CE=93(I, i).=20 For f : J =E2=86=92 I (a map I to dM(J)) and fresh j, we have restrictions= =20 using =CF=81(f, i =3D j), which I am reading as the restriction of =CF=81 a= long g : J,=20 j -> I, i (a map I, i to dm(J, j)) that takes I by f (with the inclusion of= =20 dM(J) into dM(J, j)) and takes i to j in dM(J, j). That part I think I can= =20 follow. Then down in the interpretation from syntax (bottom of p.22, top of p.23),= =20 we define the interpretation of comp as [[=CE=93; comp i A [=CF=95 =E2=86=92 u] a0]]=CF=81 =3D comp El [[=CE=93,i:I= I;A]] (I, j, =CF=81=E2=80=B2 , [[=CE=93; =CF=95]]=CF=81,=20 [[=CE=93, =CF=95, i: II; u]]=CF=81=E2=80=B2 , [[=CE=93; a0]]=CF=81) using =CF=81=E2=80=B2 =3D (=CF=81 s_j , i =3D j), supposedly in =CE=93(I, j= ). We have =CF=81 =E2=88=88 [[=CE=93]](I)=20 and s_j : I, j =E2=86=92 I is the inclusion. I don't understand how to read =CF=81=E2=80=B2 =3D (=CF=81 s_j , i =3D j). = Where does i come=20 from, and what does it mean to set =CF=81=E2=80=B2 to be a pair of =CF=81 s= _j and the=20 substitution i =3D j? I think, we have El [[=CE=93,i:II;A]] in Ty([[=CE=93,= i:II]]), so=20 we expect =CF=81=E2=80=B2 in [[=CE=93,i:II]](I, i), so =CF=81=E2=80=B2 is a= pair of [[=CE=93]](I, i) and II(I,=20 i), so i guess we have =CF=81 s_j in [[=CE=93]](I, i) and i =3D j in II(I, = i)? As I was writing this I think I made some progress, but I still don't=20 understand what it means to have i =3D j in II(I, i). Does it have anything to do with the other place =CF=81=E2=80=B2 is used, = in [[=CE=93, =CF=95, i:=20 II; u]]=CF=81=E2=80=B2 ? Thanks in advance for any clarification, - Jasper Hugunin p.s. I've been studying the CCHM model with an eye towards giving the comp= =20 operation a (hopefully fibrant) type. The only place I've seen (semantic)= =20 comp used is in the translation from syntax, which would mean that =CF=81 a= lways=20 has the form (=CF=81 s_j , i =3D j), and so possibly we could replace comp = with=20 something like "a composition structure for A in Ty(=CE=93 . II) is, for al= l I=20 and =CF=81 in =CE=93(I) (which looks like a cubical type) ... (with =CF=81 = replaced with=20 (=CF=81 s_j , i =3D j) in the body). I'm still just taking stabs in the dark in the area of model theory, so any= =20 thoughts on the feasibility of this would also be appreciated (if it isn't= =20 obviously ridiculous). The hope being that we could then define operations like fill and contr=20 inside the theory, and possibly making progress towards a=20 higher-inductive-recursive universe in the style of=20 https://homotopytypetheory.org/2014/06/08/hiru-tdd/. I don't understand Glue types very well, and they seem to be the most=20 complicated part of the system, so I've been pondering ways to do without= =20 them. ------=_Part_12644_1444359170.1508818256960 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
Hello,

I've been reading through=C2= =A0Cubical Type Theory: a = constructive interpretation of the univalence axiom, trying to understa= nd the model constructed there.
I got confused about a few detail= s, and I hoped someone on this list could help clarify them.

=
The semantic composition structure (p.19) takes as an argument = =CF=81 =E2=88=88 =CE=93(I, i). For f : J =E2=86=92 I (a map I to dM(J)) and= fresh j, we have restrictions using=C2=A0=CF=81(f, i =3D j), which I am re= ading as the restriction of =CF=81 along g : J, j -> I, i (a map I, i to= dm(J, j)) that takes I by f (with the inclusion of dM(J) into dM(J, j)) an= d takes i to j in dM(J, j). That part I think I can follow.

<= /div>
Then down in the interpretation from syntax (bottom of p.22, top = of p.23), we define the interpretation of comp as
[[=CE=93; comp = i A [=CF=95 =E2=86=92 u] a0]]=CF=81 =3D comp El [[=CE=93,i:II;A]] (I, j, = =CF=81=E2=80=B2 , [[=CE=93; =CF=95]]=CF=81, [[=CE=93, =CF=95, i: II; u]]=CF=81=E2=80=B2 , [[=CE=93; a0]]=CF=81)
using=C2=A0=CF=81=E2=80=B2 =3D (=CF= =81 s_j , i =3D j), supposedly in =CE=93(I, j). We have=C2=A0=CF=81 =E2=88= =88 [[=CE=93]](I) and=C2=A0 s_j : I, j =E2=86=92 I is the inclusion.
<= div>
I don't understand how to read =CF=81=E2=80=B2 =3D (= =CF=81 s_j , i =3D j). Where does i come from, and what does it mean to set= =CF=81=E2=80=B2 to be a pair of =CF=81 s_j and the substitution i =3D j? I= think, we have El [[=CE=93,i:II;A]] in Ty([[=CE=93,i:II]]), so we expect = =CF=81=E2=80=B2 in [[=CE=93,i:II]](I, i), so =CF=81=E2=80=B2 is a pair of [= [=CE=93]](I, i) and II(I, i), so i guess we have =CF=81 s_j in [[=CE=93]](I= , i) and i =3D j in II(I, i)?

As I was writing thi= s I think I made some progress, but I still don't understand what it me= ans to have=C2=A0 i =3D j in II(I, i).
Does it have anything to d= o with the other place =CF=81=E2=80=B2=C2=A0 is used, in [[=CE=93, =CF=95, = i: II; u]]=CF=81=E2=80=B2 ?

Thanks in advance for = any clarification,
- Jasper Hugunin

p.s.= I've been studying the CCHM model with an eye towards giving the comp = operation a (hopefully fibrant) type. The only place I've seen (semanti= c) comp used is in the translation from syntax, which would mean that =CF= =81 always has the form (=CF=81 s_j , i =3D j), and so possibly we could re= place comp with something like "a composition structure for A in Ty(= =CE=93 . II) is, for all I and =CF=81 in =CE=93(I) (which looks like a cubi= cal type) ... (with =CF=81 replaced with (=CF=81 s_j , i =3D j) in the body= ).
I'm still just taking stabs in the dark in the area of mod= el theory, so any thoughts on the feasibility of this would also be appreci= ated (if it isn't obviously ridiculous).

The h= ope being that we could then define operations like fill and contr inside t= he theory, and possibly making progress towards a higher-inductive-recursiv= e universe in the style of=C2=A0https://homotopytypetheory.org/2014/06/08/hiru-tdd/.
I don't understand Glue types very well, and they seem to = be the most complicated part of the system, so I've been pondering ways= to do without them.

------=_Part_12644_1444359170.1508818256960-- ------=_Part_12643_723249351.1508818256960--