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