Container, recursion, termination, and coinduction boundaries

Containers and ornaments. Ordinary and indexed extensions, morphisms, cartesian layer transformations for ornaments, polynomial sums, products, composition, derivatives, and the forgetful map from vectors to lists are locally calculated in chapter 81. Initial-algebra, final-coalgebra, and representation statements retain the source’s extensional equality, W-type, M-type, decidable-position, and grammar hypotheses. No such existence or representation theorem is transferred to $T_0$.

$T_{\mathsf{rec}}$ is $T_0$ plus the displayed $\mathsf{Acc}$ formation, introduction, elimination, and computation rules. Accessibility induction, the proof-indexed recursor, measures, lexicographic closure, and Euclid’s equations are local. Erasing an accessibility certificate from computation needs the stated extensional certificate-independence result; decidability of the relation is not assumed. The Bove–Capretta domain predicate is a special-purpose alternative, not a new general recursion axiom.

The finite three-label graph language, truthful matrix composition, and descent reduction are local. The finite idempotent criterion is imported at the Lee–Jones–Ben-Amram finite first-order graph signature. Sound termination additionally requires truthful extraction and a well-founded value order. Acceptance is not complete for terminating programs.

The selected rank-zero interface has formation, constructor, iterator, and beta rules, but no destructor and no implicit functor action. The strong-normalization import applies only to the exact Abel–Matthes–Uustalu calculus. Nested renaming, substitution, and fusion are local. Dependent induction separately assumes a positive action and ordinary fixed-point induction. Ahn–Sheard histomorphism divergence and Mendler’s finite constraint property $P$ retain their distinct source signatures.

$T_{\mathsf{co}}$ contains the guarded stream and finite coinductive-record schema with judgmental observation equations. Finite observation productivity, bisimulation, coinduction, copattern compilation, and the Fibonacci recurrence are local at that signature. The bounded sized fragment has no infinity size or size weakening. Downen–Ariola structural coinduction is a separate contextual calculus; its soundness theorem is not a guardedness-completeness result.

The five Kappa corpora check finite container, Euclidean, size-change, nested-substitution, and stream-observer fixtures. They establish none of the representation, normalization, infinite-descent, parametricity, productivity, or coinduction metatheorems above.