Stream: Coq users

Topic: ✔ Ghost universe level with cumulative record


view this post on Zulip 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).

view this post on Zulip Kenji Maillard (Dec 15 2021 at 15:23):

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

view this post on Zulip Notification Bot (Dec 15 2021 at 15:23):

Kenji Maillard has marked this topic as resolved.


Last updated: Mar 29 2024 at 01:40 UTC