## Stream: Coq users

### Topic: Successor universes

#### N. Raghavendra (Gitter import) (Jun 16 2021 at 22:58):

While trying to learn how to use explicit universes, I did something like this:

``````Set Universe Polymorphism.
Definition constant_function@{l m}
: forall (X : Type@{l}) (Y : Type@{m}), Y -> X -> Y
:= fun (X : Type@{l}) (Y : Type@{m}) (y : Y) (x : X) => y.
Inductive Empty@{l} : Type@{l} := .
Definition empty_function@{l m} : forall (X : Type@{m}), Empty@{l} -> X
:= fun (X : Type@{m}) => Empty_rect (constant_function@{l (m + 1)} Empty@{l} Type@{m} X).
``````

This produces a syntax error on `constant_function@{l (m + 1)}`. How does one specify the successor of a universe level, or get around doing so? Thanks.

#### Kenji Maillard (Jun 17 2021 at 06:06):

I think you need to add another level `m'` together with a constraint `m < m'`. There are restrictions on where arithmetic universe levels (containing successor or max) can be used (see this issue for instance)

#### N. Raghavendra (Gitter import) (Jun 17 2021 at 06:59):

@Kenji Maillard Thanks, yes this works:

``````Section _empty_function.
Universes l m m'.
Constraint m < m'.
Definition empty_function : forall (X : Type@{m}), Empty@{l} -> X
:= fun (X : Type@{m}) => Empty_rect (constant_function@{l m'} Empty@{l} Type@{m} X).
End _empty_function.
``````

It would be nice if the section could be abbreviated to

``````Definition empty_function@{l m m' |= m < m'} : forall (X : Type@{m}), Empty@{l} -> X
:= fun (X : Type@{m}) => Empty_rect (constant_function@{l m'} Empty@{l} Type@{m} X).
``````

#### Gaëtan Gilbert (Jun 17 2021 at 07:08):

you can say `Definition empty_function@{l m m' | m < m'}`

#### N. Raghavendra (Gitter import) (Jun 17 2021 at 07:18):

@Gaëtan Gilbert Thanks, I should have read the GH issue that @Kenji Maillard cited carefully because it has an example of the notation you mentioned. As you say, this works

``````Definition empty_function@{l m m' | m < m'} : forall (X : Type@{m}), Empty@{l} -> X
:= fun (X : Type@{m})  => Empty_rect (constant_function@{l m'} Empty@{l} Type@{m} X).
``````

Last updated: Sep 23 2023 at 14:01 UTC