Identity, indexed-family, record, and description boundaries

The locally proved interface is identity formation, reflexivity, generic-endpoint J, transport, path operations, groupoid laws, singleton contraction, based J, and K/UIP equivalence. A generic K or function-extensionality term is stuck; this observation is not an independence proof. The finite Kappa checker verifies scope and the actual reflexive substitution in four concrete J premises.

Vec and Fin programs are first derived from direct eliminators. The imported no-K statement is Cockx–Devriese–Piessens Theorem 1 at valid case trees satisfying both Section 3.1 restrictions. The IR/IIR and context/type IIT cards contain only their displayed formation, introduction, decoding, elimination, and computation rules. No canonicity, reduction-to-induction, initiality, gluing, quotient, or path-constructor theorem transfers.

Pollack’s full left-associated calculus owns repeated labels, restriction, named projection, and their beta/passing equations. It has no judgmental eta. The Pollack-to-CPT preservation/reflection theorem is local and restricted to fresh labels, projection terms, beta/dot equality, and no standalone restriction result. Singleton/manifest fields, subtyping, modules, permutation, and surjective pairing are excluded.

The executable and the first generic-program laws use the finite regular normal form. The principal indexed language is the exact MAG ISPT/SPF universe. Equality is proved only for the smaller finite $\mathsf{EqDesc}$ fragment; full ${\mathrm{\Pi }}_f$ and arbitrary index witnesses are outside it. Elaboration soundness is local to the displayed surface grammar. The binding theorem is a separate extension and supplies no LF adequacy, PHOAS parametricity, or nominal freshness theorem.

Fold and syntactic unfold equations are proved from code interpretation. No categorical initial/final-algebra theorem or container representation is transferred.