Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Is nat in Type_0?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Is nat in Type_0?


chronological Thread 
  • From: Lionel Elie Mamane <lionel AT mamane.lu>
  • To: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] Is nat in Type_0?
  • Date: Mon, 11 Nov 2002 10:50:05 +0100
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Wed, Nov 06, 2002 at 12:39:25PM +0100, Lionel Elie Mamane wrote:

> If I look, e.g. at the description of CIC in "Sets in Types, Types
> in Sets" from Benjamin Werner, there is an explicit rule, called
> Cum-Prop, that says "if A:Prop, then A:Type_i".

> But looking at the typing rules, page 72/73 of the Reference Manual
> (section 4.2, paragraph "Typing Rules"), I don't see any
> justification for it

> So, how, from the rules in the manual, does Coq infer something like
> Benjamin Werner's "Cum-Prop"?

For the sake of the archives, here is the answer I got from Benjamin
GREGOIRE 
<Benjamin.Gregoire AT inria.fr>:

If you look section (4.3) you will see a other rule : Conversion Rule.
In fact, a subtype rule:
                   E |- t : T   E |- U : s     E |- T <= U
                 ---------------------------------------------- (CONV)
                                  E |- t : U
we have |- Set <= Type(i)   and |- Prop <= Type(i).

-- 
Lionel

Attachment: pgpLt6bCDf4yL.pgp
Description: PGP signature




Archive powered by MhonArc 2.6.16.

Top of Page