ch:datatype-declarations: ch:datatype-declarations

The complete state trace is The last state follows because the inner arrow preserves its ambient sign in its codomain. A block-family application is admitted only at $(+,\mathsf{open})$, so the occurrence is rejected. The inner domain $\mathbb{N}$ is separately checked at $(+,\mathsf{blocked})$ and passes; the outer codomain $\mathbb{N}$ is checked at $(+,\mathsf{open})$ and also passes. The family occurrence is therefore the unique failing subterm.

The single parameter binder has type ${\mathcal{U}}_i:{\mathcal{U}}_{i+1}$, so $\mathsf{lev}({\mathrm{\Delta }}_p)=i+1$. The empty index telescopes contribute $0$; the constructor telescopes and family declarations contribute $i$; and the motives contribute $k$. Therefore $$L=max(i+1,0,i,i,k)=max(i+1,k).$$ Omitting ${\mathrm{\Delta }}_p$ would instead produce $max(i,k)$. For $k\le i$, that incorrect maximum is $i$, although the binder $A:{\mathcal{U}}_i$ already forces the eliminator package into at least ${\mathcal{U}}_{i+1}$.

Take $$P_T:(A:{\mathcal{U}}_i)\to \mathsf{Tree}(A)\to {\mathcal{U}}_k,P_F:(A:{\mathcal{U}}_i)\to \mathsf{Forest}(A)\to {\mathcal{U}}_k.$$ The four methods are The requested computation is the annotated chain The second line applies Block-comp to the outer forest constructor. The third line contracts the tree child’s computation, and the fourth contracts the forest child’s computation. Both recursive children have supplied exactly one induction hypothesis.

For $(D\to \mathbb{N})\to \mathbb{N}$, the outer domain changes $(+,\mathsf{open})$ to $(-,\mathsf{blocked})$. The inner domain changes that state to $(+,\mathsf{blocked})$, where the occurrence of $D$ is rejected. Thus two sign reversals do not restore strict positivity: the ancestry flag remembers that the occurrence lies under a function domain. For $\mathbb{N}\to D$, the domain $\mathbb{N}$ is checked at $(-,\mathsf{blocked})$, while the codomain $D$ is checked at the original $(+,\mathsf{open})$; both pass. The first type would require a nested or functorial positivity argument not present in the regular Timpl-data card.