* Define transport as the primitive operation of cubicaltt and derive composition from it?
@ 2017-11-04 0:27 Yuhao Huang
2017-11-05 15:09 ` Anders Mörtberg
0 siblings, 1 reply; 2+ messages in thread
From: Yuhao Huang @ 2017-11-04 0:27 UTC (permalink / raw)
To: Homotopy Type Theory
[-- 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 --]
^ permalink raw reply [flat|nested] 2+ messages in thread
* Re: Define transport as the primitive operation of cubicaltt and derive composition from it?
2017-11-04 0:27 Define transport as the primitive operation of cubicaltt and derive composition from it? Yuhao Huang
@ 2017-11-05 15:09 ` Anders Mörtberg
0 siblings, 0 replies; 2+ messages in thread
From: Anders Mörtberg @ 2017-11-05 15:09 UTC (permalink / raw)
To: Homotopy Type Theory
[-- 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 --]
^ permalink raw reply [flat|nested] 2+ messages in thread
end of thread, other threads:[~2017-11-05 15:09 UTC | newest]
Thread overview: 2+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2017-11-04 0:27 Define transport as the primitive operation of cubicaltt and derive composition from it? Yuhao Huang
2017-11-05 15:09 ` Anders Mörtberg
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).