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

Ignat Insarov kindaro at gmail.com
Sat Sep 3 11:46:11 CEST 2022


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:

More information about the Agda mailing list