The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 13/09/2017 10:26, Dominik Kirst wrote:

> When tagging the function type explicitly with two (unconstrained)
> universe variables, the exact level of the codomain is kept variable and
> the supremum becomes definable. Is this behaviour an intended minimisation?

I would not even qualify that behavior as minimization; it looks like
plain inference.

For example, (fun x : Type => x) is inferred as (Type@{i} -> Type@{i}),
not as (Type@{i} -> Type@{j} | i <= j), and this is intended.

So, if you want extra universes and constraints, just add them by hand:

Fixpoint emb'@{i j} (s : Tree@{i}) : Tree@{j} :=
  let (A, f) := s in
  sup A (fun a => emb' (f a)).

Best regards,

Guillaume