Basic questions on polymorphic universes

Using Rocq
1

Hi guys, trying to understand polymorphic universes (still in Coq 8.18)…

In the example below, why does the first attempt at defining IRel fail, despite the second and successful attempt looks to me equivalent?

Otherwise, is there any way to define IRel in terms of IOp? – Can I say, more generally, any way to instantiate a universe parameter of a universe-polymorphic definition with the Prop universe?

And, if not, as the error message seems to suggest, is it just some internal limitation of Coq compelling the duplication of definitions, or is it also conceptually (type-theoretically maybe) for some reason that my first attempt at IRel is ill-conceived?

Thanks in advance for any insight as well as technical suggestion or correction.

Set Printing Universes.
Set Universe Polymorphism.

Definition IOp@{i n o} (T : Type@{i}) : Type@{o} :=
  T -> T -> Type@{n}.
(*
  IOp@{i n o} =
  fun T : Type@{i} => T -> T -> Type@{n}
       : Type@{i} -> Type@{o}
  (* i n o |= n < o
              i <= o *)
*)

Check Type@{Prop}.
(* Prop : Type@{Set+1} *)

Fail Definition IRel@{i o} (T : Type@{i}) : Type@{o} :=
  IOp@{i Prop o} T.
(*
  The command has indeed failed with message:
  Universe instances cannot contain non-Set small levels,
  polymorphic universe instances must be greater or equal to Set.
*)

Definition IRel@{i o} (T : Type@{i}) : Type@{o} :=
  T -> T -> Type@{Prop}.  (* elaborated(?) to [T -> T -> Prop] *)
(*
  IRel@{i o} =
  fun T : Type@{i} => T -> T -> Prop
       : Type@{i} -> Type@{o}
  (* i o |= Set < o
            i <= o *)
*)
2

Maybe that question doesn’t make much sense. The fact is, I have been studying the topic, from the refman to several articles and video lectures, and it all seems quite clear and even simple conceptually, but as soon as I start writing code, in the detail of the code, I immediately have a million doubts.

Here are few preliminary questions:

  1. As I get it, universe-polymorphic is about types, not terms: i.e. when we use a term, the universe level we instantiate it at is the universe level of its type. (Correct?)

  2. Can I think of “universe” as synonym with “sort”, i.e. the various Type_i (and Prop)? And u-polymorphism as “just” a way to parametrize definitions (their types) on the sort levels (i.e. level constraints)?

  3. IIANM, we have cumulativity of sorts built-in, i.e. Type_i : Type_j for all j > i. Why do we need a flag Polymorphic Inductive Cumulativity? And why only for co-/inductive types? [But there’s already a mistake: that is not what cumulativity means…]

3

Or, for example, take this:

Structure WSet@{i o} : Type@{o} :=
  mkWSet { wset :> Type@{i} }.
(*
  Record WSet@{i o} : Type@{o} :=
    mkWSet { wset : Type@{i} }.
  (* i o |= i < o *)
*)

Structure WSet' : Type :=
  mkWSet' { wset' :> Type; }.
(*
  Record WSet'@{u} : Type@{u+1} :=
    mkWSet' { wset' : Type@{u} }.
  (* u |=  *)
*)

OTOH, the default here is the other way round (u instead of u0+1):

Definition WType' : Type := Type.
(*
  WType'@{u u0} = Type@{u0} : Type@{u}
  (* u u0 |= u0 < u *)
*)

Can anyone explain 1) why the defaults are different; and, maybe more importantly, 2) what is the difference between WSet and WSet’ (I mean, why would one want to prefer one over the other)? In the presence or not of (inductive?) cumulativity?