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

[Ignat Insarov]

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>