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 -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.