[Agda] More universe polymorphism

[Guillaume Brunerie]

Le 27 juin 2013 01:01, "Andreas Abel" <andreas.abel at ifi.lmu.de> a écrit :
>
> A minor reason for small level is Agda's built-in mechanism, where a Level is a built-in postulate
>
>   Level : Set
>
> Of course, this reason is minor because we could just have pragma
>
>   {-# BUILTIN LEVEL Level #-}
>
> without postulating Level first.
>
> I don't think there is any theoretical reason why Level should be small.  Your suggested level supremum
>
>   sup : {i : Level}{A : Set i} (j : A -> Level) -> Level
>
> could interpreted as "constructor" with the usual structural ordering
>
>   j a <= sup j.
>
> What would be an application for transfinite levels?

No idea, it just seems less ad-hoc than the current restriction and
not more difficult to implement (and hopefully consistent).
For instance it gives some kind of replacement: every small collection
of small things is small (which is not the case in Agda currently
because the sequence of the first omega universes is a small
collection of small things which is not small).

Maybe there will be a problem with equality between levels not being
well-behaved, though…

Cheers,
Guillaume

> Cheers,
> Andreas
>
>
>
> On 26.06.13 9:14 PM, Guillaume Brunerie wrote:
>>
>> Hi all,
>>
>> Quick recall of Agda’s universe polymorphism:
>>
>> There is a type Level of universe levels together with the following constants:
>>
>> zero : Level
>> suc : Level -> Level
>> max : Level -> Level -> Level
>>
>> For every i : Level, there is a universe Set i, which is also a term
>> of type Set (suc i).
>> A dependent product (x : A) -> B x such that A : Set i and B x : Set j
>> for all x : A is of type Set (max i j) (note that j cannot depend on
>> x, it has to be uniform).
>> Moreover, the type of universe levels Level is itself small (of type Type zero).
>>
>>
>> Why is Level required to be small?
>>
>> If we drop this requirement, it seems to me that we could extend max
>> so that we can get the maximum of any small family of universe levels,
>> i.e. have some max2 of type:
>>
>> max2 : (i : Level) (A : Set i) (j : A -> Level) -> Level
>>
>> Then a dependent product (x : A) -> B x where A : Set i and B x : Set
>> (j x) would be of type Set (max2 i A j), so there is no "uniformity of
>> levels" restriction anymore, the only restriction is that the domain
>> and the codomain(s) are small.
>> You need the condition that Level is not small, or else you would be
>> able to define the max of all levels, which is likely to cause some
>> trouble.
>>
>> Such universe polymorphism would permit to define a lot of new
>> universes, indexed by a lot of big countable ordinals (maybe up to the
>> Feferman–Schütte ordinal?)
>>
>> Does that make sense? Is that consistent?
>> Did I miss something obvious?
>> I think there was something requiring Level to be small, but I don’t
>> remember what it is.
>>
>> Guillaume
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Theoretical Computer Science, University of Munich
> Oettingenstr. 67, D-80538 Munich, GERMANY
>
> andreas.abel at ifi.lmu.de
> http://www2.tcs.ifi.lmu.de/~abel/