Universe — nix-effects

level: read a type's universe level as an Int; level 0 covers atomic types, level 1 contains Type_0, and so on up the stratified tower. Throws (via .universe) when the type's level is term-dependent or level-polymorphic.

level : Type -> Int

Get the universe level of a type. Equivalent to .universe field access; provided for explicit calls. Like .universe, it throws rather than fabricating a level when the type's universe is term-dependent or level-polymorphic (no ground suc^n zero).

`lift`

lift: raise a type by one universe — lift t = liftTo (t.universe + 1) t, preserving its values.

lift : Type -> Type

Raise a type by one universe level. lift t = liftTo (t.universe + 1) t. See liftTo.

`liftTo`

liftTo: explicit cross-level coercion — liftTo m t reindexes type t to universe m (require m >= t.universe), preserving its values; idempotent at m == t.universe, throws when m is below t's level.

liftTo : Int -> Type -> Type

Reindex a type to a higher universe. liftTo m t has universe m and accepts exactly the values t accepts (check is preserved); its _kernel is the kernel LiftAt of t's kernel type. Requires m >= t.universe; idempotent at m == t.universe. The non-cumulative tower has no implicit subsumption, so this is how a lower-level type becomes a member of a higher universe.

`typeAt`

typeAt: factory producing the non-cumulative universe type Type_n; values of Type_n are types of universe exactly n; Type_n itself has universe n+1.

typeAt : Int -> Type

Create universe type at level n (non-cumulative). Type_n contains exactly the types with universe n — a lower-level type is not subsumed, use lift/liftTo for the explicit coercion. Type_n itself has universe n + 1, enforcing Type_n : Type_(n+1) for all n and avoiding Russell's paradox.