ch:sort-polymorphism: ch:sort-polymorphism

For a motive in the same abstract sort $s$, Same-Sort applies: its premises are $\mathrm{\Theta }⊢s\mathsf{sort}$ and the declaration of $I$ at codomain sort $s$. A motive in $\mathsf{Prop}$ is rejected unless the environment also declares $I$ at $\mathsf{Prop}$; that declaration premise is unavailable for an abstract $s$. The $\mathsf{Type}$ case fails for the same reason, with the missing premise that $I$ is declared at codomain sort $\mathsf{Type}$. No equality or elimination constraint on the abstract $s$ is present to derive either premise.

For $I:\mathsf{SProp}$, a case expression with motive $P:I\to \mathsf{Type}$ requires $\mathrm{\Sigma }\mid \mathrm{\Theta }⊢\mathsf{elim}(I,\mathsf{Type})\mathsf{allowed}$. Rule Same-Sort can conclude only $\mathsf{elim}(I,\mathsf{SProp})\mathsf{allowed}$, because the global declaration records codomain sort $\mathsf{SProp}$. Its second premise would have to say that the same $I$ was declared at $\mathsf{Type}$, which is false. Therefore the case rule has no derivation for its elimination premise.

Suppose $\mathsf{U}$ is formed at stratum $k$. Its bound variable $X:\mathsf{Type}$ must lie at a strictly lower stratum . Then $\mathcal{P}X=X\to \mathsf{Type}$ and $\mathcal{P}(\mathcal{P}X)$ are formed using dependencies below $k$. The paradoxical substitution $X:=\mathsf{U}$ uses DT-AppTy, whose argument premise requires $\mathsf{U}{:}^j\ast$. The available derivation is $\mathsf{U}{:}^k\ast$, and cumulativity can supply the former only if $k\le j$. Together with DT-Pi’s , this gives the impossible chain . In full StraTT, the mechanized type-safety result remains available, but consistency, normalization, and decidable checking remain open; the subStraTT logical-relation consistency theorem does not apply.

The stratum assignment $j=0$, $k=1$ gives Erasing the two stratum annotations recovers the requested unannotated product shape $\mathrm{\Pi }x:A.B$. If both premises are assigned stratum $0$, DT-Pi would require , which is false; no alternative rule in the displayed subStraTT fragment forms that dependent product.

In ${\mathcal{U}}_l^s$, $s$ is a sort and indexes the elimination judgment, whereas $l$ is a universe level and indexes universe formation and level conversion. A run-time-use annotation is a grade and indexes a graded typing/context judgment. The linear-versus-affine selection is a mode and indexes the structural rules available to a context. The book supplies no general translation between any two of these four roles. For each of the six pairs, such a translation would require a syntax map, preservation of the two indexed judgments and substitution, and reflection or a countermodel showing which distinctions the map loses. Sharing a numerical notation or a finite carrier is not such a proof.

The assignment @{Type SProp; 0} instantiates the source sort of the natural-number family by $\mathsf{Type}$ and the motive sort by $\mathsf{SProp}$. Its case rule therefore generates the premise $${\mathsf{edge}}_{{\mathrm{\Theta }}_G}(\mathsf{Type},\mathsf{SProp}),$$ which belongs to the bounded calculus’s ground elimination policy. Hence the large eliminator is accepted.

The assignment @{SProp Type; 0} generates instead the premise $${\mathsf{edge}}_{{\mathrm{\Theta }}_G}(\mathsf{SProp},\mathsf{Type}).$$ That edge is absent: unrestricted elimination from a proof-irrelevant source sort into computational data would permit the result to distinguish source inhabitants. Because both endpoints are ground sorts, a sort-variable assignment cannot manufacture the missing path. Condition 1 of definition 118.12 requires every ground path to be generated already by ground edges. The rejection is therefore not failure to form the motive or either branch body.