# Basic questions on polymorphic universes

**URL:** <https://discourse.rocq-prover.org/t/basic-questions-on-polymorphic-universes/2586>\
**Category:** Using Rocq\
**Created:** [March 30, 2025, 6:58pm UTC](https://discourse.rocq-prover.org/t/basic-questions-on-polymorphic-universes/2586 "2025-03-30T18:58:58Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![jp-diegidio](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/jp-diegidio/32/819_2.png) [@jp-diegidio](https://discourse.rocq-prover.org/u/jp-diegidio)\
**Post date:** [March 30, 2025, 6:58pm UTC](https://discourse.rocq-prover.org/t/basic-questions-on-polymorphic-universes/2586/1 "2025-03-30T18:58:58Z")

</div>

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.

```coq
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 *)
*)

```

---

<div class="post-metadata">

**Author:** ![jp-diegidio](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/jp-diegidio/32/819_2.png) [@jp-diegidio](https://discourse.rocq-prover.org/u/jp-diegidio)\
**Post date:** [March 31, 2025, 5:24pm UTC](https://discourse.rocq-prover.org/t/basic-questions-on-polymorphic-universes/2586/2 "2025-03-31T17:24:18Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![jp-diegidio](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/jp-diegidio/32/819_2.png) [@jp-diegidio](https://discourse.rocq-prover.org/u/jp-diegidio)\
**Post date:** [April 1, 2025, 4:10pm UTC](https://discourse.rocq-prover.org/t/basic-questions-on-polymorphic-universes/2586/3 "2025-04-01T16:10:14Z")

</div>

Or, for example, take this:

```auto
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):

```auto
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?