coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Prop vs Type

From: Daniel Schepler <dschepler AT gmail.com>
To: Jonas Oberhauser <s9joober AT gmail.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Prop vs Type
Date: Wed, 14 Nov 2012 07:15:12 -0800

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

[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
- <Possible follow-up(s)>
- Re: [Coq-Club] Prop vs Type, Hugo Herbelin, 11/16/2012