From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Sun, 5 Nov 2017 07:09:22 -0800 (PST) From: =?UTF-8?Q?Anders_M=C3=B6rtberg?= To: Homotopy Type Theory Message-Id: In-Reply-To: References: Subject: Re: Define transport as the primitive operation of cubicaltt and derive composition from it? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_7455_1238622838.1509894562688" ------=_Part_7455_1238622838.1509894562688 Content-Type: multipart/alternative; boundary="----=_Part_7456_1665322051.1509894562688" ------=_Part_7456_1665322051.1509894562688 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit The problem with defining only transport shows up when you try to define it for Path types. For these you somehow need to remember the end-points of the path you are transporting in, which naturally leads one to generalize to the comp operation. In more detail, writing (0/i) for the substitution of 0 for i: Given G, i : II |- T and G |- t : T(0/i) we want to define G |- transport^i T t : T(1/i) We do this by case on T which means that we have to explain it for the case when T is Path A a b and t is a path p : (Path A a b)(0/i). We hence want to define: transport^i (Path A a b) p : (Path A a b)(1/i) As all type formers commute with substitution the type is equal to Path A(1/i) a(1/i) b(1/i). As we are defining a path we can try to define this using path abstraction as follows: transport^i (Path A a b) p = transport^i A (p @ j) This does indeed give us a path in A(1/i), but it connects transport^i A a with transport^i A b which is not necessarily the same as a(1/i) and b(1/i). So we need a way to enforce that the end-points of the path we construct is a(1/i) and b(1/i) which is what comp gives us. Note that one could instead have two operations instead of only comp, one for doing "comp" in a constant type (called "homogeneous comp" or "hcomp") and one for transport. This is the approach taken by computational higher type theory. We had a version of the system with this at some point, but we decided that it would be easier to only have one operation as the system would be easier to write down as we only have to explain how to do comp and not how to do both hcomp and transport. -- Anders On Friday, November 3, 2017 at 8:27:36 PM UTC-4, Yuhao Huang wrote: > > 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_7456_1665322051.1509894562688 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
The problem with defining only transport shows up when you= try to define it for Path types. For these you somehow need to remember th= e end-points of the path you are transporting in, which naturally leads one= to generalize to the comp operation.

In more detail, writing (0/i)= for the substitution of 0 for i:

Given G, i : II |- T and G |- t : = T(0/i) we want to define

G |- transport^i T t : T(1/i)

We do = this by case on T which means that we have to explain it for the case when = T is Path A a b and t is a path p : (Path A a b)(0/i). We hence want to def= ine:

transport^i (Path A a b) p : (Path A a b)(1/i)

As all ty= pe formers commute with substitution the type is equal to Path A(1/i) a(1/i= ) b(1/i). As we are defining a path we can try to define this using path ab= straction as follows:

transport^i (Path A a b) p =3D <j> trans= port^i A (p @ j)

This does indeed give us a path in A(1/i), but it c= onnects transport^i A a with transport^i A b which is not necessarily the s= ame as a(1/i) and b(1/i). So we need a way to enforce that the end-points o= f the path we construct is a(1/i) and b(1/i) which is what comp gives us.
Note that one could instead have two operations instead of only comp= , one for doing "comp" in a constant type (called "homogeneo= us comp" or "hcomp") and one for transport. This is the appr= oach taken by computational higher type theory. We had a version of the sys= tem with this at some point, but we decided that it would be easier to only= have one operation as the system would be easier to write down as we only = have to explain how to do comp and not how to do both hcomp and transport.<= br>
--
Anders

On Friday, November 3, 2017 at 8:27:36 PM UTC-4,= Yuhao Huang wrote:
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

=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 "transport= " and derive comp from it?

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

compUp (A B : U) (P : P= ath 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&#= 39; b') : Path B b b'
=C2=A0 =3D transport (<i> (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 wit= h given boundary condition. So why not start with transport and define comp= osition later? If this is doable then hopefully equality judgements for tra= nsports are simpler than that of compositions.

------=_Part_7456_1665322051.1509894562688-- ------=_Part_7455_1238622838.1509894562688--