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