1 2 3 4 5 6
Set Universe Polymorphism. Definition foo@{i j} (A : Type@{i}) : Type@{j}. Proof. abstract (exact ltac:(abstract (exact A))). Defined.