<html>
  <head>

    <meta http-equiv="content-type" content="text/html; charset=UTF-8">
  </head>
  <body>
    <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>
    <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 class="docutils literal notranslate"><span
            class="pre">transp</span> <span class="pre">A</span> <span
            class="pre">r</span>
          <span class="pre">a</span></code> to type-check, which is
        [...] that <code class="docutils literal notranslate"><span
            class="pre">A</span></code> should be a constant function
        whenever
        the constraint <code class="docutils literal notranslate"><span
            class="pre">r</span> <span class="pre">=</span> <span
            class="pre">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 class="pre"><span
          style="font-size:10.0pt;font-family:"Courier New
          ;color:#A30C0C",serif">A</span></span><span
        style="color:#A30C0C"> 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 class="moz-forward-container">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 class="moz-forward-container"><br>
    </div>
    <div class="moz-forward-container"><font color="#a30c0c">However
        when <code class="docutils literal notranslate"><span
            class="pre">r</span></code> is equal to <code
          class="docutils literal notranslate"><span class="pre">i1</span></code>
        the
        <code class="docutils literal notranslate"><span class="pre">transp</span></code>
        function will compute as the identity function.</font></div>
    <div class="moz-forward-container"><br>
    </div>
    <div class="moz-forward-container">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 class="moz-forward-container"><br>
    </div>
    <div class="moz-forward-container">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 class="moz-forward-container"><br>
    </div>
    <div class="moz-forward-container">If I can make sense of this all,
      I'll try and improve this part of the docs.<br>
    </div>
    <div class="moz-forward-container"><br>
    </div>
    <div class="moz-forward-container">-------- Forwarded Message
      --------
      <table class="moz-email-headers-table" cellspacing="0"
        cellpadding="0" border="0">
        <tbody>
          <tr>
            <th valign="BASELINE" nowrap="nowrap" align="RIGHT">Subject:
            </th>
            <td>Re: [Agda] Fwd: Question about transport and cubical</td>
          </tr>
          <tr>
            <th valign="BASELINE" nowrap="nowrap" align="RIGHT">Date: </th>
            <td>Thu, 3 Sep 2020 18:28:07 +0000</td>
          </tr>
          <tr>
            <th valign="BASELINE" nowrap="nowrap" align="RIGHT">From: </th>
            <td>Thorsten Altenkirch
              <a class="moz-txt-link-rfc2396E" href="mailto:Thorsten.Altenkirch@nottingham.ac.uk"><Thorsten.Altenkirch@nottingham.ac.uk></a></td>
          </tr>
          <tr>
            <th valign="BASELINE" nowrap="nowrap" align="RIGHT">To: </th>
            <td>Manuel Bärenz <a class="moz-txt-link-rfc2396E" href="mailto:manuel@enigmage.de"><manuel@enigmage.de></a></td>
          </tr>
        </tbody>
      </table>
      <br>
      <br>
      <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
      <meta name="Generator" content="Microsoft Word 15 (filtered
        medium)">
      <style><!--
