The Coq mailing list

[Randy Pollack <rpollack AT inf.ed.ac.uk>]

If one wants to think about PTSs, Dan's answer is the most useful: use
axioms and rules about (infinitely many) sorts to represent your
universe structure.  This was folklore in the 1980s.

As mentioned, Luo suggested the cumulative type hierarchy (ECC) which
solves an infelicity in simply stacking universes on top of one
another.  See my TCS paper with Bob Harper for a description of this
infelicity.

Perhaps close to answering Vladimir's actual question: In my thesis I
give a formulation of a slight generalization of PTS where the
beta-conversion relation is replaced by an abstract relation that is
only axiomatized to have the properties necessary to develop the basic
theory of PTS, including a type checking algorithm.  I show how Luo's
cumulative type hierarchy is in fact a functional instance of this
extended notion of PTS, and give a machine checked proof of
decidability of typechecking (only assuming normalization, which I did
not prove).

If one is interested in real subtyping in the PTS framework (which I
think is straying from Vladimir's original question), there is other
work to look at: Adriana Compagnoni (particularly recent work with
Healf Goguen) and Jan Zwanenburg (PhD thesis from Nijmegen).  The real
story on subtyping in type theory for purposes of representing
mathematics is probably Luo's coercive subtyping.

There are few misleading parts to Dan's message.  Every normalizing
PTS with a finite set of sorts has decidable typechecking, whether it
be functional or not (due to Bert Jutting).  Clearly non-normalizing
PTS can't always be decidable.  On the other hand I showed a
functional, normalizing PTS that is undecidable (see my thesis).  The
point is that the halting problem is trivially coded by typechecking
of a PTS using the naturals for its set of sorts. For the full
excrutiating story on typechecking algorithms for PTS see my paper
with Bert Jutting and Jjames McKinna.  Eric Poll has an earlier paper
on typechecking in the lambda cube.

Randy
--
On Thu, Jun 16, 2011 at 6:15 PM, Robert Harper 
<rwh AT cs.cmu.edu>
 wrote:
> Yes, Luo's ECC (Extended Calculus of Constructions) studied such universe 
> inclusions.
>
> Bob
>
> (sent from handheld)
>
> On Jun 16, 2011, at 14:55, Vladimir Voevodsky 
> <vladimir AT ias.edu>
>  wrote:
>
>> 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.
>>
>>
>> --
>> You received this message because you are subscribed to the Google Groups 
>> "Homotopy Type Theory" group.
>> To post to this group, send email to 
>> HomotopyTypeTheory AT googlegroups.com.
>> To unsubscribe from this group, send email to 
>> HomotopyTypeTheory+unsubscribe AT googlegroups.com.
>> For more options, visit this group at 
>> http://groups.google.com/group/HomotopyTypeTheory?hl=en.
>>
>
>
>