ch:tarski-universes: ch:tarski-universes

The nullary rules first give $$⌜\mathbb{N}⌝:{\mathcal{U}}_0,⌜\mathbf{1}⌝:{\mathcal{U}}_0.$$ Rule TU-Sum therefore gives $$c:=⌜+⌝(⌜\mathbb{N}⌝,⌜\mathbf{1}⌝):{\mathcal{U}}_0.$$ Weakening $c$ to the context $x:\mathsf{El}(⌜\mathbb{N}⌝)$, followed by TU-Pi, constructs $$d:=⌜\mathrm{\Pi }⌝(⌜\mathbb{N}⌝,x.c):{\mathcal{U}}_0.$$ Decode from the outside inward. Rule TU-Pi-El gives $$\mathsf{El}(d)\equiv \prod _{x:\mathsf{El}(⌜\mathbb{N}⌝)}\mathsf{El}(c)\mathsf{type}.$$ Next TU-Sum-El and the two base decoding equations give $$\mathsf{El}(c)\equiv \mathsf{El}(⌜\mathbb{N}⌝)+\mathsf{El}(⌜\mathbf{1}⌝)\equiv \mathbb{N}+\mathbf{1}.$$ Also $\mathsf{El}(⌜\mathbb{N}⌝)\equiv \mathbb{N}$ by TU-Nat-El. Dependent-product congruence, with context conversion for the codomain after changing the domain, now produces $$\cdot ⊢\mathsf{El}(d)\equiv \mathbb{N}\to (\mathbb{N}+\mathbf{1})\mathsf{type}.$$ The codomain is constant in $x$, so the context conversion has no effect on its raw expression.

More generally, suppose in $x:\mathsf{El}(⌜\mathbb{N}⌝)$ that $x:\mathsf{El}(⌜\mathbb{N}⌝)⊢c\equiv c^{\prime }:{\mathcal{U}}_0$. The TU-Cong scheme gives $$\cdot ⊢⌜\mathrm{\Pi }⌝(⌜\mathbb{N}⌝,x.c)\equiv ⌜\mathrm{\Pi }⌝(⌜\mathbb{N}⌝,x.c^{\prime }):{\mathcal{U}}_0.$$ Thus judgmentally equal codomain codes produce judgmentally equal product codes, as required.

For a representative TU-Sig instance, $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢a:{\mathcal{U}}_i\\ \mathrm{\Gamma },x:\mathsf{El}(a)⊢b:{\mathcal{U}}_i\end{array}}{\mathrm{\Gamma }⊢⌜\mathrm{\Sigma }⌝(a,x.b):{\mathcal{U}}_i},$$ erasure gives $$\frac{\begin{array}{c}|\mathrm{\Gamma }|⊢|a|:{\mathcal{U}}_i\\ |\mathrm{\Gamma }|,x:|a|⊢|b|:{\mathcal{U}}_i\end{array}}{|\mathrm{\Gamma }|⊢\sum _{x:|a|}|b|:{\mathcal{U}}_i},$$ which is exactly U-Sig. A TU-W-El conclusion erases as $$|\mathsf{El}(⌜\mathsf{W}⌝(a,x.b))|={\mathsf{W}}_{x:|a|}|b|\equiv |{\mathsf{W}}_{x:\mathsf{El}(a)}\mathsf{El}(b)|={\mathsf{W}}_{x:|a|}|b|,$$ so it becomes type reflexivity. Likewise TU-Sum-El erases to $$|a|+|b|\equiv |a|+|b|\mathsf{type}.$$

Here is the binder calculation needed in the dependent cases. Choose the bound name $y$ fresh for the substituting term $c$ and distinct from $x$. Then The third line is the induction hypothesis on the two immediate subexpressions. For W, instantiate each of the five lines with $⌜\mathsf{W}⌝$ and ${\mathsf{W}}_{-:-}-$ in place of $⌜\mathrm{\Sigma }⌝$ and $\sum _{-:-}-$ (five lines). This directly verifies $|e[c/x]|=|e|[|c|/x]$ for the two displayed dependent constructors.

