[Agda] How does level polymorphism fit into a valid type theory? (from "More universe polymorphism")

[Darryl McAdams]

Do levels really have to be things at all? If we think of levels as merely/purely syntactic elements of the type theory, then it seems like the relational judgment "type_n" that Martin mentions would sidestep the issue entirely. Levels would no more exist in the model then ":" and "valid-context" do.
 
- darryl



________________________________
 From: Peter Hancock <hancock at spamcop.net>
To: agda at lists.chalmers.se 
Sent: Monday, July 1, 2013 2:30 PM
Subject: Re: [Agda] How does level polymorphism fit into a valid type theory? (from "More universe polymorphism")
 

On 01/07/2013 17:04, Martin Escardo wrote:
> Ok, I understand, Guillaume. The crucial thing, in your formulation
> below of transfinite universes, is that Level is a type but cannot
> live in a universe, right? (So it doesn't have a type.)

In set theory, ordinals (that index the cumuluative hierarchy)
form a class, just like sets.   So, they don't live in any universe,
at least not in the sense of a Grothendieck universe.  They are
"commensurate" with the notion of set itself.

The notion of "set" (or whatever you want to call it)
is inexpressible in Agda. That is why Martin-Lof (and G. Brunerie)
proposes a judgement form for it different from a : A.  If Agda
had the notion of set, by the same token, it would have a coherent
notion of level.

One hundred years ago, we had Principia mathematica, which was a
ramified theory, with "levels" (short circuited by reducibility,
but never mind).  Nobody knew what type they lived in, or what the
level of that type should be.  It seems to me that in 100 years,
we have travelled precisely nowhere.

Hank
_______________________________________________
Agda mailing list
Agda at lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130701/35736299/attachment.html