Shared signatures

The five shared dependent signatures are named here so that later statements cannot retreat to “the usual fragment.”

$T_0$.

The intensional dependent base of chapter 26–chapter 30: dependent products and sums, the selected ordinary inductive formers, universes at the displayed levels, and intensional identity.

$T_{\mathsf{fam}}$.

$T_0$ plus exactly the indexed-family schema admitted in chapter 31.

$T_{\mathsf{rec}}$.

$T_0$ plus the well-founded recursion principles admitted in chapter 32.

$T_{\mathsf{co}}$.

$T_0$ plus the coinductive record/corecursion fragment admitted in chapter 33.

$T_{\mathsf{impl}}$ and $T_{\mathsf{impl}\text{-}\mathsf{co}}$.

The fixed implementation signatures owned respectively by chapter 48–chapter 126; the second adds only the selected stream fragment and never inherits normalization merely from the first.