From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Fri, 3 Nov 2017 17:27:36 -0700 (PDT) From: Yuhao Huang To: Homotopy Type Theory Message-Id: Subject: Define transport as the primitive operation of cubicaltt and derive composition from it? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_4068_664939191.1509755256794" ------=_Part_4068_664939191.1509755256794 Content-Type: multipart/alternative; boundary="----=_Part_4069_24485472.1509755256794" ------=_Part_4069_24485472.1509755256794 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit I've been reading the cubical type theory paper and experimenting with cubicaltt. In cubicaltt, we have the composition operation as one of the primitive operations. Given a path p from A to B, the transport is defined by trans A B p a : B = comp p a [] My question is, can we define a primitive operation "transport" and derive comp from it? For example, the comp in the following definition (using cubicaltt's syntax) compUp (A B : U) (P : Path U A B) (a a' : A) (b b' : B) (p : Path A a a') (q : PathP P a b) (q' : PathP P a' b') : Path B b b' = comp P (p @ i) [(i = 0) -> q, (i = 1) -> q'] can be replaced by compUp2 (A B : U) (P : Path U A B) (a a' : A) (b b' : B) (p : Path A a a') (q : PathP P a b) (q' : PathP P a' b') : Path B b b' = transport ( (Path (P @ i) (q @ i) (q' @ i))) p and similarly for other comps. The way I understand the composition operation is, it's a transport with given boundary condition. So why not start with transport and define composition later? If this is doable then hopefully equality judgements for transports are simpler than that of compositions. ------=_Part_4069_24485472.1509755256794 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
I've been reading the cubical type theory paper and ex= perimenting with cubicaltt.

In cubicaltt, we have the composition o= peration as one of the primitive operations. Given a path p from A to B, th= e transport is defined by

=C2=A0=C2=A0=C2=A0 trans A B p a : B =3D = comp p a []

My question is, can we define a primitive operation &quo= t;transport" and derive comp from it?

For example, the comp in = the following definition (using cubicaltt's syntax)

compUp (A B = : U) (P : Path U A B) (a a' : A) (b b' : B) (p : Path A a a') (= q : PathP P a b) (q' : PathP P a' b') : Path B b b'
=C2= =A0 =3D <i> comp P (p @ i) [(i =3D 0) -> q, (i =3D 1) -> q'= ]

can be replaced by

compUp2 (A B : U) (P : Path U A B) (a a= ' : A) (b b' : B) (p : Path A a a') (q : PathP P a b) (q' := PathP P a' b') : Path B b b'
=C2=A0 =3D transport (<i>= ; (Path (P @ i) (q @ i) (q' @ i))) p

and similarly for other com= ps.

The way I understand the composition operation is, it's a t= ransport with given boundary condition. So why not start with transport and= define composition later? If this is doable then hopefully equality judgem= ents for transports are simpler than that of compositions.

------=_Part_4069_24485472.1509755256794-- ------=_Part_4068_664939191.1509755256794--