coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Is nat in Type_0?, Lionel Elie Mamane
- Re: [Coq-Club] Is nat in Type_0?, Lionel Elie Mamane
Archive powered by MhonArc 2.6.16.