<div dir="ltr">I'm not sure either what the author of this page meant by "A has to be constant on r". Perhaps it is just poor wording but it doesn't make sense to me either. It doesn't appear in the original Cubical Agda paper.<div><br></div><div>If you ignore that everything else seems fine, though. The key point is that when r = i1 then transp must satisfy the additional constraint that "transp A i1 a = a" for all "a" and when r = i0 there is no additional constraint.</div><div><br></div><div>John</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Sep 3, 2020 at 10:51 AM 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>Hi,</p>
    <p>I'm just reading the docs on Agda's Cubical TT support, and
      stumbled over this:</p>
    <pre><font color="#a30c0c"><span>transp</span> <span>:</span> <span>∀</span> <span>{</span>ℓ<span>}</span> <span>(</span>A <span>:</span> I <span>→</span> <span>Set</span> ℓ<span>)</span> <span>(</span>r <span>:</span> I<span>)</span> <span>(</span>a <span>:</span> A i0<span>)</span> <span>→</span> A i1
</font></pre>
    <font color="#a30c0c">
    </font>
    <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>
        has to be <em>constant</em> on
        <code><span>r</span></code>.</font><font color="#a30c0c"> This means 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><a href="https://agda.readthedocs.io/en/v2.6.1/language/cubical.html#transport" target="_blank">https://agda.readthedocs.io/en/v2.6.1/language/cubical.html#transport</a></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.</p>
    <p>Probably I'm just misunderstanding something basic.<br>
    </p>
    <p>Best regards, Manuel<br>
    </p>
  </div>

_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>