The Coq mailing list

[Steve Zdancewic <stevez AT cis.upenn.edu>]

Hi everyone,

Is there a technical reason why there is no extensional equality 
principle for function types?  The base library has surjective pairing 
for products, but nothing like this axiom:

Axiom extensionality : forall (A:Set) (B:Set) (f:A->B)(g:A ->B),
  (forall x:A, f x = g x) -> f = g.

Connor McBride's recent post (in the thread "Cannot Rewrite Under 
Lambda") indicates that it is not possible to prove this as a lemma, but 
does adding this axiom lead to inconsistencies?

Thanks,

Steve Zdancewic
Dept. Computer and Information Science
University of Pennsylvania