[Agda] Fwd: Fwd: Question about transport and cubical

[John Leo]

Let me respond to some of your questions, although I am not an expert.

>But in this sentence, A is meant to be any expression, and it may contain
r as a free variable.

I don't believe it is possible for A to contain r as a free variable. A has
type A : I → Set ℓ. It is typical to use "r" to denote the input to a
function whose domain is the interval; I think this is part of the
confusion. But A should not be allowed to contain any reference to interval
variables other than its bound input.

Thorston mentions that A can pattern match on "r" (here he is using r to
refer to the input of A rather than the specific r passed to transport) but
I don't believe this is correct (see section 3.1 of the Cubical Agda
paper). One can only pattern match on an interval when creating "Partial"
elements (see later in the doc). Someone correct me if I'm wrong.

>I still don't understand what's meant by A should be a constant function.

Since the type of A is I → Set ℓ it simply means that the value of A must
not depend on its input (a member of the interval type). Of course there
are some followup questions: How is this checked by the typechecker? And if
A can't depend on its input why not just force it to have type Set ℓ?

I haven't looked at the code but I assume the check is a basic syntactic
check that if A is of the form λ i → B then i cannot appear in B (so it may
exclude functions which are not syntactically constant). However my
understanding (again correct me if I'm wrong) is that this check only takes
place when typechecking "transp A r" and r is not known to be i0. In the
case r=i0 there is no constraint on A and A is allowed to be nonconstant.
This happens in the definition of transport immediately below: "transport p
a = transp (λ i → p i) i0 a". In this case A is not necessarily constant.

>At the end, doesn't transp A i always compute as the identity function?
Isn't the point of transport to just verify that two types are equal so we
can safely coerce?

No, transport takes a proof of the equality of two types as an input and
then does the coercion. It need not be the identity function. For example,
using the non-refl self-equivalence of Bool, transport should send true to
false and vice-versa.

John
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200903/32057690/attachment.html>