(* Used in output/UnivBinders.v *)

Monomorphic Definition mono@{u} := Type@{u}.

Polymorphic Definition poly@{u} := Type@{u}.

Monomorphic Universe reqU.