improve lift and lower

This is not actually necessary; the fact that you have `A : Type@{i}` and you are returning it as `A : Type@{j}` will already enforce `i <= j`,