coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] two related questions

From: Vladimir Voevodsky <vladimir AT ias.edu>
To: Coq Club <coq-club AT inria.fr>
Cc: Vladimir Voevodsky <vladimir AT ias.edu>
Subject: [Coq-Club] two related questions
Date: Mon, 18 Oct 2010 17:02:28 -0400

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)?

Vladimir.

[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