T_0 and its normalized subfragment

$T_0$ is exactly the full intensional base owned by chapter 26–chapter 30. $T_{\mathrm{\Pi }\mathbf{2}}$ is its structural/$\mathrm{\Pi }$/$\mathbf{2}$ subfragment of convention 49.8.

The set interpretation gives consistency and Boolean separation for $T_0$ at the displayed universe assumptions. Identity types are interpreted by singleton-or-empty equality fibers.

Exactly two results, both by the Tait computability argument of section 49.2: Boolean separation (proposition 49.3) and canonicity for closed Booleans (theorem 49.2). Nothing else.

The normalization package $(\ast )$, including normality, soundness, completeness, and idempotence, is theorem 111.76; normal-form stability is lemma 111.77. Canonicity for $\mathbf{2}$, $\mathbb{N}$, identity, and vectors is theorem 49.18; decidable conversion is corollary 49.20. The six total conversion and head-inversion operations, their universal coherence, and $\mathrm{\Pi }$-head injectivity are theorem 111.81. Consequently corollary 111.82 discharges demands D1, D2, and D4 for the full displayed $T_{\mathsf{impl}}$ signature. The proof-relevant Kripke relation uses an explicit world action on syntax, values, closures, quotation, reification, neutral readback, semantic evidence, and stored judgments. Reflection requires an all-depth self-related neutral. Cross-level functionality is founded on a paired-level multiset followed by a Hessenberg sum of construction and membership ranks, and evidence is erased only after same-endpoint, bridge, cross-level vector, and peeling maps have proved the exact indexed equivalences.

Theorem 49.17 proves decidability of equality in the initial model at $T_{\mathrm{Coq}}$, the cumulative universe-bearing signature of convention 111.90, which is not $T_{\mathrm{\Pi }\mathbf{2}}$, $T_{\mathrm{el}}$ or $T_{\mathsf{impl}}$. The proof keeps the universe fibre $U_n^{\prime }$, because that fibre is the carrier of every type datum of the normalization model and the stratification its recursion descends on; it cannot be deleted or replaced by a normal-type judgment without re-founding the construction (remark 111.91). It proves no normalization, decidable-conversion, or injectivity statement for any book calculus.

The local construction proves its package simultaneously for $T_{\mathsf{impl}}$; remark 49.39 records the construction and the still separate extensions. It does not cover the $W$, sum, or void formers of all of $T_0$, coinduction, extensional type theory, or the subformula argument needed for conservativity over $T_{\mathsf{el}}$. Hence no normalization or decidable-conversion theorem for all of $T_0$ is claimed.