[Agda] Universe polymorphism

[Peter Hancock]

On Sat, 26 Sep 2009, at 12:51, Nils Anders Danielsson wrote:
>
> data Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
>   _,_ : (x : A) (y : B x) → Σ A B
>

That's quite interesting: you don't allow the b in Set b to depend
on x : A.  Suppose you did, so that the type of the Sigma quantifier
is
    (a : Level) ->
    (A : Set a) ->
    (b : El a A -> Level) ->
    (B : (x : El a A) -> Set (b x)) ->
    Set (sup_a A b)

where

    sup : (a : Level)->
          (A : Set a)->
          (El a A -> Level)-> Level

    El a A is just A if you prefer a la Russell.

This makes the levels something like a W-type, which seems as reasonable
an idea as any.
(I had wondered why it should not be the signed integers, or the  
rationals, ...)

Personally, I think that universes are hairy enough that they are best
programmed explicitly, as Set-indexed families of Sets/Functors/ 
Whatever.
That is, they should be internal universes of Set = Set0.  I haven't
ever felt the need for Set2, though Set1 is very convenient.
I don't think Agda should provide automation for weird towers of
universes over Set0.

Hank