The coq manual says " To ensure compatibility, every global universe is set to be strictly greater than Set
when it is introduced". Why is that? What compatibility is being considered? I know Set
needs to be different when using -impredicative-set
, but what about the common case where that option is not passed?
(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" ) -*- *)
Universe u.
Inductive unit : Type@{u} := tt.
Print Universes.
(* Set < Top.24 *)
(* < u *)
(* Prop < Set *)
I am asking because this makes non-polymorphic container types and non-container types have different universes (e.g. nat
is in Set
but list nat
is <Set
if `list is not universe polymorohic or template polymorphic).
I think the idea is that if you have a Type you probably don’t want it
lowered to Set. ie if you have universe-monomorphic list, when using
list nat : Set
the options are either that every list and types it’s
been applied to becoming Set and prevent anyone else from applying list
to non-Set, or an error. (I guess in practice probably someone has
already applied list to something that can’t be Set so you can’t avoid
the error)
Gaëtan Gilbert
That’s an historic choice, I think everything would be fine if only Set <= i
was required (I don’t think potential impredicativity is important here). However that would still leave your list type in i
unless you make it Set -> Set
explicitly. Note that the universe of list has to be greater or equal to its parameter universe, so any later instantiation of list A with A’s type larger than Set will make its conclusion type “grow” accordingly.