coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Cumulatively of Universes

From: Gregory Malecha <gmalecha AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] Cumulatively of Universes
Date: Mon, 13 Mar 2017 13:51:54 +0000
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gmalecha AT gmail.com; spf=Pass smtp.mailfrom=gmalecha AT gmail.com; spf=None smtp.helo=postmaster AT mail-ua0-f169.google.com
Ironport-phdr: 9a23:cgwaXR/W3hfET/9uRHKM819IXTAuvvDOBiVQ1KB42uscTK2v8tzYMVDF4r011RmSDNidtq4P1reempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9ZDeZwVFiCC9bL59Ixm7rQXcvdQKjIV/Lao81gHHqWZSdeRMwmNoK1OTnxLi6cq14ZVu7Sdete8/+sBZSan1cLg2QrJeDDQ9LmA6/9brugXZTQuO/XQTTGMbmQdVDgff7RH6WpDxsjbmtud4xSKXM9H6QawyVD+/9KpgVgPmhzkbOD446GHXi9J/jKRHoBK6uhdzx5fYbJyJOPZie6/Qe84RS2hcUcZLTyFODYOyYYUMAeQcI+hXs5LwqEESoRakHwSgGP/jxz1Oi3Tr3aM6yeMhEQTe0QIhBdIBrnvUrNLvNKYSTOu7y7PHzTHdYPxK2Tfy8pXDfxcuofGJR71wddTexlUvFwzflViQponlMCmU1uQJqWSU8+1gVee2hmMhtgp/rD+vxsI2hYnIgIIY0l/E9SRlwIY1ON23U1R3Yd+jEJZWqiqUNJN2T9s8T210vCs20L4LtJ6hcCQU1ZgqxQTTZ+GGfoWM5B/oSfyfLi1ihH1/fbKynxay/lakyu37TsS01UxFritBktXVq3ACzQDf5tGJSvdg/0qs3SyD1w/U6uFDLkA0kbTUJ4Q9zb43k5ofqUXDHinol0XqlKKaaFko9+yy5+nkYrjqvIGQO5J2hw3kL6gjm8iyDfw9MgcUXmib/eq81Kfk/U38WLhKgfg2nbPdsJ/EOcsbprS2DhRa0oYm8Rm/DjOm3M4EknkAKVJJYAiHgJTxO1HSPPD4Cu+yjEirkDdy3vzJIrnhAojWIXXYi7fgfbN961ZGxwYpzNBf4YhUCrAbL/7pVE/xro+QMhhsGAuti83jFd81gogZQCeEBrKTGKLUq16BoOw1dbqifogQ7RnnJvci/e+mqHY9lFQddOH90p4ebH2zHv1OLECQYH6qidAERzRZ9jEiRfDn3QXRGQVYYGy/Cudlvmk2

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

[Coq-Club] Cumulatively of Universes, Gregory Malecha, 03/13/2017
- Re: [Coq-Club] Cumulatively of Universes, Frédéric Blanqui, 03/13/2017
  - Re: [Coq-Club] Cumulatively of Universes, Bas Spitters, 03/13/2017
    - Re: [Coq-Club] Cumulatively of Universes, Matthieu Sozeau, 03/13/2017
      - Re: [Coq-Club] Cumulatively of Universes, Gregory Malecha, 03/13/2017
  - Re: [Coq-Club] Cumulatively of Universes, Jason Gross, 03/13/2017