<div dir="ltr"><div dir="ltr"></div><div>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:<br></div><div><br></div><div><a href="https://arxiv.org/abs/1802.01170">https://arxiv.org/abs/1802.01170</a></div><div><br></div><div>I'll try to answer some of your questions below.<br></div><div><br></div><div></div><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Sep 3, 2020 at 9:19 PM Manuel Bärenz <<a href="mailto:manuel@enigmage.de" target="_blank">manuel@enigmage.de</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div>
<p>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.</p></div></blockquote><div><br></div><div>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):<br></div><div><br></div><div>\(j : I). transp (\(i : I). B (i /\ j)) j u</div><div><br></div><div>This is an example where the "A" contains the "r" (in this case A is \(i : I). B (i /\ j) and r is j).<br></div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div>
<p>Taking John's advice to ignore that phrase, I look at the
following:<br>
</p>
<p><font color="#a30c0c">There is an additional side condition to be
satisfied for <code><span>transp</span> <span>A</span> <span>r</span>
<span>a</span></code> to type-check, which is
[...] that <code><span>A</span></code> should be a constant function
whenever
the constraint <code><span>r</span> <span>=</span> <span>i1</span></code> is satisfied.</font></p>
<p>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.<br>
</p>
<p>I still don't understand what's meant by <span><span>A</span></span><span style="color:rgb(163,12,12)"> should be a constant function</span>. 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?<br></p></div></blockquote><div><br></div><div>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.<br></div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div><p>
</p>
<div>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:</div>
<div><br>
</div>
<div><font color="#a30c0c">However
when <code><span>r</span></code> is equal to <code><span>i1</span></code>
the
<code><span>transp</span></code>
function will compute as the identity function.</font></div>
<div><br>
</div>
<div>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.<br>
</div>
<div><br></div></div></blockquote></div><div class="gmail_quote"><br></div><div class="gmail_quote">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 <br></div><div class="gmail_quote"><br></div><div class="gmail_quote">transp (ua e) i0 x = fst e x</div><div class="gmail_quote"><br></div><div class="gmail_quote">(up to a path, see <a href="https://github.com/agda/cubical/blob/master/Cubical/Foundations/Univalence.agda#L233">https://github.com/agda/cubical/blob/master/Cubical/Foundations/Univalence.agda#L233</a> for the proof)</div><div class="gmail_quote"><div> <br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div><div>
</div>
<div>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.</div>
<div><br>
</div>
<div>If I can make sense of this all,
I'll try and improve this part of the docs.<br>
</div>
<div><br></div></div></blockquote><div><br></div><div>That's very welcome! <br></div><br></div></div>