[Agda] eta expansion

[Martin Escardo]

Actually, I do have something similar to what you suggest, and eta is 
happening. I will try to condense the example and then post it here.

Thanks for the other replies.

On 08/03/13 15:46, Peter Hancock wrote:
> 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
>
>
>