The meta-parameter layer check.

The type theory implemented in rzk separates a /meta-theoretic parameter layer/ from the object theory (RSTT proper): see §3.2 of the Rzk paper (Kudasov, Sim, Ahrens, "Rzk: a Proof Assistant for Synthetic ∞-Categories", arXiv:2607.12207), where a statement is abstracted over a context of schematic cube, tope, and type parameters. The checker did not enforce responsible use of this layer. Per declaration, the meta prefix is the parameter prefix up to and including the last parameter whose type lives outside RSTT proper: a universe, CUBE, TOPE, or a Π-type quantifying over or landing in one of those. Interleaved object parameters are swept in, which only strengthens the check.

The discipline: the meta prefix must be fully supplied wherever the declaration is used at an object-level position; unsaturated use at a meta-typed position is legitimate macro-level plumbing and stays allowed. Then the development reads as a family of object-theory definitions, one per meta instantiation.

Positions are classified structurally, on the elaborated term:

• the root of a declaration's type and value is meta (a definition may alias a schema), and a λ-body inherits its λ's position (the value's leading λs are the declaration's own parameters);
• an application argument is meta when the function's Π-domain at that position is meta-shaped (the receiver declared a schema parameter);
• the components of type formers are meta (types are the schema layer), except the endpoints of an identity type, which are terms;
• everything else (pair components, projections, recOR branches, a let-bound value, …) is an object position.

The strict rule (the default, see MetaPrefixSensitivity) additionally requires an unsaturated schema argument to sit within a top-level receiver's meta prefix. This also polices meta-shaped domains that only arise by instantiating a receiver's object parameters with large types (as in composing schema-level implications with a generic comp); such uses are emitted with the distinct code MetaPrefixStrictOnly, so the structural sensitivity can silence them without losing the rest.

Known blind spot: under type-in-type, an impredicative instantiation can forge a meta-shaped argument domain out of an object parameter — with g : (X : U) → X → X, in g ((X : U) → X → X) my-id the second domain is meta-shaped only because X was instantiated with a large type. The structural sensitivity reads such a position as meta and stays silent. The strict default flags it when the argument falls outside the receiver's meta prefix (as here), but a forgery landing within the prefix, or behind a λ-bound receiver, still passes: deciding whether an instantiation is genuinely impredicative is level inference, a separate (planned) analysis, not this check.