coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Thorsten Altenkirch <txa AT Cs.Nott.AC.UK>
- To: Vladimir Voevodsky <vladimir AT ias.edu>
- Cc: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] two related questions
- Date: Wed, 20 Oct 2010 11:15:17 +0100
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
- [Coq-Club] two related questions, Vladimir Voevodsky
- Re: [Coq-Club] two related questions,
Adam Chlipala
- Re: [Coq-Club] two related questions, Conor McBride
- Re: [Coq-Club] two related questions,
Thorsten Altenkirch
- Re: [Coq-Club] two related questions, Thorsten Altenkirch
- [Coq-Club] a question,
Vladimir Voevodsky
- Re: [Coq-Club] a question, Adam Chlipala
- <Possible follow-ups>
- Re: [Coq-Club] two related questions, Benjamin Werner
- Re: [Coq-Club] two related questions,
Adam Chlipala
Archive powered by MhonArc 2.6.16.