coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Propositional extensionality is inconsistent in Coq

From: Robbert Krebbers <mailinglists AT robbertkrebbers.nl>
To: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
Cc: Maxime Dénès <mail AT maximedenes.fr>, coq-club AT inria.fr
Subject: Re: [Coq-Club] Propositional extensionality is inconsistent in Coq
Date: Fri, 13 Dec 2013 11:52:02 +1100

On 12/13/2013 10:23 AM, Pierre-Marie Pédrot wrote:

That's really surprising, to say the least... Is there a lot of
contributions using this axiom in the wild?

Cannot we prove

(False -> False) = True

using univalence? In that case, univalence would be inconsistent with the current version of Coq, which would be quite bad.

Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, (continued)
- Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, Maxime Dénès, 12/13/2013
- Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, Jacques-Henri Jourdan, 12/13/2013
  - Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, Matthieu Sozeau, 12/13/2013
    - Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, Jacques-Henri Jourdan, 12/13/2013
- Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, Jacques-Henri Jourdan, 12/14/2013
  - Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, AUGER Cédric, 12/14/2013