The Coq mailing list

[Dan Doel <dan.doel AT gmail.com>]

On Monday 13 September 2010 9:05:42 am Randy Pollack wrote:

> It seems that Agda has some experimental feature of explicit
> (outermost?) quantification over universe levels that should be looked
> into.

I don't know what you mean by "outermost". But yes, it's quite simple to 
encode T in Agda:

  data T (i : Level) : Set (suc i) where
    t : Set i -> T i

  u : forall i -> T (suc i)
  u i = t (T i)

I can even make the indices implicit so it'll look weird:

  data T {i : Level} : Set (suc i) where
    t : Set i -> T

  u : forall {i} -> T {suc i}
  u = t T

I'm not sure how the Aczel set theory thing would work out. I suspect it 
would 
fail earlier, or you'd only be able to prove that R i \in R (suc i) 
(depending 
on how R was defined).

Level is almost an ordinary type---there's a little compiler support for 
normalizing expressions like 'lub x x' to 'x' even for open terms; I think 
this is in part due to Agda totaly lacking cumulativity, so lubs of multiple 
levels variables need to be used instead of implicitly lifting everything 
involved to a single level. Also, I believe the rule for universe polymorphic 
functions is adequately described by:

  if U[x] : Set S, where x is free in S
  then ((x : T) -> U[x]) : Setω

Where ω is not itself a Level (and thus Setω is not itself of the form Set i 
for some i : Level, which would probably be paradoxical).

This stuff isn't remotely well-established theoretically as far as I know, 
though. At least, it's novel with respect to all the published papers I've 
seen on universe polymorphism. So I could understand people being reluctant 
to 
put it in Coq at this point.

-- Dan