The Coq mailing list

[Conor McBride <ctm AT cs.nott.ac.uk>]

Steve Zdancewic wrote:
> 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?

For a fairly comprehensive treatment of these issues, see Martin Hofmann's
PhD thesis 'Extensional concepts in intensional type theory'. But the
bottom line is that it's consistent to add extensionality. Intuitively,
this is because application is the only observation we can make on
functions. Correspondingly, there's no way you can construct a predicate
P on functions such that P f is inhabited and P g is empty when f and g
agree on all arguments: the only thing P can do with its function is
apply it.

You do lose the property that closed terms have canonical values. That is,
you can write a function weird : Nat -> Bool, such that weird 3 normalizes to
subst (extensionality f g ...) P b, rather than true or false. Moreover, if
the substitution 'predicate' P is sufficiently perverse, then P f, the type of
b might not be Bool, but rather some subst (extensionality ...) P' Bool, and
that's presume P' isn't too perverse. Some people find this inconvenient. It's
not obvious to me whether it's a serious obstacle either to 'proof irrelevant'
reasoning or to program extraction.

Cheers

Conor

--
http://www.cs.nott.ac.uk/~ctm