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

[Thorsten Altenkirch]

Hi John,

I hope Anders answer clarifies the situation.

Sent from my iPhone

> On 3 Sep 2020, at 21:04, John Leo <leo at halfaya.org> wrote:
> 
> 
> 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.

There is an interesting confusion here. “r” is a meta variable standing for a term not an object variable which may or may not appear in A. However it can be a variable in the current context which occurs in A.
> 
> 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.
> 

Yes exactly this is the point. The systems which are implemented via pattern matching simplify due to constraints like r=i1 and as a result A may become a constant function.


> >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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda



This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.