The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

Hello,

thank you very much for the answers to my question about Set. I'll  
have to think about it more but so far it confirms my feeling that I  
do not have to bother with Set while learning Coq.  At least not at  
first.

Here is another question. As explained in Coq documentation Type is  
actually an hierarchy of types and a member of Type(i) is a type  
which was defined without mentioning Type(j) for j>=i. Fine. But what  
if I have a member of a low level type which is defined using higher  
order universes? For example declare a variable P:Type -> Prop. Let's  
assume it was declared as going from some Type(i). I do not care  
which one. Consider now a:Prop := ex P. Coq tells me that it is well  
defined. Hence, I have a member of Prop which is defined using higher  
universes. This feels wrong.

Vladimir.