The Coq mailing list

[Thorsten Altenkirch <txa AT Cs.Nott.AC.UK>]

Hi Vladimir,

> Hi, I have the following two questions:
> 
> Q.1 Is it  impossible to prove in Coq that any two functions from empty 
> type to empty type are equal ?
> 
> Q.2 Is it possible to preserve extraction after adding the functional 
> extensionality axiom ((forall x:X, f x = g x) -> f =g)?

People have already commented on this. Adding the axiom indeed preserves 
extraction but it interferes with the  computational behaviour of Type 
Theory: e.g. there are closed terms of type Nat which do not reduce to a 
numeral. This means that equalities which should hold definitionally have to 
be proven. However, this can be avoided, as we have shown in our paper 
"Observational Equality, now" 
(http://www.cs.nott.ac.uk/~txa/publ/obseqnow.pdf). This is going to be 
implemented i Epigram 2 (I hope).

Also Martin Hofmann has shown that extensional type theory is conservative 
over intensional type theory + ext + uip (uniqueness of identity proofs). It 
would be nice to have a similar result without uip. However, then we have to 
replace extensional type theory with something else ("univalent type theory" 
or as I call it "higher dimensional type theory"). We certainly need 
additional constants such as that the definable term 

        extinv : forall f  g : A -> B,  (f = g) -> forall a : A -> (f a = g a)

is inverse to ext. But this won't be enough.

Cheers,
Thorsten