# _internal


fx.tc.check._internal: cross-part checker helpers reachable from sibling parts via the self-fixpoint; not part of the stable consumer surface.

## `checkDescAtAnyLevel`

_checkDescAtAnyLevel: description checking at any universe level — accepts both primitive `VDesc` results and encoded `VMu` descriptions (the `VDesc ↔ μ_⊤(descDesc I L)` correspondence) and threads the universe level back to the caller for downstream encoding decisions._

```
checkDescAtAnyLevel : Ctx -> Tm -> Val -> Computation { term; level }
```

Trusted-annotation fast path: when `dTm` is a `T.mkAnnTrusted`
with a complete `_descRef`, build a canonical description term
directly (skipping the unfolding scan) and reuse the carried
level. Otherwise fall through to inference and dispatch on the
inferred type's tag:

- `VDesc`: the level is already on the type; conv-check that the
  index type matches `iTyVal` and forward.
- `VMu`: the description is encoded — scan a bounded list of
  candidate universe levels (the prelude exercises `L = 0..3`)
  and ask `conv` whether `V.vDesc lev iTyVal` unifies with the
  inferred type. Conv fires the symmetric `VDesc ↔ VMu`
  unfolding internally (same mechanism as
  `conv.nix:344-355`).
- Anything else: emit a `typeError` — not a description.

Used by `desc-con` checking (`check.nix`) for `_descConCert`
validation, by `infer.nix` for `desc-ind` motive and branch
checking, and by `type.nix:mu` to thread the description level
into the `μ` type's universe level.

## `checkMotive`

_checkMotive: eliminator-motive validation — walks the lambda layers of a motive against an expected domain chain `D_1 → … → D_n → U(k)` and returns the elaborated motive term together with the universe level `k` of its codomain._

```
checkMotive : Ctx -> Tm -> Chain -> Comp { term; level }
```

The domain chain is a `{ head : Val; tail : Val → Chain } | null`
sequence so each layer's domain may depend on the previously-bound
value (required by `desc-ind`, whose motive is
`(i : I) → μ D i → U(k)`). 1-argument call sites use the
`singleton` helper to build a one-element chain.

- Lambda motive: extend the context with the current layer's
  domain, recurse into the body with `chain.tail freshV`, and
  wrap the result in `T.mkLam`. The level threads up unchanged
  through each lam wrapper so the innermost codomain's universe
  flows back to eliminators that care about it (e.g., `desc-ind`'s
  `allTy`).
- Non-lambda motive: fall through to `infer`, then walk the
  inferred Π-chain in lock-step with the expected `chain`,
  conv-checking each domain and instantiating each codomain
  through a fresh variable. The innermost codomain must be a
  universe; its level is the motive's level.

Failure modes emit `D.mkKernelError` under the `P.Motive` position
for the diagnostic renderer. Cross-ref: `singleton` for the
unary-chain helper, `infer` for the synthesis fallback,
`checkTypeLevel` for the innermost-universe leaf.

## `singleton`

_singleton: build a one-element motive chain — `{ head = dom; tail = _: null; }` — the trivial telescope used by `checkMotive` call sites with a single domain and no nested binder dependency._

```
singleton : Val -> Chain
```

The motive chain consumed by `checkMotive` is a nested
`{ head : Val; tail : Val → Chain } | null` structure so each
layer's domain may depend on prior binder values. Most
eliminator sites (Sum, Eq, Squash) have only one motive
argument and no inter-binder dependency; `singleton dom` packs
that into the chain shape with a constant `tail` that ignores
its argument and returns `null` — closing the chain after a
single layer.