The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi all,

  Indeed it is less useful in presence of polymorphism, but not completely useless still,

if it can go through inductive types (examples in the work of Timany on a category theory 

library suggest that). Ali Assaf's thesis is indeed the most up-to-date comparison for universes

with and without cumulativity I think. I think there is an advantage of cumulativity in the presence of 

polymorphism (or just lots of universes) regarding unifying universe expressions, which are relegated 

to the constraint inference engine. E.g. you don't get into problems like max(i,j) =? max(i',j') that have 

no canonical solutions but instead get two fresh universes l and l' representing these two lubs and l = l'.

Best,

-- Matthieu

On Mon, Mar 13, 2017 at 3:57 PM Bas Spitters <b.a.w.spitters AT gmail.com> wrote:

Interestingly, the lean developers (in CC) have decided against
cumulative universes.
IIRC cumulativity complicates the implementation and the meta-theory,
but *in the presence of universe polymorphism* it does not add much
extra convenience.

Unfortunately, I cannot find a discussion of the rationale, but
someone will fill us in, I hope.


On Mon, Mar 13, 2017 at 3:00 PM, Frédéric Blanqui
<frederic.blanqui AT inria.fr> wrote:
> Hi Grégory, you may be interested in Ali Assaf's PhD thesis:
> https://pastel.archives-ouvertes.fr/tel-01235303v4 .
>
>
> Le 03/13/2017 à 02:51 PM, Gregory Malecha a écrit :
>
> Hi, Coq-Club --
>
> I'm wondering if anyone can point me to literature related to cumulatively
> vs. non-cumulatibity of universes. My vague understanding is that
> cumulatively offers no additional power but that there are some things that
> are easier to express with cumulative universes (in particular you can avoid
> resizing in terms). Cobstructivwly, I would expect such a result to give a
> translation from a world with cumulative universes to one without them. A
> paper on that topic would be particularly interesting to me.
>
> Thanks in advance for any pointers.
> --
>
> - gregory malecha
>   gmalecha.github.io
>
>