The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

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