<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
</head>
<body>
<p>Thanks Thorsten for the extended explanation. I think I now
understand that the point is that we might call transp in a
situation where A is an expression that may contain r.</p>
<p>Taking John's advice to ignore that phrase, I look at the
following:<br>
</p>
<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> 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>One part of the confusion was probably that I thought about A as
a closed expression, since there is a binding of the same name
directly before in the type signature. But in this sentence, A is
meant to be any expression, and it may contain r as a free
variable.<br>
</p>
<p>I still don't understand what's meant by <span class="pre"><span
style="font-size:10.0pt;font-family:"Courier New
;color:#A30C0C",serif">A</span></span><span
style="color:#A30C0C"> should be a constant function</span>. Who
checks that? Obviously the semantics of A has to be constant,
after all that's the point behind cubical type theory, isn't it?
So I guess it must mean that the sort-of-lambda-expression must be
a constant function in that it doesn't depend on its argument. Is
Cubical Agda able to check whether functions of type I -> Set
are constant? How does the check work? λ _ . A is constant, but is
λ i . (λ _ . A) i constant for that matter? Or does it normalize A
i0 and A i1 and then tries to unify them?<br>
</p>
<div class="moz-forward-container">I realize that this is maybe not
the place to discuss articles. But I believe it's the right place
to talk about the documentation of the language. During ICFP I got
the impression that I'm not the only one struggling with an
intuitive understanding of how to use Cubical Agda. Keeping the
documentation understandable is important to improve that.
Especially on an intricate topic like equality reasoning,
confusing wording can be an obstruction. For example:</div>
<div class="moz-forward-container"><br>
</div>
<div class="moz-forward-container"><font color="#a30c0c">However
when <code class="docutils literal notranslate"><span
class="pre">r</span></code> is equal to <code
class="docutils literal notranslate"><span class="pre">i1</span></code>
the
<code class="docutils literal notranslate"><span class="pre">transp</span></code>
function will compute as the identity function.</font></div>
<div class="moz-forward-container"><br>
</div>
<div class="moz-forward-container">At the end, doesn't transp A i
always compute as the identity function? Isn't the point of
transport to just verify that two types are equal so we can safely
coerce? I believe I can sort of see what the argument is intending
to say, it's more like "transp A i1 must be able to have the type
{B : Set l} -> B -> B, so in the branch where transp is
called with r = i1 we must have that A is constantly B.", but I
might be misunderstanding this again.<br>
</div>
<div class="moz-forward-container"><br>
</div>
<div class="moz-forward-container">It is sometimes said that HoTT
solves the problem of equality, but it seems to me more like that
it pushes the problem to documentation and conversation, because
we don't have good words to talk about the different kinds of
equality.</div>
<div class="moz-forward-container"><br>
</div>
<div class="moz-forward-container">If I can make sense of this all,
I'll try and improve this part of the docs.<br>
</div>
<div class="moz-forward-container"><br>
</div>
<div class="moz-forward-container">-------- 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] Fwd: Question about transport and cubical</td>
</tr>
<tr>
<th valign="BASELINE" nowrap="nowrap" align="RIGHT">Date: </th>
<td>Thu, 3 Sep 2020 18:28:07 +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;}
@font-face
{font-family:"Courier New \;color\:\#A30C0C";
panose-1:2 7 3 9 2 2 5 2 4 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.EmailStyle29
{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">Ok,
we now have equational assumptions like r=i1 where r is some
expression of type I. For example a variable like i.<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">Now
the type A also uses “r” and you can check that if r==i1
then A is constant. It may contain a match on r and if r=i1
then the branch doesn’t mention the paremeter.<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">This
is a requirement for the expression “transp A r a” to
typecheck. E.g. in my example it would be transp A i a which
has the type A i1. Assuming r=i1 it is equal to a : A i0.
But this deosn’t matter because of the condition on A. <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">I
think the best way to understand this is to start proving
something about transp and then to write down each step of
the derivation in a comment. Then you realize why you need
it.<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 19:12<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] Fwd: Question about transport and
cubical<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<p>I'm still confused. r doesn't influence the type of a in the
expression transp A r a. If it was
<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 r</span><o:p></o:p></pre>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">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 -------- <o:p></o:p></p>
<table class="MsoNormalTable" cellspacing="0" cellpadding="0"
border="0">
<tbody>
<tr>
<td style="padding:0cm 0cm 0cm 0cm" valign="top"
nowrap="nowrap">
<p class="MsoNormal" style="text-align:right"
align="right"><b>Subject: <o:p></o:p></b></p>
</td>
<td style="padding:0cm 0cm 0cm 0cm">
<p class="MsoNormal">Re: [Agda] Question about
transport and cubical<o:p></o:p></p>
</td>
</tr>
<tr>
<td style="padding:0cm 0cm 0cm 0cm" valign="top"
nowrap="nowrap">
<p class="MsoNormal" style="text-align:right"
align="right"><b>Date: <o:p></o:p></b></p>
</td>
<td style="padding:0cm 0cm 0cm 0cm">
<p class="MsoNormal">Thu, 3 Sep 2020 18:06:46 +0000<o:p></o:p></p>
</td>
</tr>
<tr>
<td style="padding:0cm 0cm 0cm 0cm" valign="top"
nowrap="nowrap">
<p class="MsoNormal" style="text-align:right"
align="right"><b>From: <o:p></o:p></b></p>
</td>
<td style="padding:0cm 0cm 0cm 0cm">
<p class="MsoNormal">Thorsten Altenkirch <a
href="mailto:Thorsten.Altenkirch@nottingham.ac.uk"
moz-do-not-send="true">
<Thorsten.Altenkirch@nottingham.ac.uk></a><o:p></o:p></p>
</td>
</tr>
<tr>
<td style="padding:0cm 0cm 0cm 0cm" valign="top"
nowrap="nowrap">
<p class="MsoNormal" style="text-align:right"
align="right"><b>To: <o:p></o:p></b></p>
</td>
<td style="padding:0cm 0cm 0cm 0cm">
<p class="MsoNormal">Manuel Bärenz <a
href="mailto:manuel@enigmage.de"
moz-do-not-send="true"><manuel@enigmage.de></a><o:p></o:p></p>
</td>
</tr>
</tbody>
</table>
<p class="MsoNormal" style="margin-bottom:12.0pt"><o:p> </o:p></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">Yes,
this puzzled me as well first.
</span><o:p></o:p></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"> </span><o:p></o:p></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.</span><o:p></o:p></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">Then
transp A r a : A i1</span><o:p></o:p></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"> </span><o:p></o:p></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.</span><o:p></o:p></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"> </span><o:p></o:p></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">Thorsten</span><o:p></o:p></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"> </span><o:p></o:p></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 href="mailto:agda-bounces@lists.chalmers.se"
moz-do-not-send="true"><agda-bounces@lists.chalmers.se></a>
on behalf of Manuel Bärenz
<a href="mailto:manuel@enigmage.de"
moz-do-not-send="true"><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"
moz-do-not-send="true">"agda@lists.chalmers.se"</a> <a
href="mailto:agda@lists.chalmers.se"
moz-do-not-send="true">
<agda@lists.chalmers.se></a><br>
<b>Subject: </b>[Agda] Question about transport and
cubical</span><o:p></o:p></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</span><o:p></o:p></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",serif">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",serif">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",serif">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",serif">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",serif">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",serif">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",serif">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",serif">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",serif">=</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",serif">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>
<pre>This message and any attachment are intended solely for the addressee<o:p></o:p></pre>
<pre>and may contain confidential information. If you have received this<o:p></o:p></pre>
<pre>message in error, please contact the sender and delete the email and<o:p></o:p></pre>
<pre>attachment. <o:p></o:p></pre>
<pre><o:p> </o:p></pre>
<pre>Any views or opinions expressed by the author of this email do not<o:p></o:p></pre>
<pre>necessarily reflect the views of the University of Nottingham. Email<o:p></o:p></pre>
<pre>communications with the University of Nottingham may be monitored <o:p></o:p></pre>
<pre>where permitted by law.<o:p></o:p></pre>
<pre><o:p> </o:p></pre>
<pre><o:p> </o:p></pre>
<pre><o:p> </o:p></pre>
</div>
</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>