# Universe


Universe hierarchy: Type_0 : Type_1 : Type_2 : ... Lazy infinite non-cumulative tower.

## `Type_0`

_Type_0: first universe in the non-cumulative tower._

Predefined `Type_0` universe.

## `Type_1`

_Type_1: second universe in the non-cumulative tower._

Predefined `Type_1` universe.

## `Type_2`

_Type_2: third universe in the non-cumulative tower._

Predefined `Type_2` universe.

## `Type_3`

_Type_3: fourth universe in the non-cumulative tower._

Predefined `Type_3` universe.

## `Type_4`

_Type_4: fifth universe in the non-cumulative tower._

Predefined `Type_4` universe.

## `level`

_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.