The Coq mailing list

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

> I.e. the argument type of a function type can live in a higher universe 
than the result type.

Yes, but "lst" is an _inhabitant_ of the function type, it's not the function 
type itself.

Similarly "(fun A:Type@{u+1} => A) : Type@{u+1} -> Type@{u}" is rejected

PS Coq does not expect you to write algebraic universes (using + or max) and may error 
with messages such as "Unable to handle arbitrary u+k <= v constraints." if 
you do

Gaëtan Gilbert

On 16/11/2022 21:02, Helmut Brandl wrote:
> I’d like to understand universes and universe polymorphism better. Therefore 
> I have some questions:
>
> The following term is well typed in coq:
>
>     Universe u.
>     Check forall A:Type@{u+1}, Type@{u}.
>
>
> I.e. the argument type of a function type can live in a higher universe than 
> the result type. If I try the same with an inductive type, I get an error.
>
>     Inductive lst (A: Type@{u+1}): Type@{u} :=
>     | nil: lst A
>     | cons: A -> lst A -> lst A.
>
>     *Error:*Universe inconsistency. Cannot enforce u = max(Set, u+1).
>
>
> What is the theoretical background of this consistency error. The type of 
> ‘lst’ is exactly the type I have checked above as well typed. I suspect that 
> if it were well typed, then I could ‘hide’ an object from the universe ‘u+1’ 
> in the list which resides in the universe ‘u’. Can anybody help to give a 
> more precise explanation.
>
> Regards
> Helmut