[Agda] More universe polymorphism

[Martin Escardo]

On 28/06/13 22:04, Martin Escardo wrote:
> I show below that, in the presense of universe levels, there is an
> Agda type that doesn't have any Agda type.

I should have written:

   I show below that, in the presence of a *type* of universe levels,
   there is an Agda type that doesn't have any Agda type.

There is nothing wrong with universe levels, but rather with a *type* of 
universe levels. This should be clear from what I say in the long
message, but I wanted to clarify this to speed-of-light readers.

Martin