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

[Darryl McAdams]

That's a good point, yes. I wonder if there's a way to have level-pi types without being inconsistent then. probably not?

G, a level |-- A type a   ===>   G |- LPi a. A type ?n

This probably can't work, indeed.

- darryl



________________________________
 From: Guillaume Brunerie <guillaume.brunerie at gmail.com>
To: Darryl McAdams <psygnisfive at yahoo.com> 
Cc: Peter Hancock <hancock at spamcop.net>; "agda at lists.chalmers.se" <agda at lists.chalmers.se> 
Sent: Monday, July 1, 2013 3:16 PM
Subject: Re: [Agda] How does level polymorphism fit into a valid type theory? (from "More universe polymorphism")
 

Well, if you want to define a polymorphic function (polymorphic on all
small types, not restricted to some universe), you have to quantify
over all levels.
Or you can use typical ambiguity, but this is kind of cheating.
Maybe you could instead have a notion of universal quantification over
all universes which would be a primitive notion, distinct from the
usual Pi types. Various people were talking about that at the IAS this
year but I don’t know if anyone tried to write down the rules.

But if having a type of universe levels is consistent and natural and
pretty, I don’t see why we should try to avoid it.

Guillaume

2013/7/1 Darryl McAdams <psygnisfive at yahoo.com>:
> 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
>
>
>
> _______________________________________________
> 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/8c16804c/attachment-0001.html