Write $$L:=\mathsf{El}(⌜\mathrm{\Pi }⌝(a,x.b)),R:=\prod _{x:\mathsf{El}(a)}\mathsf{El}(b),$$ and let the chosen definitional isomorphism consist of $$F:L\to R,G:R\to L,G(F(u))\equiv u,F(G(v))\equiv v.$$ For $p:L$ and $s:\mathsf{El}(a)$, define weak application by $${\mathsf{app}}_{\varphi }(p,s):=F(p)(s):\mathsf{El}(b[s/x]).$$ For a term $t:\mathsf{El}(b)$ in context $x:\mathsf{El}(a)$, define weak abstraction by $${\mathsf{lam}}_{\varphi }(x.t):=G(\lambda x.t):L.$$ The beta calculation uses exactly one round-trip law and ordinary product beta: The first judgmental step is $F\circ G\equiv {\mathrm{id}}_R$; the second is $\mathrm{\Pi }$-beta. For $p:L$, the other calculation is explicit: $${\mathsf{lam}}_{\varphi }(x.{\mathsf{app}}_{\varphi }(p,x))=G(\lambda x.F(p)x)\stackrel{\mathrm{\Pi }-\eta }{\equiv }G(F(p))\stackrel{\text{inverse law}}{\equiv }p.$$

This local argument proves only the beta behavior of this one chosen isomorphism. It says nothing about compatibility of separately chosen isomorphisms with substitution, congruence, nested $\mathrm{\Pi }$-, $\mathrm{\Sigma }$-, or W-codes, composition of decodings, or two different paths through a chain of weak decoding laws. Those are commuting-diagram conditions on a whole family of choices. They require a separate coherence theorem and do not follow from the two round-trip equations for one $\varphi$.

Erasure sends the open code variable $a:{\mathcal{U}}_0$ to the same Russell term. If decoration follows the resulting U-El derivation, it returns the Tarski type $\mathsf{El}(a)$, and code mode returns $a$ by the variable rule. Thus the fixed syntax-directed round trip is reflexive. If a second Russell derivation forms the same erased type directly, its decoration need not end in TU-El. Equating that output with $\mathsf{El}(a)$ is exactly the missing mixed coherence equation. It must be stable under every substitution into the context. At the semantic signature cited in the chapter, this stability is supplied by natural inverse operations $\mathsf{Code}$ and $\mathsf{El}$, together with the Russell identification $\mathsf{El}(t)=t$. None of those equations is supplied by structural recursion on the raw terms of definition 75.1.

Each $C_i=V_{{\kappa }_i}\times \{0,1\}$ is a set. If , then , so $(C_j,0)\in C_i$; decoding this pair returns $C_j$, which proves TU-Hier and TU-Hier-El.

For the dependent-product case, write $a=(A,ϵ)$ and suppose the body assigns $b_x=(B_x,{ϵ}_x)\in C_i$ to every $x\in A$. Strong inaccessibility gives $$P:=\prod _{x\in A}{B}_x\in V_{{\kappa }_i}.$$ Interpret the product constructor by $(P,0)\in C_i$. Its decoding is ${\mathsf{El}}_i(P,0)=P$, exactly the dependent product of the decoded domain and fibres. This proves TU-Pi and TU-Pi-El; the other constructors use the corresponding closure operation.

Let $1$ be the singleton interpretation of $\mathbf{1}$. The codes $(1,0)$ and $(1,1)$ are distinct elements of $C_i$, but $${\mathsf{El}}_i(1,0)=1={\mathsf{El}}_i(1,1).$$ Thus decoding is not injective in this model. The comparison theorem uses only formation, congruence, substitution, and the named decoding equalities; it never reflects equality of decoded types back to equality of codes. Consequently the collision does not refute theorem 75.6.