The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

I have been looking at Barendregt's "Lambda calculi with Types" and I have 
the following question. It seems that he is considering systems with 
different universe arrangements but he never assumes one universe to be a 
sub-universe of another. Is it so or am I missing something? And if this is 
so is there a careful analysis of the analog of PST's where universes are not 
only members but also subtypes of each other?

Thanks!
Vladimir.