[Agda] More universe polymorphism

[Dan Licata]

Hi Martin,

How would using such a system be different than implicit universe
polymorphism, like was recently implemented in Coq?  It seems like a
difference in perspective---"all type:type programs are good programs,
but we can pick out the ones that level check", as opposed to "only the
level-checking programs are good, but the user can act as if type:type
and we can infer whether they do while type checking"---which could be
helpful for designing a tool.  But from the users' perspective, what
differences would you expect?  

>From a "how heavy is it to use" perspective, I think the main thing I
dislike about Agda's current solution is the lack of cumulativity.
Personally, I think types with lots of paramters look nicer if you just
have one level parameter, rather than one for each independent type, and
lots of "max"'es expressing the relationship between them.  
But I know there are issues with cumulativity in Coq.  

Alternatively, if Agda implicitly added quantifiers over dependencies
like Twelf does,, at least I wouldn't have to write and read the levels
as much.  In Twelf, if you have indices of a type that is reconstructed,
those indicies are also quantified over.  For example:

forall {A B} -> A -> B

would mean

forall {l1 l2 : Level} {A : Set l1} {B : Set l2} -> A -> B

Though I know there are difference that make this difficult (like being
able to supply implicit arguments explicitly in Agda).  So this is
really me complaining about the state of the art without having a solution...

-Dan

On Jul02, Martin Escardo wrote:
> NB. Their paper already passes the test, of the referees and mine and more 
> people - it is not in question. What is in question is whether there is a 
> general way of deciding whether uses of type-in-type are good as posed 
> above.

And Agda -- we have done a version of this proof without type:type :)