The Coq mailing list

[Vincent Siles <vincent.siles AT ens-lyon.org>]

Your right, there is not structure on the universes of PTS, which is
actually their strenght:
the interesting point about PTS is this "lack" of structure about the
universes, you can have multiple results without choosing the relation
between the universes (like subject reduction, strenghthening,
confluence...
I have a quick survey of these results in my phd thesis, but I don't
consider subtyping).
If you are interested by particular instances of PTS with subtyping,
you should take a look at Luo's Extended Calculus of Constructions or
Goguen's UTT.
The type theory behind Agda2 might also be of some interest.

Cheers,
Vincent


2011/6/16 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.
>
>
>
>