[Agda] More universe polymorphism

[Andreas Abel]

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?

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/