The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

> 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. 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.