Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


chronological Thread 
  • From: Robert Harper <rwh AT cs.cmu.edu>
  • To: "homotopytypetheory AT googlegroups.com" <homotopytypetheory AT googlegroups.com>
  • Cc: "homotopytypetheory AT googlegroups.com" <homotopytypetheory AT googlegroups.com>, Coq-Club Club <coq-club AT inria.fr>
  • Subject: [Coq-Club] Re: [HoTT] pure type systems (Barendregt)
  • Date: Thu, 16 Jun 2011 15:15:00 -0700
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.
> 


Archive powered by MhonArc 2.6.16.

Top of Page