[Agda] Question about transport and cubical

[John Leo]

I'm not sure either what the author of this page meant by "A has to be
constant on r". Perhaps it is just poor wording but it doesn't make sense
to me either. It doesn't appear in the original Cubical Agda paper.

If you ignore that everything else seems fine, though. The key point is
that when r = i1 then transp must satisfy the additional constraint that
"transp A i1 a = a" for all "a" and when r = i0 there is no
additional constraint.

John

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

> 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
> _______________________________________________
> 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/794b0f49/attachment.html>