[Agda] Fwd: Question about transport and cubical

[Manuel Bärenz]

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>
To: 	Manuel Bärenz <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> on behalf of Manuel Bärenz
<manuel at enigmage.de>
*Date: *Thursday, 3 September 2020 at 18:51
*To: *"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||ato type-check, which is that Ahas to be /constant/ on r.
This means that Ashould be a constant function whenever the constraint
r||=||i1is 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.



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