The Coq mailing list

[Adam Chlipala <adamc AT cs.berkeley.edu>]

Pierre Casteran wrote:

> Hi,
>  Notice that your definitions make False, True, 0 <> 1 being 
> inhabitants of Type (with some index >0), and
> not plain propositions (i.e. of type Prop( at its turn of type Type(0)).
> Check (True:Prop).
> Toplevel input, characters 837-841
> > Check (True:Prop).
> >        ^^^^
> Error: The term "True" has type "Type" while it is expected to have type
> "Prop"

Is this really a problem?  In my long journey towards understanding the 
metatheory of Coq, I've come to explain to myself the distinction among 
Set/Prop/Type as only being necessary to support extraction.  Do you 
really need more than the different levels of Type if you're only 
interested in checking proofs in the simplest possible calculus?