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

[John Leo]

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.

John

On Thu, Sep 3, 2020 at 3:10 PM Thorsten Altenkirch <
Thorsten.Altenkirch at nottingham.ac.uk> wrote:

> 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.
>
>
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200903/b745a379/attachment.html>