## Stream: Coq users

### Topic: ✔ Ghost universe level with cumulative record

#### Kenji Maillard (Dec 15 2021 at 15:21):

Hello, I'm trying to control the quantifications over polymorphic universes in a few definitions and I have troubles understanding what happens with the following code using cumulative records:

``````Set Universe Polymorphism.
Set Printing Universes.

Cumulative Record F@{v} (X : Type@{v}) : Type@{v} := { R : Set }.

Section Bar.
Universe u.
Context (A : Type@{u}) (FA : F A).
Section foo.
Context (aa : R A FA).
Definition foo := tt.
Print foo.
(* No universe bound *)
(* foo@{} = tt *)
(*      : unit *)
End foo.
Print foo.
(* A universe appears in the context *)
(* foo@{} = tt *)
(*      : unit *)
(* (*  |= Set < bug.31 *)
(*        u <= bug.31 *) *)
End Bar.
Print foo.
(* both the declared and undeclared universe end up bound *)
(* foo@{u bug.31} = tt *)
(*      : unit *)
(* (* u bug.31 |= Set < bug.31 *)
(*                u <= bug.31 *) *)

Section Bar2.
Universe u.
(* Now trying to be explicit about the universes fed to F *)
Context (A : Type@{u}) (FA : (F@{u} A : Type@{u})).
Section foo.
Context  (aa : R A FA).
Definition foo2 := tt.
Print foo2.
(* No universe bound *)
(* foo2@{} = tt *)
(*      : unit *)
End foo.
Print foo2.
(* A universe appears again, and gets bound immediately *)
(* foo2@{bug.53} = tt *)
(*      : unit *)
(* (* bug.53 |= Set < bug.53 *)
(*              u <= bug.53 *) *)
End Bar2.
Print foo2.
(* In the end two universes are bound *)
(* foo2@{u bug.53} =  *)
(* tt *)
(*      : unit *)
(* (* u bug.53 |= Set < u *)
(*                Set < bug.53 *)
(*                u <= bug.53 *) *)
``````

I would have expected some way to obtain a definition of `foo` that depends at most on the universe level `u` and I don't see how to proceed (using coq 8.13).

#### Kenji Maillard (Dec 15 2021 at 15:23):

Just realised that the ghost universe level is coming from the projection `R`...

#### Notification Bot (Dec 15 2021 at 15:23):

Kenji Maillard has marked this topic as resolved.

Last updated: Jun 25 2024 at 15:02 UTC