The Coq mailing list

[Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com>]

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.
-- 
Matej Košík