<html>
  <head>

    <meta http-equiv="content-type" content="text/html; charset=UTF-8">
  </head>
  <body>
    <p>I'm still confused. r doesn't influence the type of a in the
      expression transp A r a. If it was <br>
    </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></pre>
    <div class="moz-forward-container"><br>
    </div>
    <div class="moz-forward-container">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 --------
      <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] Question about transport and cubical</td>
          </tr>
          <tr>
            <th valign="BASELINE" nowrap="nowrap" align="RIGHT">Date: </th>
            <td>Thu, 3 Sep 2020 18:06:46 +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;}
/* 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.EmailStyle28
        {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">Yes,
            this puzzled me as well first.
            <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">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.<o:p></o:p></span></p>
        <p class="MsoNormal"><span style="mso-fareast-language:EN-US">Then
            transp A r a : A i1<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">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.<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 18:51<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] Question about transport and
              cubical<o:p></o:p></span></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<o:p></o:p></span></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">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">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">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">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">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">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">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">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">=</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">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>
      </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>