Dependent-core and Dybjer-source boundaries

Chapters 71–73 fix derivable contexts, type and term typing, type and term equality, the selected structural rules, dependent products and sums, unit, empty and Boolean types, coproducts, natural numbers, W-types, and one unindexed strictly positive constructor schema. The displayed beta, eta, and computation rules are exactly those recorded in subappendix A.4, subappendix A.5.

Presupposition and regularity, weakening, one-variable and telescope substitution, identity and composition of relative telescope maps, the selected $\mathrm{\Pi }$/$\mathrm{\Sigma }$ equivalences, set soundness of the base formers and unindexed polynomial schema, and the stated W-recursion encodings. The encoded natural numbers, lists, and trees are claimed to have the displayed recursors, not judgmental dependent eliminators.

The starred development uses the separate extensional calculus ${\mathcal{T}}_{\mathrm{D}}$ of convention 73.46. Its first Russell universe is closed under the displayed formers and admits the large eliminations used to define arity families. Identity types with equality reflection and uniqueness, function extensionality, empty/unit function uniqueness, coproduct splitting, and extensional W-induction support the container normal form and its initial W-algebra.

The Dybjer initial-algebra theorem is not stated for the intensional core $T_0$. It neither supplies indexed inductive families nor proves homotopy-initiality of higher inductive types.

The three Kappa supplements check finite capture-avoiding substitution, selected $\mathrm{\Pi }$/$\mathrm{\Sigma }$ calculations, and a finite strict-positivity traversal. They do not implement the declarative kernel, the set interpretation, the external rule-set construction, or the initial-algebra theorem.