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

[Guillaume Brunerie]

On 2013/7/1 Darryl McAdams <psygnisfive at yahoo.com> wrote:
> 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.

Maybe I misunderstood your question but Agda already has level-pi
types without (I think) being inconsistent. It just happens that in
Agda level-pi types are ordinary Pi-types indexed by the type of
universe levels.

My point was that having level-pi types distinct from other Pi types
would complicate the type theory without bringing any obvious benefit.

> - 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
>>
>