Tarski Universes and Decoding

Proof. Use the substitution theorem for the extended binding signature. The only new binder case is representative. Choose $y$ fresh for $s$: For stability of the decoding equality, the corresponding judgmental calculation is For $\mathrm{\Sigma }$, instantiate TU-Sig and TU-Sig-El in place of TU-Pi and TU-Pi-El; for W, use TU-W and TU-W-El (two lines each). Coproduct uses the two nonbinding induction hypotheses, while hierarchy and nullary codes are unchanged (one line each). Applying substitution to the displayed decoding derivation proves its judgmental stability in every case. ◻

Proof. Proof idea. The three clauses use three different induction hypotheses. For (1), every immediate Tarski premise erases to a derivable Russell premise, and erasure commutes with each substitution in the final rule. For (2), every immediate Russell premise has a decorated derivation whose erasure has the premise’s literal conclusion. For (3), every immediate round-trip conclusion is comparison-aligned with its Tarski premise. We verify the representative formation, binder, substitution, conversion, and mixed decoding cases.

For (1), consider TU-Pi. The premise induction hypotheses give $$E(\mathrm{\Gamma })⊢E(a):{\mathcal{U}}_i,E(\mathrm{\Gamma }),x:E(a)⊢E(b):{\mathcal{U}}_i.$$ Rule U-Pi derives $E(\mathrm{\Gamma })⊢\prod _{x:E(a)}E(b):{\mathcal{U}}_i$, which is the erasure of $⌜\mathrm{\Pi }⌝(a,x.b)$. Under a binder, the required raw equation is $$E(b[s/x])=E(b)[E(s)/x].$$ It follows by the same fresh-binder structural induction as lemma 75.3; in a decoded binder, that lemma supplies the literal equation for $\mathsf{El}$. The same calculation aligns the substituted contexts. For the conversion case TU-El-Eq, the premise induction hypothesis gives $$E(\mathrm{\Gamma })⊢E(a)\equiv E(a^{\prime }):{\mathcal{U}}_i,$$ and U-El-Eq gives $E(\mathrm{\Gamma })⊢E(a)\equiv E(a^{\prime })\mathsf{type}$, exactly the erased conclusion. A decoding rule such as TU-Pi-El erases to reflexivity of the Russell $\mathrm{\Pi }$-type. The $\mathrm{\Sigma }$-, W-, coproduct-, hierarchy-, and nullary cases instantiate these displays with their named formation and decoding rules (one to three lines each); structural and ordinary term rules are homomorphic. This proves (1).

For (2), induct on the chosen Russell derivation with the literal conclusion hypothesis for every premise. A final U-Pi decorates its premises and applies TU-Pi; erasing the result returns the same raw $\mathrm{\Pi }$-expression. A final U-El has premise $$\mathrm{\Gamma }⊢A:{\mathcal{U}}_i.$$ Decoration produces a code $Q(A)$ and concludes, by TU-El, $$Q(\mathrm{\Gamma })⊢\mathsf{El}(Q(A))\mathsf{type}.$$ Erasure returns the literal Russell conclusion $\mathrm{\Gamma }⊢A\mathsf{type}$. By contrast, a chosen derivation ending in ordinary $\mathrm{\Pi }$-formation remains ordinary $\mathrm{\Pi }$-formation. Thus two derivations of one Russell type may decorate by different routes, but each chosen route separately has the claimed erasure. Conversion uses TU-El-Eq; the remaining closure and structural rules instantiate this induction schema (one line each). This proves (2).

For (3), induct on $D_T$ with comparison alignment as the induction hypothesis for every premise. In a TU-Pi case, TU-Cong combines the aligned domain and body codes after the binder-context conversion supplied by TU-El-Eq. The substitution case uses the literal identity $(\mathsf{El}(b))[s/x]=\mathsf{El}((b[s/x]))$ from lemma 75.3, so both derivations enter the same converted binder context. In a TU-El-Eq case, congruence of $\mathsf{El}$ turns the aligned code endpoints into equal decoded types.

The mixed case is a strict decoding rule. For example, TU-Pi-El erases to reflexivity of $\prod _{x:E(a)}E(b)$. Syntax-directed decoration may rebuild that reflexivity by direct $\mathrm{\Pi }$-formation rather than by TU-Pi-El. The two left endpoints are nevertheless equal by TU-Pi-El; the two right endpoints are aligned by the premise induction hypotheses, and dependent- product congruence supplies the required context conversion. Hence the conclusions are comparison-aligned even though their final rules differ. The other strict decodings instantiate this calculation with their named rules (two lines each); all remaining cases are homomorphic. This proves (3). ◻