# [Agda] More universe polymorphism

Martin Escardo m.escardo at cs.bham.ac.uk
Tue Jul 2 23:31:35 CEST 2013

```
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

```