The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi Herman,

> 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.

Good question. It is at least easy to define the coercion of Prop as a
small type of itself, but then I don't see right away how to define a
retract.
 
> 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

Thanks, I'll fix it.

Hugo

> 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/