[Agda] Question about transport and cubical

[Manuel Bärenz]

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

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