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