[Agda] Pointwise function equality

[Thorsten Altenkirch]

On 30 Nov 2010, at 09:40, Dominique Devriese wrote:

> Hi all,
> 
> I hope someone here can help me with another Agda beginner's question.
> The following seems useful and intuitively makes sense to me, but I am
> not sure if this is sound and if/where/how it fits in the
> in-/extensionality range.
> 
>  postulate pointwise : ∀ {l} {A B : Set l} {f₁ : A → B} {f₂ : A → B}
> → ((x : A) → f₁ x ≡ f₂ x) → f₁ ≡ f₂
> 
> Can anyone here shed some light on this and/or provide interesting references?
> 
> Thanks in advance,
> Dominique
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

Hi Dominique,

indeed, the lack of extensionality in Agda is most annoying and many of the Agda developers would like to fix it. In the moment all you can do is add a postulate as you suggest, which has the disadvantage that it destroys "canonicity", i.e. there are closed terms which don't reduce to values because their normalisation is stopped by the postulate (which I would call ext, btw). Apart from this it is sound and even better you can prove all the theorems of "extensional type theory", which uses "equality reflection", that is any proof of an equality can be magically turned into a definitional equality and used during typechecking. This has been shown by Martin-Hofmann ("Conservativity of Equality Reflection over Intensional Type Theory"), and I also recommend his PhD thesis ("Extensional Concepts in Type Theory"). 

I have written a paper a while ago showing that if you have proof-irrelevant universe of propositions you can translate a type theory with extensionality into one without ("Extensional Equality in Intensional Type Theory", LICS 99). However, this wasn't a good base for an implementation, so more recently with Conor McBride and others we developed "Observational Type Theory" which is currently being implemented as part of the Epigram 2 system (I hope), this is based on our PLPV 07 paper (with Wouter Swierstra) "Observational Equality, Now!".  In particular this approach addresses the issue of canonicity for sets.

Cheers,
Thorsten