The Coq mailing list

[Herman Geuvers <herman AT cs.ru.nl>]

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/