The Coq mailing list

[Yasuaki Kudo <yasu AT yasuaki.com>]

Thank you, this is also very helpful and I think I now have better 
understanding.  Let me continue to read my coq art book - I may have more 
questions again :-).  Yasuaki 

> On Aug 2, 2015, at 14:18, 
> 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
>