[Agda] More universe polymorphism

[Martin Escardo]

On 28/06/13 22:04, Martin Escardo wrote:
> Moreover, ignoring the above, explicit universe levels as in Agda are
> painful, to the extent that some people (e.g. Dan Licata and Mike
> Shulman in their LICS'2013 paper in Agda) prefer to use type-in-type
> to achieve universe polymorphism, checking themselves by *hand* that
> there is a consistent universe level assignment for everything they
> write down in Agda.

Before this interesting thread fades away, I would like to pose the 
following question.

Of course, type-in-type is inconsistent. However, both in lectures and 
in personal conversations, Thierry Coquand pointed out some interesting, 
consistent, uses of Type:Type. We can add the above, by Dan and Mike.

I am not sure how to formulate the question (before knowing the answer), 
but here it goes. Rough attempt: can we precisely formulate consistent 
uses of type-in-type? (An example is Dan and Mike's LICS paper.)

A more detailed attempt: define a type "Level" *inductively* (using data 
in Agda). Then inductively define the property that an element of a 
given type "has some level" (again using Agda's data, where you are 
allowed to be daring in your kind of induction, but you are required to 
be strictly positive).

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.

Conjecture: if you define "has some level" properly, and if your proof 
has some level, then your proof is a bonafide proof. Example: Dan and 
Mike's proof should "have some level".

Open problem: It is possible to formulate the question more precisely 
and answer it positively? In particular, in such a way that e.g. Dan and 
Mike's paper pass the test (as it should) ?

Caveat: the question is not precisely formulated, and any answer would 
need a reformulation. In essence, the problem is to give criteria to 
detect bonafide uses of type-in-type via a type of levels. This is not 
what Guillaume asked originally in the thread, and not a proposal to 
adopt type-in-type, but rather to understand when it works.

Martin