[Agda] Question about transport and cubical

[Andreas Källberg]

The wording is indeed confusing. I think, by “constant on r”, they mean “constant when r is i1”, which is consistent with phrasing used in some other contexts in the paper, especially regarding comp, where "on φ” means “the faces of a cube where φ is i1”. I think I’ve seen this concept being called a “face lattice” somewhere.

If we didn’t have this restriction, we could have a function like this:

    bad-refl : ∀ {ℓ} {A B : Set ℓ} → A ≡ B → A → B
    bad-refl p a = transp (λ i → p i) i1 a

which would evaluate to

    bad-refl : ∀ {ℓ} {A B : Set ℓ} → A ≡ B → A → B
    bad-refl p a = refl a

which obviously doesn’t type check.

Regards,
Andreas

> On 3 Sep 2020, at 20:07, John Leo <leo at halfaya.org> wrote:
> 
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda