Re: Define transport as the primitive operation of cubicaltt and derive composition from it?

["Anders Mörtberg" <"andersm..."@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 2893 bytes --]

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 = <j> 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'
>   = <i> 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 (<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 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.
>
>

[-- Attachment #1.2: Type: text/html, Size: 3264 bytes --]