<html>
  <head>

    <meta http-equiv="content-type" content="text/html; charset=UTF-8">
  </head>
  <body>
    <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 class="nf">transp</span> <span class="ow">:</span> <span class="ow">∀</span> <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
</font></pre>
    <font color="#a30c0c">
    </font>
    <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>
        has to be <em>constant</em> on
        <code class="docutils literal notranslate"><span class="pre">r</span></code>.</font><font
        color="#a30c0c"> This means 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><a class="moz-txt-link-freetext" href="https://agda.readthedocs.io/en/v2.6.1/language/cubical.html#transport">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>
  </body>
</html>