[Agda] eta expansion

[Peter Hancock]

On 08/03/2013 14:46, Martin Escardo wrote:
> Is it possible to disable the eta expansion for definitional equality in Agda?

If you define your own Pi-sets, as in Martin-Lof type theory, with eliminator
funsplit (as in the book by Smith et al. p 56) that can be used to define "ap"
(see the book), then you will not have eta (for functions) holding definitionally.
(It *will* hold wrt Id types.) A similar story for Sigma and its eta.

Of course, you will have to rewrite all your code to use these Pi-sets...
But you will have the benefit of being able to claim (with greater certainty)
that what you have done (whatever that is) could be done in Martin-Lof type-theory.
In essence you would be using a small fragment of Agda just as a logical framework.

Hank