We work in the core type theory. Let \(i_{1},i_{2}:\mathord {\textnormal {\textsf {Level}}}\), let \(A:\mathord {\textnormal {\textsf {Type}}}(i_{1})\), and suppose that \(i_{1}\le i_{2}\). Then \(A:\mathord {\textnormal {\textsf {Type}}}(i_{2})\).
We work in the core type theory. Let \(i_{1},i_{2}:\mathord {\textnormal {\textsf {Level}}}\), let \(A:\mathord {\textnormal {\textsf {Type}}}(i_{1})\), and suppose that \(i_{1}\le i_{2}\). Then \(A:\mathord {\textnormal {\textsf {Type}}}(i_{2})\).