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

Thu Sep 3 21:19:11 CEST 2020

Thanks Thorsten for the extended explanation. I think I now understand
that the point is that we might call transp in a situation where A is an
expression that may contain r.

Taking John's advice to ignore that phrase, I look at the following:

One part of the confusion was probably that I thought about A as a
closed expression, since there is a binding of the same name directly
before in the type signature. But in this sentence, A is meant to be any
expression, and it may contain r as a free variable.

I still don't understand what's meant by Ashould be a constant function.
Who checks that? Obviously the semantics of A has to be constant, after
all that's the point behind cubical type theory, isn't it? So I guess it
must mean that the sort-of-lambda-expression must be a constant function
in that it doesn't depend on its argument. Is Cubical Agda able to check
whether functions of type I -> Set are constant? How does the check
work? λ _ . A is constant, but is λ i . (λ _ . A) i constant for that
matter? Or does it normalize A i0 and A i1 and then tries to unify them?

I realize that this is maybe not the place to discuss articles. But I
believe it's the right place to talk about the documentation of the
language. During ICFP I got the impression that I'm not the only one
struggling with an intuitive understanding of how to use Cubical Agda.
Keeping the documentation understandable is important to improve that.
Especially on an intricate topic like equality reasoning, confusing
wording can be an obstruction. For example:

However when |r| is equal to |i1| the |transp| function will compute as
the identity function.

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? I believe I can sort of see what the argument is
intending to say, it's more like "transp A i1 must be able to have the
type {B : Set l} -> B -> B, so in the branch where transp is called with
r = i1 we must have that A is constantly B.", but I might be
misunderstanding this again.

It is sometimes said that HoTT solves the problem of equality, but it
seems to me more like that it pushes the problem to documentation and
conversation, because we don't have good words to talk about the
different kinds of equality.

If I can make sense of this all, I'll try and improve this part of the docs.

-------- Forwarded Message --------
Subject: 	Re: [Agda] Fwd: Question about transport and cubical
Date: 	Thu, 3 Sep 2020 18:28:07 +0000
From: 	Thorsten Altenkirch <Thorsten.Altenkirch at nottingham.ac.uk>
To: 	Manuel Bärenz <manuel at enigmage.de>

Ok, we now have equational assumptions like r=i1 where r is some
expression of type I. For example a variable like i.

Now the type A also uses “r” and you can check that if r==i1 then A is
constant.  It may contain a match on r and if r=i1 then the branch
doesn’t mention the paremeter.

This is a requirement for the expression “transp A r a” to typecheck.
E.g. in my example it would be transp A i a which has the type A i1.
Assuming r=i1 it is equal to a : A i0. But this deosn’t matter because
of the condition on A.

I think the best way to understand this is to start proving something
about transp and then to write down each step of the derivation in a
comment. Then you realize why you need it.

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 19:12
*To: *"agda at lists.chalmers.se" <agda at lists.chalmers.se>
*Subject: *[Agda] Fwd: Question about transport and cubical

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>
<mailto:Thorsten.Altenkirch at nottingham.ac.uk>

*To: *

Manuel Bärenz <manuel at enigmage.de> <mailto: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>
<mailto:agda-bounces at lists.chalmers.se> on behalf of Manuel Bärenz
<manuel at enigmage.de> <mailto:manuel at enigmage.de>
*Date: *Thursday, 3 September 2020 at 18:51
*To: *"agda at lists.chalmers.se" <mailto:agda at lists.chalmers.se>
<agda at lists.chalmers.se> <mailto: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.

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/87d4342f/attachment.html>