/* Font Definitions */
@font-face
        {font-family:"Cambria Math";
        panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
        {font-family:Calibri;
        panose-1:2 15 5 2 2 2 4 3 2 4;}
@font-face
        {font-family:Consolas;
        panose-1:2 11 6 9 2 2 4 3 2 4;}
@font-face
        {font-family:"Courier New \;color\:\#A30C0C";
        panose-1:2 7 3 9 2 2 5 2 4 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
        {margin:0cm;
        font-size:11.0pt;
        font-family:"Calibri",sans-serif;}
a:link, span.MsoHyperlink
        {mso-style-priority:99;
        color:blue;
        text-decoration:underline;}
code
        {mso-style-priority:99;
        font-family:"Courier New";}
pre
        {mso-style-priority:99;
        mso-style-link:"HTML Preformatted Char";
        margin:0cm;
        font-size:10.0pt;
        font-family:"Courier New";}
span.HTMLPreformattedChar
        {mso-style-name:"HTML Preformatted Char";
        mso-style-priority:99;
        mso-style-link:"HTML Preformatted";
        font-family:Consolas;}
span.nf
        {mso-style-name:nf;}
span.ow
        {mso-style-name:ow;}
span.o
        {mso-style-name:o;}
span.kt
        {mso-style-name:kt;}
span.pre
        {mso-style-name:pre;}
span.EmailStyle29
        {mso-style-type:personal-reply;
        font-family:"Calibri",sans-serif;
        color:windowtext;}
.MsoChpDefault
        {mso-style-type:export-only;
        font-size:10.0pt;}
@page WordSection1
        {size:612.0pt 792.0pt;
        margin:72.0pt 72.0pt 72.0pt 72.0pt;}
div.WordSection1
        {page:WordSection1;}
--></style>
      <div class="WordSection1">
        <p class="MsoNormal"><span style="mso-fareast-language:EN-US">Ok,
            we now have equational assumptions like r=i1 where r is some
            expression of type I. For example a variable like i.<o:p></o:p></span></p>
        <p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
        <p class="MsoNormal"><span style="mso-fareast-language:EN-US">Now
            the type A also uses “r” and you can check that if r==i1
            then A is constant.  It may contain a match on r and if r=i1
            then the branch doesn’t mention the paremeter.<o:p></o:p></span></p>
        <p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
        <p class="MsoNormal"><span style="mso-fareast-language:EN-US">This
            is a requirement for the expression “transp A r a” to
            typecheck. E.g. in my example it would be transp A i a which
            has the type A i1. Assuming r=i1 it is equal to a : A i0.
            But this deosn’t matter because of the condition on A. <o:p></o:p></span></p>
        <p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
        <p class="MsoNormal"><span style="mso-fareast-language:EN-US">I
            think the best way to understand this is to start proving
            something about transp and then to write down each step of
            the derivation in a comment. Then you realize why you need
            it.<o:p></o:p></span></p>
        <p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
        <p class="MsoNormal"><span style="mso-fareast-language:EN-US">Thorsten<o:p></o:p></span></p>
        <p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
        <div style="border:none;border-top:solid #B5C4DF
          1.0pt;padding:3.0pt 0cm 0cm 0cm">
          <p class="MsoNormal"><b><span
                style="font-size:12.0pt;color:black">From: </span></b><span
              style="font-size:12.0pt;color:black">Agda
              <a class="moz-txt-link-rfc2396E" href="mailto:agda-bounces@lists.chalmers.se"><agda-bounces@lists.chalmers.se></a> on behalf of Manuel
              Bärenz <a class="moz-txt-link-rfc2396E" href="mailto:manuel@enigmage.de"><manuel@enigmage.de></a><br>
              <b>Date: </b>Thursday, 3 September 2020 at 19:12<br>
              <b>To: </b><a class="moz-txt-link-rfc2396E" href="mailto:agda@lists.chalmers.se">"agda@lists.chalmers.se"</a>
              <a class="moz-txt-link-rfc2396E" href="mailto:agda@lists.chalmers.se"><agda@lists.chalmers.se></a><br>
              <b>Subject: </b>[Agda] Fwd: Question about transport and
              cubical<o:p></o:p></span></p>
        </div>
        <div>
          <p class="MsoNormal"><o:p> </o:p></p>
        </div>
        <p>I'm still confused. r doesn't influence the type of a in the
          expression transp A r a. If it was
          <o:p></o:p></p>
        <pre><span class="nf"><span style="color:#A30C0C">transp</span></span><span style="color:#A30C0C"> <span class="ow">:</span> </span><span class="ow"><span style="font-family:"Cambria Math",serif;color:#A30C0C">∀</span></span><span style="color:#A30C0C"> <span class="o">{</span>ℓ<span class="o">}</span> <span class="o">(</span>A <span class="ow">:</span> I <span class="ow">→</span> <span class="kt">Set</span> ℓ<span class="o">)</span> <span class="o">(</span>r <span class="ow">:</span> I<span class="o">)</span> <span class="o">(</span>a <span class="ow">:</span> A i0<span class="o">)</span> <span class="ow">→</span> A r</span><o:p></o:p></pre>
        <div>
          <p class="MsoNormal"><o:p> </o:p></p>
        </div>
        <div>
          <p class="MsoNormal">or something else where r is actually
            used in the rest of the signature, that would make sense,
            but how does setting some unrelated variable to a value
            influence the transport?<br>
            <br>
            -------- Forwarded Message -------- <o:p></o:p></p>
          <table class="MsoNormalTable" cellspacing="0" cellpadding="0"
            border="0">
            <tbody>
              <tr>
                <td style="padding:0cm 0cm 0cm 0cm" valign="top"
                  nowrap="nowrap">
                  <p class="MsoNormal" style="text-align:right"
                    align="right"><b>Subject: <o:p></o:p></b></p>
                </td>
                <td style="padding:0cm 0cm 0cm 0cm">
                  <p class="MsoNormal">Re: [Agda] Question about
                    transport and cubical<o:p></o:p></p>
                </td>
              </tr>
              <tr>
                <td style="padding:0cm 0cm 0cm 0cm" valign="top"
                  nowrap="nowrap">
                  <p class="MsoNormal" style="text-align:right"
                    align="right"><b>Date: <o:p></o:p></b></p>
                </td>
                <td style="padding:0cm 0cm 0cm 0cm">
                  <p class="MsoNormal">Thu, 3 Sep 2020 18:06:46 +0000<o:p></o:p></p>
                </td>
              </tr>
              <tr>
                <td style="padding:0cm 0cm 0cm 0cm" valign="top"
                  nowrap="nowrap">
                  <p class="MsoNormal" style="text-align:right"
                    align="right"><b>From: <o:p></o:p></b></p>
                </td>
                <td style="padding:0cm 0cm 0cm 0cm">
                  <p class="MsoNormal">Thorsten Altenkirch <a
                      href="mailto:Thorsten.Altenkirch@nottingham.ac.uk"
                      moz-do-not-send="true">
                      <Thorsten.Altenkirch@nottingham.ac.uk></a><o:p></o:p></p>
                </td>
              </tr>
              <tr>
                <td style="padding:0cm 0cm 0cm 0cm" valign="top"
                  nowrap="nowrap">
                  <p class="MsoNormal" style="text-align:right"
                    align="right"><b>To: <o:p></o:p></b></p>
                </td>
                <td style="padding:0cm 0cm 0cm 0cm">
                  <p class="MsoNormal">Manuel Bärenz <a
                      href="mailto:manuel@enigmage.de"
                      moz-do-not-send="true"><manuel@enigmage.de></a><o:p></o:p></p>
                </td>
              </tr>
            </tbody>
          </table>
          <p class="MsoNormal" style="margin-bottom:12.0pt"><o:p> </o:p></p>
          <p class="MsoNormal"><span style="mso-fareast-language:EN-US">Yes,
              this puzzled me as well first.
            </span><o:p></o:p></p>
          <p class="MsoNormal"><span style="mso-fareast-language:EN-US"> </span><o:p></o:p></p>
          <p class="MsoNormal"><span style="mso-fareast-language:EN-US">What
              is meant is that if you know r=i1 where r is any
              expression then A i = A j for any i,j : I.</span><o:p></o:p></p>
          <p class="MsoNormal"><span style="mso-fareast-language:EN-US">Then
              transp A r a : A i1</span><o:p></o:p></p>
          <p class="MsoNormal"><span style="mso-fareast-language:EN-US"> </span><o:p></o:p></p>
          <p class="MsoNormal"><span style="mso-fareast-language:EN-US">You
              need this because if =i1 then transp A r a = a, but the
              lhs is in A i0 and the rhs is in A i1.</span><o:p></o:p></p>
          <p class="MsoNormal"><span style="mso-fareast-language:EN-US"> </span><o:p></o:p></p>
          <p class="MsoNormal"><span style="mso-fareast-language:EN-US">Thorsten</span><o:p></o:p></p>
          <p class="MsoNormal"><span style="mso-fareast-language:EN-US"> </span><o:p></o:p></p>
          <div style="border:none;border-top:solid #B5C4DF
            1.0pt;padding:3.0pt 0cm 0cm 0cm">
            <p class="MsoNormal"><b><span
                  style="font-size:12.0pt;color:black">From: </span></b><span
                style="font-size:12.0pt;color:black">Agda
                <a href="mailto:agda-bounces@lists.chalmers.se"
                  moz-do-not-send="true"><agda-bounces@lists.chalmers.se></a>
                on behalf of Manuel Bärenz
                <a href="mailto:manuel@enigmage.de"
                  moz-do-not-send="true"><manuel@enigmage.de></a><br>
                <b>Date: </b>Thursday, 3 September 2020 at 18:51<br>
                <b>To: </b><a href="mailto:agda@lists.chalmers.se"
                  moz-do-not-send="true">"agda@lists.chalmers.se"</a> <a
                  href="mailto:agda@lists.chalmers.se"
                  moz-do-not-send="true">
                  <agda@lists.chalmers.se></a><br>
                <b>Subject: </b>[Agda] Question about transport and
                cubical</span><o:p></o:p></p>
          </div>
          <div>
            <p class="MsoNormal"> <o:p></o:p></p>
          </div>
          <p>Hi,<o:p></o:p></p>
          <p>I'm just reading the docs on Agda's Cubical TT support, and
            stumbled over this:<o:p></o:p></p>
          <pre><span class="nf"><span style="color:#A30C0C">transp</span></span><span style="color:#A30C0C"> <span class="ow">:</span> </span><span class="ow"><span style="font-family:"Cambria Math",serif;color:#A30C0C">∀</span></span><span style="color:#A30C0C"> <span class="o">{</span>ℓ<span class="o">}</span> <span class="o">(</span>A <span class="ow">:</span> I <span class="ow">→</span> <span class="kt">Set</span> ℓ<span class="o">)</span> <span class="o">(</span>r <span class="ow">:</span> I<span class="o">)</span> <span class="o">(</span>a <span class="ow">:</span> A i0<span class="o">)</span> <span class="ow">→</span> A i1</span><o:p></o:p></pre>
          <p><span style="color:#A30C0C">There is an additional side
              condition to be satisfied for
            </span><span class="pre"><span
                style="font-size:10.0pt;font-family:"Courier New
                ;color:#A30C0C",serif">transp</span></span><code><span
                style="font-size:10.0pt;color:#A30C0C">
              </span></code><span class="pre"><span
                style="font-size:10.0pt;font-family:"Courier New
                ;color:#A30C0C",serif">A</span></span><code><span
                style="font-size:10.0pt;color:#A30C0C">
              </span></code><span class="pre"><span
                style="font-size:10.0pt;font-family:"Courier New
                ;color:#A30C0C",serif">r</span></span><code><span
                style="font-size:10.0pt;color:#A30C0C">
              </span></code><span class="pre"><span
                style="font-size:10.0pt;font-family:"Courier New
                ;color:#A30C0C",serif">a</span></span><span
              style="color:#A30C0C"> to type-check, which is that
            </span><span class="pre"><span
                style="font-size:10.0pt;font-family:"Courier New
                ;color:#A30C0C",serif">A</span></span><span
              style="color:#A30C0C"> has to be
              <em><span
                  style="font-family:"Calibri",sans-serif">constant</span></em>
              on </span>
            <span class="pre"><span
                style="font-size:10.0pt;font-family:"Courier New
                ;color:#A30C0C",serif">r</span></span><span
              style="color:#A30C0C">. This means that
            </span><span class="pre"><span
                style="font-size:10.0pt;font-family:"Courier New
                ;color:#A30C0C",serif">A</span></span><span
              style="color:#A30C0C"> should be a constant function
              whenever the constraint
            </span><span class="pre"><span
                style="font-size:10.0pt;font-family:"Courier New
                ;color:#A30C0C",serif">r</span></span><code><span
                style="font-size:10.0pt;color:#A30C0C">
              </span></code><span class="pre"><span
                style="font-size:10.0pt;font-family:"Courier New
                ;color:#A30C0C",serif">=</span></span><code><span
                style="font-size:10.0pt;color:#A30C0C">
              </span></code><span class="pre"><span
                style="font-size:10.0pt;font-family:"Courier New
                ;color:#A30C0C",serif">i1</span></span><span
              style="color:#A30C0C"> is satisfied.
            </span><o:p></o:p></p>
          <p><a
href="https://agda.readthedocs.io/en/v2.6.1/language/cubical.html#transport"
              moz-do-not-send="true">https://agda.readthedocs.io/en/v2.6.1/language/cubical.html#transport</a><o:p></o:p></p>
          <p>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.<o:p></o:p></p>
          <p>Probably I'm just misunderstanding something basic.<o:p></o:p></p>
          <p>Best regards, Manuel<o:p></o:p></p>
          <pre>This message and any attachment are intended solely for the addressee<o:p></o:p></pre>
          <pre>and may contain confidential information. If you have received this<o:p></o:p></pre>
          <pre>message in error, please contact the sender and delete the email and<o:p></o:p></pre>
          <pre>attachment. <o:p></o:p></pre>
          <pre><o:p> </o:p></pre>
          <pre>Any views or opinions expressed by the author of this email do not<o:p></o:p></pre>
          <pre>necessarily reflect the views of the University of Nottingham. Email<o:p></o:p></pre>
          <pre>communications with the University of Nottingham may be monitored <o:p></o:p></pre>
          <pre>where permitted by law.<o:p></o:p></pre>
          <pre><o:p> </o:p></pre>
          <pre><o:p> </o:p></pre>
          <pre><o:p> </o:p></pre>
        </div>
      </div>
      <pre>
This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.



</pre>
    </div>
  </body>
</html>