The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

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