On 01/05/2019 03:50, Michael Shulman wrote:> Interesting point!  I definitely agree that we don't want to be

> *forced* to be typically ambiguous; there are times when we need to

> explicitly distinguish universes.  This was already the case in a few

> places in the book, e.g. Lemmas 10.3.21 and 10.3.22.  And Coq's

> universe polymorphism now also *allows* the user to explicitly specify

> universe levels when desired.  (On the other hand, it's also nice to

> not be forced to label all universes explicitly all the time.  But on

> the third hard, at least in Coq as it is now, the interaction of

> user-specified universes with automatically-deduced ones seems to be

> fairly fragile.)

Right.

> However, it's not clear to me why cumulativity would be a problem.

In Agda each type gets a unique universe (or at most one universe) and

often (but not always) the system is able to infer them if we write

question marks "?" for them (but not always).

Cumulativity is not "on the nose" in the sense that from X : U_l you

would get X : U_m for m ≥ l. Instead, if you need to have (a copy of)

X in U_m, you need to use an explicit embedding U_l → U_m. (I only

ever used this embedding to show that U_l is a retract of U_m if we

assume propositional resizing.)

In practice, however, I never needed to use this embedding, as the

closure properties for universes work with more than one universe at a

time. For instance,

  if X:U_l and A : X → U_m, then Π X A : U_{max l m}.

With this kind of closure property, I haven't encountered the

practical need for cumulativity.

It is nice, in practice, that universes are uniquely

determined. Insted of thousands of level constraints, we have a

unique, small, (polymorphic) level assignment.

> In fact you wrote in the paper that "We don't assume that the

> universes are cumulative... but we also don't assume that they are

> not".  Which makes it sound as though cumulativity, though not

> necessary, wouldn't be a problem if it did hold -- would it?

In theory it wouldn't be a problem if it holds. However, if Agda did

have cumulativity, it would lose the unique-level assignment property

that I use to infer the levels of the results from my given levels of

the data. However, in the absence of a concrete proof assistant with

the option to enable and disable cumulativity, it is impossible to

perform experiments to confirm or reject this conjectural impression.

I consider the universe-level system of Agda to be excellent in

practice, and easy to use. Moreover, as I said, if I publish a

mathematical theorem developed in Agda, I think it is fair to the

reader to let them know what the universe level assignments are rather

than just say that they exist. In some cases, as injectivity, the

universe levels are crucial, and if we ignore them we get false

claims.

Best,

Martin