Sort Polymorphism and Stratified Type Theory

Proof. This is the stipulated substitution closure of the parameter judgment. For Same-Sort, substitution sends both occurrences of $s$ to the same ground or variable sort, so the rule rebuilds directly. Every additional ground rule is required by convention 118.1 to be closed under the same substitution; otherwise it is not an admissible SortPoly elimination policy. ◻

Proof. Checking $\theta$ tests finitely many equalities in $G$ and finitely many memberships in $E$, each decidable because $G$ and $E$ are finite. The candidate maps form the finite set $G^n$, so the solutions are obtained by filtering it. For the last clause, reflexivity of $E$ discharges every atom $\mathsf{elim}(s,s)\mathsf{allowed}$ at any $\theta$, so only the equations constrain the map. ◻

Proof. Four inductions establish the result. First, sort substitution preserves sort formation, level formation, contexts, typing, and conversion. For a ground sort substitution the ground-sort rule is unchanged; a substituted sort variable becomes either a ground sort or a variable still declared in the target context. The level cases are structural. In the mutual judgment induction, context extension, universe formation, and universe conversion use these two facts. Global lookup composes its sort-and-level substitution with the one being applied. Case and iota also use stability of the allowed- elimination premise. Product, application, abstraction, fixpoint, beta, eta, and conversion rebuild their original rule from the induction hypotheses.

Second, $m_G(\mathrm{\Sigma })$ is exhaustive. If $({\mathrm{\Theta }}_C⊢C:A)\in \mathrm{\Sigma }$ and $\overrightarrow{s}$ is a well-formed ground assignment from $G$ for the sort binders of ${\mathrm{\Theta }}_C$, then $$(\mathcal{L}({\mathrm{\Theta }}_C)⊢C_{\overrightarrow{s}}:m_G(A[\overrightarrow{s}]))\in m_G(\mathrm{\Sigma }).$$ For a definition this is the copy inserted by the definition of $m_G$. For an inductive declaration it is either the copied type former or one of its copied constructors. Those are the only forms of global declaration.

Third, assume $m_G(\mathrm{\Sigma })$ is well formed and the local sort context has no sort variables. Mutual induction on context formation, typing, and conversion proves that $m_G$ preserves each judgment. Since $m_G$ traverses local syntax homomorphically, every rule except empty-context and global lookup is rebuilt from the same rule and its induction hypotheses. The empty-context case uses well-formedness of $m_G(\mathrm{\Sigma })$. In a lookup $C\{\overrightarrow{p}\}$, split $\overrightarrow{p}$ into ground sort arguments $\overrightarrow{s}$ and level arguments $\overrightarrow{u}$. Absence of local sort variables puts $\overrightarrow{s}$ in the finite enumeration used by $m_G$; exhaustivity gives $C_{\overrightarrow{s}}$, and global lookup at $\overrightarrow{u}$ has type $$m_G(A[\overrightarrow{s}])[\overrightarrow{u}]=m_G(A[\overrightarrow{s},\overrightarrow{u}]).$$

Finally, induct on well-formation of $\mathrm{\Sigma }$. The empty environment maps to itself. For a definition, apply sort substitution to each finite ground assignment, then the third induction to its body; extend the monomorphized environment once for each copy, weakening earlier derivations across later copies. For an inductive declaration, do the same simultaneously for its parameter telescope, index telescope, constructor telescopes, and constructor indices; the instantiated declared sort is in $G$, and level constraints are unchanged. Thus $m_G(\mathrm{\Sigma })$ is well formed. Applying the third induction to the assumed typing derivation yields the displayed judgment. The argument uses the elimination policy fixed in convention 118.1; it says nothing about an arbitrary table or about definition 118.5. ◻

