[Agda] Fwd: Question about transport and cubical

[John Leo]

Thorsten's explanation is good. Just ignore the phrase " A has to be
constant on r". Everything else makes sense. If you want to know why there
is this additional condition, read the Cubical Agda paper.

John

On Thu, Sep 3, 2020 at 11:12 AM Manuel Bärenz <manuel at enigmage.de> wrote:

> I'm still confused. r doesn't influence the type of a in the expression
> transp A r a. If it was
>
> transp : ∀ {ℓ} (A : I → Set ℓ) (r : I) (a : A i0) → A r
>
>
> or something else where r is actually used in the rest of the signature,
> that would make sense, but how does setting some unrelated variable to a
> value influence the transport?
>
> -------- Forwarded Message --------
> Subject: Re: [Agda] Question about transport and cubical
> Date: Thu, 3 Sep 2020 18:06:46 +0000
> From: Thorsten Altenkirch <Thorsten.Altenkirch at nottingham.ac.uk>
> <Thorsten.Altenkirch at nottingham.ac.uk>
> To: Manuel Bärenz <manuel at enigmage.de> <manuel at enigmage.de>
>
> Yes, this puzzled me as well first.
>
>
>
> What is meant is that if you know r=i1 where r is any expression then A i
> = A j for any i,j : I.
>
> Then transp A r a : A i1
>
>
>
> You need this because if =i1 then transp A r a = a, but the lhs is in A i0
> and the rhs is in A i1.
>
>
>
> Thorsten
>
>
>
> *From: *Agda <agda-bounces at lists.chalmers.se>
> <agda-bounces at lists.chalmers.se> on behalf of Manuel Bärenz
> <manuel at enigmage.de> <manuel at enigmage.de>
> *Date: *Thursday, 3 September 2020 at 18:51
> *To: *"agda at lists.chalmers.se" <agda at lists.chalmers.se>
> <agda at lists.chalmers.se> <agda at lists.chalmers.se>
> *Subject: *[Agda] Question about transport and cubical
>
>
>
> Hi,
>
> I'm just reading the docs on Agda's Cubical TT support, and stumbled over
> this:
>
> transp : ∀ {ℓ} (A : I → Set ℓ) (r : I) (a : A i0) → A i1
>
> There is an additional side condition to be satisfied for transp A r a to
> type-check, which is that A has to be *constant* on r. This means that A
> should be a constant function whenever the constraint r = i1 is
> satisfied.
>
> https://agda.readthedocs.io/en/v2.6.1/language/cubical.html#transport
>
> I don't understand what that means. A is introduced before r. By
> definition, A does not depend on r, because r isn't even in scope for A. So
> any constraint on r doesn't have any effect on A. In fact, r never appears
> again in the type signature. So vacuously, A is constant on r because it
> doesn't use r.
>
> Probably I'm just misunderstanding something basic.
>
> Best regards, Manuel
>
> 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.
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200903/47047697/attachment.html>