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

[Apostolis Xekoukoulotakis]

*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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20220905/7077448e/attachment.html>