coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Herman Geuvers <herman AT cs.ru.nl>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Prop vs Type
- Date: Thu, 15 Nov 2012 10:27:22 +0100
Hi,
That's a nice proof Hugo. I was wondering whether one could show _directly_ that there is a retract from Prop into a small type, from the assumption that Prop = Type.
BTW the link in the Coq StdLib to my note on this is wrong; it should be
http://www.cs.ru.nl/~herman/PUBS/newnote.ps.gz
Best
Herman Geuvers
On 11/15/2012 04:30 AM, Hugo Herbelin wrote:
Hi,
Attached is a proof relying on Hurkens' paradox (not without pain)!
Hugo
On Thu, Nov 15, 2012 at 12:16:52AM +0100, Andreas Abel wrote:
You could try to adopt Hurkens' Paradox (inconsistency of Prop :
Prop). I do not know whether it will work, because under the
assumption
H : Type = Prop
you only get something like
cast H Prop : Prop
but it might work nevertheless.
Andreas
On 14.11.12 4:15 PM, Daniel Schepler wrote:
On Tue, Nov 13, 2012 at 4:54 PM, Jonas Oberhauser
<s9joober AT gmail.com>
wrote:
Can I prove
Goal Prop <> Type.
In coq?
Kind regards,
Jonas
Well, Prop has impredicative constructions, which in Type would lead
to contradictions. That's where I'd start looking for something to
distinguish between the two. Though I couldn't immediately think of
any way to exploit this...
--
Andreas Abel <>< Du bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.abel AT ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
- [Coq-Club] Prop vs Type, Jonas Oberhauser, 11/14/2012
- Re: [Coq-Club] Prop vs Type, AUGER Cédric, 11/14/2012
- Re: [Coq-Club] Prop vs Type, Daniel Schepler, 11/14/2012
- Re: [Coq-Club] Prop vs Type, Andreas Abel, 11/15/2012
- Re: [Coq-Club] Prop vs Type, Hugo Herbelin, 11/15/2012
- Re: [Coq-Club] Prop vs Type, Herman Geuvers, 11/15/2012
- Re: [Coq-Club] Prop vs Type, Hugo Herbelin, 11/15/2012
- Re: [Coq-Club] Prop vs Type, Andreas Abel, 11/16/2012
- Re: [Coq-Club] Prop vs Type, Herman Geuvers, 11/15/2012
- Re: [Coq-Club] Prop vs Type, Hugo Herbelin, 11/15/2012
- Re: [Coq-Club] Prop vs Type, Andreas Abel, 11/15/2012
- <Possible follow-up(s)>
- Re: [Coq-Club] Prop vs Type, Hugo Herbelin, 11/16/2012
Archive powered by MHonArc 2.6.18.