[Agda] «Extensionally but not definitionally equal» — can I say that?

[Andreas Nuyts]

See also Pfenning's paper about "Intensionality, Extensionality, and 
Proof Irrelevance in Modal Type Theory":
https://www.cs.cmu.edu/~fp/papers/lics01.pdf

On 06.09.22 12:45, Apostolis Xekoukoulotakis wrote:
> 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)
>
> 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.
>
> Thus we would be able to show that a function f is intensionally 
> distinct with itself.
>
>
> On Tue, Sep 6, 2022 at 12:36 AM Thorsten Altenkirch 
> <Thorsten.Altenkirch at nottingham.ac.uk> wrote:
>
>     How does this matter?
>
>     Get Outlook for iOS <https://aka.ms/o0ukef>
>     ------------------------------------------------------------------------
>     *From:* Apostolis Xekoukoulotakis
>     <apostolis.xekoukoulotakis at gmail.com>
>     *Sent:* Monday, September 5, 2022 8:35:28 PM
>     *To:* Thorsten Altenkirch (staff) <psztxa at exmail.nottingham.ac.uk>
>     *Cc:* Ignat Insarov <kindaro at gmail.com>; agda at lists.chalmers.se
>     <agda at lists.chalmers.se>
>     *Subject:* Re: [Agda] «Extensionally but not definitionally equal»
>     — can I say that?
>     /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./
>
>     On Mon, Sep 5, 2022 at 12:38 PM Thorsten Altenkirch
>     <Thorsten.Altenkirch at nottingham.ac.uk> wrote:
>
>         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.
>
>         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.
>
>         Cheers,
>
>         Thorsten
>
>         *From: *Agda <agda-bounces at lists.chalmers.se> on behalf of
>         Ignat Insarov <kindaro at gmail.com>
>         *Date: *Saturday, 3 September 2022 at 10:45
>         *To: *agda at lists.chalmers.se <agda at lists.chalmers.se>
>         *Subject: *[Agda] «Extensionally but not definitionally equal»
>         — can I say that?
>
>         Hello!
>
>         Suppose I have two definitions of addition — one works on Peano
>         numbers and the other works in binary representation. Can I
>         express in
>         Agda that these two definitions are extensionally equal but
>         definitionally distinct?
>
>         Ideally in the future I want to proceed to reasoning about their
>         asymptotic performance (linear versus logarithmic). So, I want
>         to have
>         several notions of equality, finer than the commonly postulated
>         functional extensionality.
>
>         The way I imagine this could go is by reifying the definition
>         of said
>         functions as a syntactic tree or another appropriate encoding
>         of the
>         way Agda sees them. Then I should say «these two functions are
>         extensionally equal × their representation as syntactic trees is
>         distinct». Is this realistic? Are there other approaches?
>
>         See also on Zulip:
>         <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>
>         _______________________________________________
>         Agda mailing list
>         Agda at lists.chalmers.se
>         https://lists.chalmers.se/mailman/listinfo/agda
>
>         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.
>
>
>
>         _______________________________________________
>         Agda mailing list
>         Agda at lists.chalmers.se
>         https://lists.chalmers.se/mailman/listinfo/agda
>
>     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.
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20220906/df6b41d3/attachment-0001.html>