Section Univ.

Universe u.
Universe v.

Variable X:Type@{u}.
Variable Y:Type@{v}.

Check (X -> Y).
(* : Type@{max(u, v)} *)

Check (list X).
(* : Type@{max(Set, u)} *)

Check (forall T : Type@{u}, T).
(* : Type@{u+1} *)