The Coq mailing list

[Lionel Elie Mamane <lionel AT mamane.lu>]

Hi,

I'm confused about the relation between the inhabitants of Set (and
Prop) and the Type(i) hierarchy.

In the Coq _implementation_, it is the case that if x:Set or x:Prop,
than x:Type(i) for some i (I strongly think it is any i)

Inductive Foo: Type:= Cons:Type->Foo.
Parameter A:Set.
Parameter P:Prop.

Now,

 Check (Cons P).
answers
 (Cons P)
     : Foo

and similarly "Check (Cons A)." says that (Cons A) is of type Foo.

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:

 - Ax gives Set:Type(q), but not nat:Type(q) or True:Type(p)
 - No other rule applies


So is this a documentation bug?

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


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


Thank you for your explanations,

-- 
Lionel

Attachment: pgpDcE8FCFVFu.pgp
Description: PGP signature