coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] JMeq_eq vs. UIP

From: Adam Chlipala <adam AT chlipala.net>
To: Christian Doczkal <doczkal AT ps.uni-sb.de>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] JMeq_eq vs. UIP
Date: Fri, 19 Mar 2010 08:27:46 -0400

Christian Doczkal wrote:

So is JMeq_eq is provable in Coq using UIP? Does anyone have a proof?

In Section 9.5 of CPDT (http://adam.chlipala.net/cpdt/), there is another take on what it means to answer this question. In particular, [JMeq] is defined in terms of [eq], and then the "axiom" is proved as a consequence of [UIP].

[Coq-Club] JMeq_eq vs. UIP, Christian Doczkal
- Re: [Coq-Club] JMeq_eq vs. UIP, Pierre Corbineau
- Re: [Coq-Club] JMeq_eq vs. UIP, Pierre Corbineau
- Re: [Coq-Club] JMeq_eq vs. UIP, Adam Chlipala