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

[Anders Mortberg]

Thanks for the many questions! I totally agree that the documentation for
Cubical Agda should improve, especially the part about transp. The current
version of the documentation was mostly written by me to explain some of
the (quite technical) ideas from the paper where we introduced the transp
operation:

https://arxiv.org/abs/1802.01170

I'll try to answer some of your questions below.

On Thu, Sep 3, 2020 at 9:19 PM Manuel Bärenz <manuel at enigmage.de> wrote:

> 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.
>

Yeah, so A is just any function out of the interval into the universe. So
it can contain any interval variables that are currently in scope. For
example, given some B : I -> Set and u : B i0 we can write (in pseudo-Agda):

\(j : I). transp (\(i : I). B (i /\ j)) j u

This is an example where the "A" contains the "r" (in this case A is \(i :
I). B (i /\ j) and r is j).


> Taking John's advice to ignore that phrase, I look at the following:
>
> There is an additional side condition to be satisfied for transp A r a to
> type-check, which is [...] that A should be a constant function whenever
> the constraint r = i1 is satisfied.
>
> 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 A should 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?
>

Agda checks it during conversion checking. One way to do it is to check
that whenever r = i1 then A is convertible with \(_ : I). A i0. In other
words that A is a constant function whenever r = i1.


> 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.
>
>
The transp function does not always compute as the identity function. For
instance if A is defined using univalence applied to some equivalence e,
then "transp A i0 u" will apply the first projection of e (i.e. the
function) to u. That is, given e : Equiv X Y and x : X then

transp (ua e) i0 x = fst e x

(up to a path, see
https://github.com/agda/cubical/blob/master/Cubical/Foundations/Univalence.agda#L233
for the proof)


> 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.
>
>
That's very welcome!
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200903/26b51ef8/attachment.html>