The Coq mailing list

[yasu AT yasuaki.com]

Hi,

Thank you, this helps a lot!   On page 38, 2.5.2 Universes in 
Interactive Theorem Proving and Program Development, it says:

Level 0: programs and basic values
Level 1: specifications and data types
Level 2: the Set sort
Level 3: the universe Type(0)
Level i+3: the universe Type(i)


Where is Prop in this, Level 2?

Cheers,
Yasuaki



On 01.08.2015 22:40, Gabriel Scherer wrote:
> Prop and Set are two universes of types, and Prop is included in Set.
> The different can be felt in various ways, including:
> - a value in Prop can be seen as a value in Set (but the converse is 
> not true)
> - the rules to build terms whose type is in Prop are stricter than
> those to build terms whose type is in Set (constructions by
> case-distinction are restricted if you want to create a Prop)
> - quantifying on all types in Prop is a "small quantification" (the
> resulting polymorphic type is itself in Prop), while quantifying on
> all types in Set (it quantifies on more things) is a "large
> quantification" (the resulting polymorphic type lives in a strictly
> larger universe)
>
>
> I think this should be explained in most documents teaching Coq -- in
> a section on the universe hierarchy.
>
> On Sat, Aug 1, 2015 at 2:56 PM,  
> <yasu AT yasuaki.com>
>  wrote:
> > Hi,
> >
> > I am currently learning COQ. Why is the sequence below valid?   Are 
> > Prop and
> > Set terms interchangable?
> >
> > Variable n : Prop.
> > Variable f : Set -> nat.
> > Check (f n).
> >
> >    f n : nat
> >
> >
> > Regards,
> > Yasuaki