<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
See also Pfenning's paper about "Intensionality, Extensionality, and
Proof Irrelevance in Modal Type Theory":<br>
<a class="moz-txt-link-freetext" href="https://www.cs.cmu.edu/~fp/papers/lics01.pdf">https://www.cs.cmu.edu/~fp/papers/lics01.pdf</a><br>
<br>
<div class="moz-cite-prefix">On 06.09.22 12:45, Apostolis
Xekoukoulotakis wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CAFEV_-jC5_6GxdEMKicib8ySJxn4V0RimdFzfiCLjv9+fJ7Y-g@mail.gmail.com">
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
<div dir="ltr">
<div>I was thinking that something that can not be shown
definitionally equal by the type checker does not tell us
anything about whether it is propositionally equal or not. ( I
was assuming that this would be the way to encode
"definitional" equality in Agda)<br>
</div>
<div><br>
</div>
<div>But now I understand your point. Any data structure that
would indicate that two functions are intensionally distinct
would be impossible since extensionally equal functions are
equal in cubical theory.</div>
<div><br>
</div>
<div>Thus we would be able to show that a function f is
intensionally distinct with itself.<br>
</div>
<div><br>
</div>
</div>
<br>
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">On Tue, Sep 6, 2022 at 12:36
AM Thorsten Altenkirch <<a
href="mailto:Thorsten.Altenkirch@nottingham.ac.uk"
moz-do-not-send="true" class="moz-txt-link-freetext">Thorsten.Altenkirch@nottingham.ac.uk</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>
<div>
<div>
<div dir="ltr">How does this matter?</div>
</div>
<div id="m_8699128748558656276ms-outlook-mobile-signature">
<div><br>
</div>
Get <a href="https://aka.ms/o0ukef" target="_blank"
moz-do-not-send="true">Outlook for iOS</a></div>
</div>
<hr style="display:inline-block;width:98%">
<div id="m_8699128748558656276divRplyFwdMsg" dir="ltr"><font
style="font-size:11pt" face="Calibri, sans-serif"
color="#000000"><b>From:</b> Apostolis Xekoukoulotakis
<<a href="mailto:apostolis.xekoukoulotakis@gmail.com"
target="_blank" moz-do-not-send="true"
class="moz-txt-link-freetext">apostolis.xekoukoulotakis@gmail.com</a>><br>
<b>Sent:</b> Monday, September 5, 2022 8:35:28 PM<br>
<b>To:</b> Thorsten Altenkirch (staff) <<a
href="mailto:psztxa@exmail.nottingham.ac.uk"
target="_blank" moz-do-not-send="true"
class="moz-txt-link-freetext">psztxa@exmail.nottingham.ac.uk</a>><br>
<b>Cc:</b> Ignat Insarov <<a
href="mailto:kindaro@gmail.com" target="_blank"
moz-do-not-send="true" class="moz-txt-link-freetext">kindaro@gmail.com</a>>;
<a href="mailto:agda@lists.chalmers.se" target="_blank"
moz-do-not-send="true" class="moz-txt-link-freetext">agda@lists.chalmers.se</a>
<<a href="mailto:agda@lists.chalmers.se"
target="_blank" moz-do-not-send="true"
class="moz-txt-link-freetext">agda@lists.chalmers.se</a>><br>
<b>Subject:</b> Re: [Agda] «Extensionally but not
definitionally equal» — can I say that?</font>
<div> </div>
</div>
<div>
<div dir="ltr"><i>I think that one missing piece of
information here is that the fact that you cant prove
that two things are equal doesnt not mean that they
are not equal.</i><br>
</div>
<br>
<div>
<div dir="ltr">On Mon, Sep 5, 2022 at 12:38 PM Thorsten
Altenkirch <<a
href="mailto:Thorsten.Altenkirch@nottingham.ac.uk"
target="_blank" moz-do-not-send="true"
class="moz-txt-link-freetext">Thorsten.Altenkirch@nottingham.ac.uk</a>>
wrote:<br>
</div>
<blockquote style="margin:0px 0px 0px
0.8ex;border-left:1px solid
rgb(204,204,204);padding-left:1ex">
<div>
<div lang="EN-GB">
<div>
<p><span>No you cannot distinguish extensionally
equal object in type theory. Otherwise
extensionality as provided by cubical agda
would be inconsistent. This is a feature,
not a bug.</span></p>
<p><span> </span></p>
<p><span>If you want to talk about intensional
aspects of functions you need to talk about
function codes not functions. That is you
need to implement a representation of
functions that reveals the intensional
aspects you want to talk about. In your case
you may want to use a monad (I think it is
called the writer monad) which counts the
number of steps and then work in this monad.
</span></p>
<p><span> </span></p>
<p><span>Cheers,</span></p>
<p><span>Thorsten</span></p>
<p><span> </span></p>
<div style="border-color:rgb(181,196,223)
currentcolor currentcolor;border-style:solid
none none;border-width:1pt medium
medium;padding:3pt 0cm 0cm">
<p
style="margin-right:0cm;margin-bottom:12pt;margin-left:36pt">
<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" moz-do-not-send="true"
class="moz-txt-link-freetext">agda-bounces@lists.chalmers.se</a>>
on behalf of Ignat Insarov <<a
href="mailto:kindaro@gmail.com"
target="_blank" moz-do-not-send="true"
class="moz-txt-link-freetext">kindaro@gmail.com</a>><br>
<b>Date: </b>Saturday, 3 September 2022
at 10:45<br>
<b>To: </b><a
href="mailto:agda@lists.chalmers.se"
target="_blank" moz-do-not-send="true"
class="moz-txt-link-freetext">agda@lists.chalmers.se</a>
<<a
href="mailto:agda@lists.chalmers.se"
target="_blank" moz-do-not-send="true"
class="moz-txt-link-freetext">agda@lists.chalmers.se</a>><br>
<b>Subject: </b>[Agda] «Extensionally but
not definitionally equal» — can I say
that?</span></p>
</div>
<div>
<p style="margin-left:36pt">Hello!<br>
<br>
Suppose I have two definitions of addition —
one works on Peano<br>
numbers and the other works in binary
representation. Can I express in<br>
Agda that these two definitions are
extensionally equal but<br>
definitionally distinct?<br>
<br>
Ideally in the future I want to proceed to
reasoning about their<br>
asymptotic performance (linear versus
logarithmic). So, I want to have<br>
several notions of equality, finer than the
commonly postulated<br>
functional extensionality.<br>
<br>
The way I imagine this could go is by
reifying the definition of said<br>
functions as a syntactic tree or another
appropriate encoding of the<br>
way Agda sees them. Then I should say «these
two functions are<br>
extensionally equal × their representation
as syntactic trees is<br>
distinct». Is this realistic? Are there
other approaches?<br>
<br>
See also on Zulip:<br>
<<a
href="https://agda.zulipchat.com/#narrow/stream/238741-general/topic/Extensionally.20but.20not.20definitionally.20equal.20.E2.80.94.20can.20I.20say.20that.3F/near/296889550"
target="_blank" moz-do-not-send="true"
class="moz-txt-link-freetext">https://agda.zulipchat.com/#narrow/stream/238741-general/topic/Extensionally.20but.20not.20definitionally.20equal.20.E2.80.94.20can.20I.20say.20that.3F/near/296889550</a>><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se"
target="_blank" moz-do-not-send="true"
class="moz-txt-link-freetext">Agda@lists.chalmers.se</a><br>
<a
href="https://lists.chalmers.se/mailman/listinfo/agda"
target="_blank" moz-do-not-send="true"
class="moz-txt-link-freetext">https://lists.chalmers.se/mailman/listinfo/agda</a></p>
</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>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se"
target="_blank" moz-do-not-send="true"
class="moz-txt-link-freetext">Agda@lists.chalmers.se</a><br>
<a
href="https://lists.chalmers.se/mailman/listinfo/agda"
rel="noreferrer" target="_blank"
moz-do-not-send="true"
class="moz-txt-link-freetext">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div>
</blockquote>
</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>
</blockquote>
</div>
<br>
<fieldset class="moz-mime-attachment-header"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<br>
</body>
</html>