<div dir="ltr">Thorsten's explanation is good. Just ignore the phrase " A has to be constant on r". Everything else makes sense. If you want to know why there is this additional condition, read the Cubical Agda paper.<div><br></div><div>John</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Sep 3, 2020 at 11:12 AM Manuel Bärenz <<a href="mailto:manuel@enigmage.de">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>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><span style="color:rgb(163,12,12)">transp</span></span><span style="color:rgb(163,12,12)"> <span>:</span> </span><span><span style="font-family:"Cambria Math",serif;color:rgb(163,12,12)">∀</span></span><span style="color:rgb(163,12,12)"> <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 r</span></pre>
<div><br>
</div>
<div>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 cellspacing="0" cellpadding="0" border="0">
<tbody>
<tr>
<th valign="BASELINE" nowrap align="RIGHT">Subject:
</th>
<td>Re: [Agda] Question about transport and cubical</td>
</tr>
<tr>
<th valign="BASELINE" nowrap align="RIGHT">Date: </th>
<td>Thu, 3 Sep 2020 18:06:46 +0000</td>
</tr>
<tr>
<th valign="BASELINE" nowrap align="RIGHT">From: </th>
<td>Thorsten Altenkirch
<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk" target="_blank"><Thorsten.Altenkirch@nottingham.ac.uk></a></td>
</tr>
<tr>
<th valign="BASELINE" nowrap align="RIGHT">To: </th>
<td>Manuel Bärenz <a href="mailto:manuel@enigmage.de" target="_blank"><manuel@enigmage.de></a></td>
</tr>
</tbody>
</table>
<br>
<br>
<div>
<p class="MsoNormal"><span>Yes,
this puzzled me as well first.
<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal"><span>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.<u></u><u></u></span></p>
<p class="MsoNormal"><span>Then
transp A r a : A i1<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal"><span>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.<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal"><span>Thorsten<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<div style="border-right:none;border-bottom:none;border-left:none;border-top:1pt solid rgb(181,196,223);padding:3pt 0cm 0cm">
<p class="MsoNormal"><b><span style="font-size:12pt;color:black">From: </span></b><span style="font-size:12pt;color:black">Agda
<a href="mailto:agda-bounces@lists.chalmers.se" target="_blank"><agda-bounces@lists.chalmers.se></a> on behalf of Manuel
Bärenz <a href="mailto:manuel@enigmage.de" target="_blank"><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" target="_blank">"agda@lists.chalmers.se"</a>
<a href="mailto:agda@lists.chalmers.se" target="_blank"><agda@lists.chalmers.se></a><br>
<b>Subject: </b>[Agda] Question about transport and
cubical<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<p>Hi,<u></u><u></u></p>
<p>I'm just reading the docs on Agda's Cubical TT support, and
stumbled over this:<u></u><u></u></p>
<pre><span><span style="color:rgb(163,12,12)">transp</span></span><span style="color:rgb(163,12,12)"> <span>:</span> </span><span><span style="font-family:"Cambria Math",serif;color:rgb(163,12,12)">∀</span></span><span style="color:rgb(163,12,12)"> <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<u></u><u></u></span></pre>
<p><span style="color:rgb(163,12,12)">There is an additional side
condition to be satisfied for
</span><span><span>transp</span></span><code><span style="font-size:10pt;color:rgb(163,12,12)">
</span></code><span><span>A</span></span><code><span style="font-size:10pt;color:rgb(163,12,12)">
</span></code><span><span>r</span></span><code><span style="font-size:10pt;color:rgb(163,12,12)">
</span></code><span><span>a</span></span><span style="color:rgb(163,12,12)"> to type-check, which is that
</span><span><span>A</span></span><span style="color:rgb(163,12,12)"> has to be
<em><span style="font-family:Calibri,sans-serif">constant</span></em>
on </span>
<span><span>r</span></span><span style="color:rgb(163,12,12)">. This means that
</span><span><span>A</span></span><span style="color:rgb(163,12,12)"> should be a constant function
whenever the constraint
</span><span><span>r</span></span><code><span style="font-size:10pt;color:rgb(163,12,12)">
</span></code><span><span>=</span></span><code><span style="font-size:10pt;color:rgb(163,12,12)">
</span></code><span><span>i1</span></span><span style="color:rgb(163,12,12)"> is satisfied.
</span><u></u><u></u></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><u></u><u></u></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.<u></u><u></u></p>
<p>Probably I'm just misunderstanding something basic.<u></u><u></u></p>
<p>Best regards, Manuel<u></u><u></u></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>
</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>