Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] pure type systems (Barendregt)

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] pure type systems (Barendregt)


chronological Thread 
  • From: Matthieu Sozeau <matthieu.sozeau AT gmail.com>
  • To: Vladimir Voevodsky <vladimir AT ias.edu>
  • Cc: homotopytypetheory AT googlegroups.com, Coq-Club Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] pure type systems (Barendregt)
  • Date: Thu, 16 Jun 2011 15:21:33 -0700
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=subject:mime-version:content-type:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to:x-mailer; b=rdljg3sHoAWLMp4ZKEprd7CNuaZ43WCE40VJawpn3BY9651gC96AwAYhAEmucrwaw+ yMxpHdL4+Qos42c807p0rD4bdTPUYfwBG9V2+j/TYc3qtBUb7fI4Mvqm0xIFbL0OTKdY R4iagpv2cW0OaV7gDFAbE8DocMSBu35IB4Zqw=
Hi Vladimir,

  you are looking for PTSs with subtyping, of which ECC of Luo [1] is a prime 
example.
Subtyping of universes is called cumulativity in this case.

http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.38.7596

Cheers,
-- Matthieu

Le 16 juin 2011 à 14: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.
> 
> 
> 



Archive powered by MhonArc 2.6.16.

Top of Page