The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

There are theorems which are expressible with and without cumulativity, but which require either function extensionality or judgmental reduction rules for lift and lower which may not be standard in a presentation with non-cumulative universes.  For example, in Coq with cumulative universes, we can define:
Definition Lift@{i j} (A : Type@{i}) : Type@{j} := A.
Definition lift@{i j} {A} (x : A) : Lift@{i j} A := x.
Definition lower@{i j} {A} (x : Lift@{i j} A) : A := x.
Lemma test@{i j} A : @lift@{i i} A = (fun x => x) /\ (fun x : A => lower@{i j} (lift@{i j} x)) = (fun x => x).
Proof. repeat constructor. Qed.

Are these provable in Agda without function extensionality?

On Mon, Mar 13, 2017, 10:00 AM 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