The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Vladimir Voevodsky wrote:
> Q.1 Is it  impossible to prove in Coq that any two functions from empty type 
> to empty type are equal ?
>    

I would assume this requires an extensionality axiom like below, but 
I'll wait for a more informed person to answer this part. :)

> Q.2 Is it possible to preserve extraction after adding the functional 
> extensionality axiom ((forall x:X, f x = g x) ->  f =g)?
>    

I think this poses no problems, because this axiom would live in the 
[Prop] universe (because of the use of [=]), and extraction erases 
everything in that universe, anyway.