The Coq mailing list

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

I forgot to put in a reference to Martin's paper

@article{hofmann1996conservativity,
  title={{Conservativity of equality reflection over intensional type 
theory}},
  author={Hofmann, M.},
  journal={Types for Proofs and Programs},
  pages={153--164},
  year={1996},
  publisher={Springer}
}

If you are subscribed to Springer you can download it from 
http://www.springerlink.com/content/y26jp374t0147505/

Thorsten

On 20 Oct 2010, at 09:58, Thorsten Altenkirch wrote:

> 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