The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

> Is there any way of convincing Coq that pack2's codomain is pack@{i+1}?

No, algebraic universes (+1 and max) are allowed only on Type itself, 
not on definitions/inductives.

Gaëtan Gilbert

On 17/01/2019 15:18, Arthur Azevedo de Amorim wrote:
> Coq accepts the following snippet, which declares a universe-polymorphic 
> type that lives in a successor universe:
>
> Polymorphic Inductive pack@{i} : Type@{i+1} :=
>    Pack { sort : Type@{i}; elt : sort }.
>
> However, if I try to take the successor of a universe level elsewhere, I 
> get a parse error:
>
> Polymorphic Definition pack2@{i} (T : Type@{i}) (x : T) : pack@{i+1} :=
>    Pack pack@{i} (Pack@{i} T x).
>
> (* Toplevel input, characters 65-66: *)
> (* > Polymorphic Definition pack2@{i} (T : Type@{i}) (x : T) : 
> pack@{i+1} :=   Pack pack@{i} (Pack@{i} T x). *)
> (* >                                                                  ^ *)
> (* Error: Syntax error: [constr:universe_level] or '}' expected (in 
> [instance]). *)
>
> If I omit the annotation, Coq complains that I haven't declared the 
> universe where the definition should live:
>
> Polymorphic Definition pack2@{i} (T : Type@{i}) (x : T) :=
>    Pack pack@{i} (Pack@{i} T x).
> (* Toplevel input, characters 61-65: *)
> (* > Polymorphic Definition pack2@{i} (T : Type@{i}) (x : T) :=   Pack 
> pack@{i} (Pack@{i} T x). *)
> (* >                                                              ^^^^ *)
> (* Error: Universe {Top.72} is unbound. *)
>
> Is there any way of convincing Coq that pack2's codomain is pack@{i+1}?
>
> Thanks!
>
> Best,
> Arthur