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

[Yuhao Huang <temp....@gmail.com>]

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

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: 1314 bytes --]