<div dir="ltr">Yes thanks Anders for the clarifications. I was incorrect in saying r can't appear free in A (I forgot about the case in which transp appears in a larger context which contains more interval variables) and also that the code would only check that the input of A was ignored--checking that "A is convertible with \(_ : I). A i0" is certainly more sophisticated and will catch more cases. However as far as I understand one could still define a function that is propositionally equal to a constant function but not definitionally equal and the conversion checker would not be able to handle this case. Maybe it would be best to explicitly say " A is convertible with \(_ : I). A i0" in the documentation.<div><br></div><div>John</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Sep 3, 2020 at 3:10 PM Thorsten Altenkirch <<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk">Thorsten.Altenkirch@nottingham.ac.uk</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hi John,<br>
<br>
I hope Anders answer clarifies the situation.<br>
<br>
Sent from my iPhone<br>
<br>
> On 3 Sep 2020, at 21:04, John Leo <<a href="mailto:leo@halfaya.org" target="_blank">leo@halfaya.org</a>> wrote:<br>
> <br>
> <br>
> Let me respond to some of your questions, although I am not an expert.<br>
> <br>
> >But in this sentence, A is meant to be any expression, and it may contain r as a free variable.<br>
> <br>
> 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.<br>
<br>
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.<br>
> <br>
> 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.<br>
> <br>
<br>
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.<br>
<br>
<br>
> >I still don't understand what's meant by A should be a constant function.<br>
> <br>
> 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 ℓ?<br>
> <br>
> 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.<br>
> <br>
> >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?<br>
> <br>
> 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.<br>
> <br>
> John<br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br>
<br>
<br>
This message and any attachment are intended solely for the addressee<br>
and may contain confidential information. If you have received this<br>
message in error, please contact the sender and delete the email and<br>
attachment. <br>
<br>
Any views or opinions expressed by the author of this email do not<br>
necessarily reflect the views of the University of Nottingham. Email<br>
communications with the University of Nottingham may be monitored <br>
where permitted by law.<br>
<br>
<br>
<br>
<br>
</blockquote></div>