Kenji Maillard (Dec 15 2021 at 15:21): 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: Oct 03 2023 at 02:34 UTC