Universe
Universe hierarchy: Type_0 : Type_1 : Type_2 : ... Lazy infinite tower.
level
Get the universe level of a type.
typeAt
Create universe type at level n (cumulative). Type_n contains all types
with universe ≤ n. Type_n itself has universe n + 1.
Type_n : Type_(n+1) for all n