Proof. Suppose such a term exists in a signature $\mathrm{\Sigma }$ containing the displayed empty declaration. Substitute $\mathsf{Type}$ for every remaining sort variable of $\mathrm{\Theta }$, so that the judgment has no sort variables; apply theorem 118.8. It remains to construct the pCUIC embedding rather than assume it. Mutual induction on the ground SortPoly context, typing, and conversion derivations keeps variables and the $\mathrm{\Pi }$, application, abstraction, fixpoint, beta, eta, and conversion rules unchanged. A universe is either $\mathsf{Prop}$ or $\mathsf{Type}$, so the corresponding pCUIC universe rule applies. In a global lookup, the monomorphized signature contains the same ground declaration. In case and iota, an inductive in $\mathsf{Prop}$ eliminates only into $\mathsf{Prop}$ or, under the stated premise, by singleton elimination; these are precisely the pCUIC cases. Induction on the global environment applies this translation to each definition and to every inductive and constructor declaration, showing that the monomorphized global environment is a pCUIC environment. Hence the translated judgment is a closed pCUIC inhabitant of its empty type, contradicting pCUIC consistency. The $\mathsf{Prop}$-elimination hypothesis is used exactly in the case and iota cases and is not implied by definition 118.3 alone. ◻

Proof. This is the consequence of Hurkens’s construction [Hur95]. Its large and small product interfaces are both interpreted by the single product rule; the universe code and its decoding are interpreted by $\ast$ and the identity; and the source’s arbitrary small code is interpreted by $F$. The construction then returns an element of its decoding, namely $f:F$. The import uses only products, application, abstraction, and their beta equations; it uses no inductive elimination. Hence changing allowed-elimination constraints cannot invalidate the construction while $\ast :\ast$ and $(\ast ,\ast ,\ast )$ remain. ◻

Proof. For clause 1, let $\delta$ send a dominated variable $s$ to its dominant ground sort $g_s$, and every undominated variable to $g_i$. A ground edge is fixed. If an edge ends at an undominated variable, validity clause 2 puts its incident ground endpoint above $g_i$; if it ends at a dominated variable, clause 3 puts its ground endpoint below $g_s$. Edges between variables reduce to these two cases through transitive closure. Validity clause 1 prevents a path through variables from creating a new ground edge. Thus every edge of $\mathrm{\Theta }$ maps to an edge of ${\mathrm{\Theta }}_G^{+}$, so $\delta$ is a valid sort substitution. Structural induction on typing, with the case and fixpoint rules using the mapped elimination edge, proves substitution preservation.

For clause 2, induct first on raw syntax to show that the generated context contains one fresh sort variable for every anonymous universe and exactly the edges printed by the generating clause. Variables, applications, products, and ordinary constructors take unions of their recursive constraints. Record formation threads the constraints field by field. A case adds the edge from the scrutinee sort to the motive sort, and a fixpoint adds the edge from its recursive source to its codomain; no other clause adds an edge. Now induct on a typing derivation of an alternative assignment. The induction hypotheses validate all recursively generated edges. The record case composes the field substitutions, while case and fixpoint validate their single new edge from the corresponding typing premise. Therefore the alternative assignment is a substitution into the inferred context. Since the initial variables were never freshened, it fixes ${\mathrm{\Theta }}_0$, proving the displayed implication.

For clause 3, prove mutually that $m_G$ preserves global environments, contexts, typing, and conversion. Empty contexts and local structural rules are homomorphic. A global declaration has only finitely many sort variables and $G$ is finite, so the monomorphized environment contains every ground instance required by lookup. Products, conversion, inductives, constructors, case, and fixpoint rebuild the same rule at the selected copies. The premise $\mathrm{\Theta }=U(\mathrm{\Theta })$ is used in case and fixpoint: their elimination edges are already ground and hence remain in the target. This proves the displayed judgment.

For clause 4, apply clause 1 to replace every sort variable by a ground sort, then clause 3 to monomorphize. The bound on $s$ selects a consistent ground copy of the empty declaration. A closed inhabitant would therefore give a closed SortPoly inhabitant of that copy, contradicting the assumed consistency.

For clause 5, induct simultaneously on SortPoly environment formation, context formation, typing, and conversion. Copy every premise unchanged and use the corresponding bounded rule with no nonground edge. The universe, product, conversion, inductive, and elimination cases keep their existing ground policy; variable and structural cases add no edge. All three clauses of definition 118.12 are therefore satisfied. This gives the inclusion $\iota$. An inconsistency of SortPoly transfers along $\iota$; clause 4 transfers a bounded inconsistency at a consistent ground bound back to SortPoly. Hence the theories are equiconsistent at those sorts. Validity and the consistent-sort premise are used at the indicated steps; the proof does not cover arbitrary graphs or first-class level terms. ◻