The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

Hi Matej,

There are at least three sources of confusion in this thread.

1) < vs : (the difference was clearly explained in previous messages)
2) that there is no term of a given type in the current context does not
mean that the type has no inhabitants
3) inductive types *are* part of the core logic, and that's clear from
both the manual and the basic parts of the implementation (see constr.ml)

Maxime.

On 01/19/17 13:42, Matej Kosik wrote:
> On 01/19/2017 12:28 PM, Théo Zimmermann wrote:
>>
>>> I guess that you wanted to say "Prop is impredicative" and "Set is 
>>> predicative".
>>
>> Yes, this is what I meant, sorry. I regularly confuse the terminology.
>>
>>> after starting the toplevel like this:
>>>
>>>  coqtop -noinit
>>>
>>> neither Prop nor Set have any inhabitants
>>
>> I disagree. Inductive types are part of Coq's logic.
> 
> Where did you read that?
> (documentation? source code?)
> 
>> Even if you didn't declare any inductive type yet, all the inductive types 
>> that you could declare form part of the various universes. Inductive
>> types are not like axioms which, as long as you haven't introduced them, 
>> are not part of the logic.
>>
>>> Well, if you claim "Prop < Set", how can you say that "Set" is at the 
>>> bottom of the type hierarchy?
>>
>> I want to retract this. But then it really depends on whether we define 
>> the hierarchy based on < or on : (having a correspondence between the two 
>> would ease the reasoning but Bruno explained why we
>> don't want that).
>>
>> Going back to your initial question, Prop and Set are very specific 
>> universes but if you have some Type@{i} <= Type@{j} universe constraint, 
>> the constraint resolution algorithm should be able to solve
>> this by making Type@{i} = Type@{j}. In the case of Prop and Set, we 
>> clearly don't want that but, as I said, there seem to be other mechanisms 
>> to prevent it anyways.
> 
> Provided that you are wrong concerning your claim:
> 
>   Inductive types are part of Coq's logic.
>   Even if you didn't declare any inductive type yet, all the inductive 
> types that you could declare form part of the various universes.
>   Inductive types are not like axioms which, as long as you haven't 
> introduced them, are not part of the logic.
> 
> you make, I think, a wrong conclusion above.
>