Stream: Coq users

Topic: Successor universes


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

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

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

view this post on Zulip Gaëtan Gilbert (Jun 17 2021 at 07:08):

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

view this post on Zulip 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: Jan 28 2023 at 06:30 UTC