The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

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