The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

The core difference between Set and Prop is that Set contains
"programs" and Prop contains "proofs." I put those in quotes because
the two obviously get intermixed when doing Coq developments.

That chart seems somewhat misleading with respect to your current
question.  Basically, you have Set and Prop at level zero, and then
Type(i) at every i.  Prop admits proof irrelevance, leading to the
distinctions that Gabriel pointed out earlier.

Basically, I'd think about it as:

Prop -> Type(0) -> Type(1) -> Type(2) -> ...
Set   -^

This leads to a variety of pragmatic differences.  E.g., if you have a
sigma type { x | P } in Set, you actually can destruct and compute
with that x, but if you have a proof of the sum in Prop, `exists x, P
x`, you can't actually *use* that x, you are merely allowed to know
that one exists that satisfies that property.

Basically, things in Set are things you can compute with (e.g.,
destruct on) or observe.  Things in Prop are things you can use to
prove other things via (e.g.,) modus ponens.

Adam Chlipala's book has a good chapter on Universes from a pragmatic
perspective that might be more helpful to you:

http://adam.chlipala.net/cpdt/html/Universes.html

Type is a hierarchy of universes, you'll have to read that chapter to
get an intuitive understanding for what that means.  For most
practical purposes you don't need to worry about it, other than to
know about it.  The simple explanation is that if you didn't have it,
you'd be able to encode a type theoretic variant of Russell's paradox.
E.g., by having a Prop that quantifies over all Props.

Kris

On Sun, Aug 2, 2015 at 1:18 AM,  
<yasu AT yasuaki.com>
 wrote:
> 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