The Coq mailing list

[Frederic Blanqui <frederic.blanqui AT inria.fr>]

Unfortunately, no. There is no general theory of PTS's with subtyping yet.

The only general work I know about typed lambda calculus and subtyping 
is Gang Chen's PhD on the calculus of constructions (so, only two 
universes):

@PhdThesis{chen98phd,
  author =      {G. Chen},
  title =      {Subtyping, Type Conversion and Transitivity Elimination},
  school =      {Universit\'e Paris VII, France},
  year =      1998}

See also:

@ARTICLE{castagna01ic,
AUTHOR    = {G. Castagna and G. Chen},
TITLE    = {Dependent types with subtyping and late-bound overloading},
JOURNAL    = {Information and Computation},
YEAR    = {2001},
VOLUME    = {168},
NUMBER    = {1},
PAGES    = {1-67}}

Frederic.


Le 17/06/2011 05:55, Vladimir Voevodsky a écrit :
> 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.