ch:normalization: ch:normalization

Assume $\cdot ⊢v:\mathbf{0}$. Empty elimination gives the closed term $$p:={\mathsf{abort}}_{{\mathsf{Id}}_{\mathbf{2}}(\mathsf{tt},\mathsf{ff})}(v):{\mathsf{Id}}_{\mathbf{2}}(\mathsf{tt},\mathsf{ff}).$$ Canonicity at identity types applied to $p$ says, in particular, $$\cdot ⊢\mathsf{tt}\equiv \mathsf{ff}:\mathbf{2},$$ contradicting proposition 49.3. Therefore no such $v$ exists.

Boolean canonicity alone cannot produce this contradiction. Eliminating $v$ into $\mathbf{2}$ gives a closed Boolean, and Boolean canonicity merely says that this term is equal to one of $\mathsf{tt}$ or $\mathsf{ff}$. Both outcomes are individually consistent; it does not force the two constructors to be equal. Identity canonicity is stronger in exactly the needed way: an inhabitant of an identity type forces its endpoints to be judgmentally equal.

We prove both statements simultaneously by structural induction on the raw expression $t$. Write $$E=(\gamma ,{\gamma }^{\bullet }),E_a=((\gamma ,a),({\gamma }^{\bullet },a^{\bullet })).$$ All equalities below are equalities of the meta-level values defined in definition 49.9.

Variables. For weakening, the side condition excludes $t=x$. If $t=y$ is a variable of $\mathrm{\Gamma }$, lookup in $E_a$ and in $E$ returns the same component $y^{\bullet }$. For substitution there are two cases: $$(x[a/x]{)}^{\bullet }(E)=a^{\bullet }(E)=x^{\bullet }((\gamma ,a[\gamma ]),({\gamma }^{\bullet },a^{\bullet }(E))),$$ and, for $y\ne x$, $$(y[a/x]{)}^{\bullet }(E)=y^{\bullet }(E)=y^{\bullet }((\gamma ,a[\gamma ]),({\gamma }^{\bullet },a^{\bullet }(E))).$$

Constants. The clauses for $\mathsf{tt}$, $\mathsf{ff}$, and $\mathbf{2}$ ignore the added component except through recursively interpreted subexpressions, so the required equations are immediate.

Application. Let $t=fu$. For weakening, the induction hypotheses for $f$ and $u$ give Here ordinary syntactic weakening gives $u[(\gamma ,a)]=u[\gamma ]$. For substitution, ordinary substitution composition and the two induction hypotheses give where $E_{a[\gamma ]}=((\gamma ,a[\gamma ]),({\gamma }^{\bullet },a^{\bullet }(E)))$.

Abstraction. Alpha-rename so that $t=\lambda y.b$ with $y\ne x$ and $y$ fresh for $a$ and the displayed environments. Meta-level functions are equal extensionally. Fix an admissible argument $(c,c^{\bullet })$. The weakening induction hypothesis for $b$, in the context also extended by $y$, gives $$b^{\bullet }((\gamma ,a,c),({\gamma }^{\bullet },a^{\bullet },c^{\bullet }))=b^{\bullet }((\gamma ,c),({\gamma }^{\bullet },c^{\bullet }));$$ therefore the two functions interpreting $\lambda y.b$ are equal. For substitution, the induction hypothesis for $b$ in the extended context gives Freshness identifies $(b[a/x])[\gamma ,c/y]$ with $b[\gamma ,a[\gamma ]/x,c/y]$, so pointwise equality proves the abstraction case.

$\mathrm{\Pi }$-types. The proof is the same binder argument, followed by extensionality of the displayed dependent products. For each closed argument $c$ and each $c^{\bullet }\in A^{\bullet }(c)$, apply the induction hypothesis to the codomain $B$ in the environment extended by $(c,c^{\bullet })$. The induction hypothesis for the domain identifies the sets of admissible pairs.

Boolean elimination. Apply the induction hypotheses to the scrutinee, motive, and both branches. The scrutinee evidence is the same on both sides, so both semantic eliminators select the same case, $0$ or $1$; the corresponding branch induction hypothesis proves equality. In the substitution case, alpha-rename the motive binder and use ordinary capture-avoiding substitution composition.

Every raw constructor is handled by one of these patterns: lookup, constant, nonbinding composition, or binding composition. This proves both clauses of lemma 49.11.

Fix a computable closing instantiation $E=(\gamma ,{\gamma }^{\bullet })\in {\mathrm{\Gamma }}^{\bullet }$.

$\lambda$-congruence. Suppose the final rule is $$\frac{\mathrm{\Gamma },x:A⊢b\equiv b^{\prime }:B}{\mathrm{\Gamma }⊢\lambda x.b\equiv \lambda x.b^{\prime }:\prod _{x:A}B}.$$ The two interpretations are dependent functions. Given any admissible $(a,a^{\bullet })$, induction hypothesis (d) for the premise, instantiated at $((\gamma ,a),({\gamma }^{\bullet },a^{\bullet }))$, gives $$b^{\bullet }((\gamma ,a),({\gamma }^{\bullet },a^{\bullet }))=b^{\prime \bullet }((\gamma ,a),({\gamma }^{\bullet },a^{\bullet })).$$ Thus the functions agree pointwise, and meta-level function extensionality gives equality of the two pieces of evidence.

Congruence for Boolean elimination. Write $$e={\mathsf{ind}}_{\mathbf{2}}(x.C;c_0,c_1;b),e^{\prime }={\mathsf{ind}}_{\mathbf{2}}(x.C^{\prime };c_0^{\prime },c_1^{\prime };b^{\prime }).$$ The congruence premises give, by the simultaneous induction hypotheses, $$C^{\bullet }=C^{\prime \bullet },c_0^{\bullet }=c_0^{\prime \bullet },c_1^{\bullet }=c_1^{\prime \bullet },b^{\bullet }=b^{\prime \bullet }.$$ The last equality means that both semantic eliminators inspect the same scrutinee evidence. If it is $1$, both select their first branch and use $c_0^{\bullet }=c_0^{\prime \bullet }$; if it is $0$, both select their second branch and use $c_1^{\bullet }=c_1^{\prime \bullet }$. No other case is reachable for a well-typed Boolean, by part (c). The motive equality identifies the result fibers.

Part (b) for $\mathrm{\Pi }$-congruence. Suppose the final rule has premises $$\mathrm{\Gamma }⊢A\equiv A^{\prime }\mathsf{type},\mathrm{\Gamma },x:A⊢B\equiv B^{\prime }\mathsf{type}$$ (with the usual conversion if the second context is displayed using $x:A^{\prime }$). By induction hypothesis (b), $A^{\bullet }(E)=A^{\prime \bullet }(E)$. Hence both products quantify over exactly the same closed $a$ and evidence $a^{\bullet }$. For each such pair, induction hypothesis (b) for the codomain premise at the extended instantiation gives $$B^{\bullet }((\gamma ,a),({\gamma }^{\bullet },a^{\bullet }))=B^{\prime \bullet }((\gamma ,a),({\gamma }^{\bullet },a^{\bullet })).$$ Every corresponding factor in the two dependent products is therefore equal, so the product families themselves are equal. This is exactly the claim required by part (b).

Extend the assignment by $${\mathbb{N}}^{\bullet }(E)(n)=\{m\in \mathbb{N}\mid \cdot ⊢n\equiv {\mathsf{suc}}^m(\mathsf{0}):\mathbb{N}\}.$$ The constructor clauses are $${\mathsf{0}}^{\bullet }(E)=0,(\mathsf{suc}(n){)}^{\bullet }(E)=n^{\bullet }(E)+1.$$ They are sound because reflexivity witnesses $\mathsf{0}\equiv {\mathsf{suc}}^0(\mathsf{0})$, and from $n\equiv {\mathsf{suc}}^m(\mathsf{0})$ congruence gives $\mathsf{suc}(n)\equiv {\mathsf{suc}}^{m+1}(\mathsf{0})$.

For the eliminator, let its motive be $C$, its zero branch have evidence $c_0^{\bullet }$, and its successor branch transform evidence at $m$ and for the recursive result into evidence at $m+1$. Define its semantic value by primitive recursion on the actual number $m=n^{\bullet }(E)$: The induction hypothesis for $n$ supplies $n[\gamma ]\equiv {\mathsf{suc}}^m(\mathsf{0})$. Congruence of the eliminator, followed by its zero or successor computation rule, places $R(m)$ in the required fiber. This validates the Nat eliminator case of the fundamental lemma.

Now let $\cdot ⊢n:\mathbb{N}$. Part (c) at the empty instantiation gives an actual $$m=n^{\bullet }((),())\in {\mathbb{N}}^{\bullet }((),())(n),$$ so, by definition, $$\cdot ⊢n\equiv {\mathsf{suc}}^m(\mathsf{0}):\mathbb{N}.$$ If also $n\equiv {\mathsf{suc}}^k(\mathsf{0})$, then the two numerals are judgmentally equal. Interpreting $\mathbb{N}$ as $\mathbb{N}$, or using constructor disjointness and successor injectivity, yields $m=k$. Thus the numeral is unique.

The eliminator needs the evidence value $m$, not merely the proposition that the evidence set is inhabited: $m$ determines how many successor-branch iterations define $R(m)$. Mere inhabitation would hide the recursion index.

Let $\cdot ⊢p:{\mathsf{Id}}_A(a,b)$. By the assumed term clause of the fundamental lemma, $p^{\bullet }$ belongs to the identity-evidence set displayed in remark 49.13. Hence it contains a pair $(q,r)$ with $$q:\cdot ⊢a\equiv b:A,r:\cdot ⊢p\equiv {\mathsf{refl}}_a:{\mathsf{Id}}_A(a,b).$$ The derivation $q$ is also what permits the reflexivity term, whose native type is ${\mathsf{Id}}_A(a,a)$, to be viewed at the displayed type of $r$. Thus the endpoint equality and the canonicity equation are stored in the evidence itself; no injectivity theorem for the identity former is used.

This closed calculation is conditional on the enlarged fundamental lemma named in the exercise. The open construction of lemma 111.74 proves the corresponding identity statement for $T_{\mathsf{impl}}$. By contrast, the local Tait proof has no identity or $J$ case, and the Coquand construction at $T_{\mathsf{Coq}}$ supplies no such clause. Neither of those two smaller arguments proves the identity result.

Eta-long readback expands at every negative type former.

1. The outer lambda is already present, but its body $f$ has function type and must itself be eta-expanded: $$\lambda f.\lambda x.fx.$$

2. The variable $g$ has two successive $\mathrm{\Pi }$-types, so its eta-long normal form is $$\lambda x.\lambda y.gxy.$$

3. The variable $h$ has a function type, so readback first introduces an argument $f:\mathbf{2}\to \mathbf{2}$. Because that argument is itself used at function type, its eta-long occurrence is $\lambda x.fx$. Hence the fully eta-long normal form is $$\lambda f.h(\lambda x.fx).$$ Both expansions are instances of the $\mathrm{\Pi }$-$\eta$ rule; no $\mathrm{\Sigma }$- or Unit clause is used.

The eta rule for $\mathbf{1}$ is precisely $$\frac{\mathrm{\Gamma }⊢t:\mathbf{1}}{\mathrm{\Gamma }⊢t\equiv \star :\mathbf{1}},$$ so every term of unit type is judgmentally $\star$.

Take the same raw term $x$ in two contexts: $$x:\mathbf{1}⊢x:\mathbf{1},x:\mathbf{2}⊢x:\mathbf{2}.$$ At $\mathbf{1}$, eta-long normalization returns $\star$. At $\mathbf{2}$, the variable is a neutral normal form, so normalization returns $x$. Thus the same raw syntax has different normal forms depending on its typing judgment.

A function that inspects only the raw term would have to return the same answer for these two inputs. Returning $x$ is incomplete at $\mathbf{1}$, while returning $\star$ is unsound at $\mathbf{2}$. Therefore normalization and readback must be indexed by the type and context.

Suppose $x:\mathbf{2}⊢x\equiv \mathsf{tt}:\mathbf{2}$. The substitution lemma with $x\mapsto \mathsf{ff}$ gives $\cdot ⊢\mathsf{ff}\equiv \mathsf{tt}:\mathbf{2}$, contradicting Boolean separation. Dually, a derivation of $x:\mathbf{2}⊢x\equiv \mathsf{ff}:\mathbf{2}$ and the substitution $x\mapsto \mathsf{tt}$ would give $\cdot ⊢\mathsf{tt}\equiv \mathsf{ff}:\mathbf{2}$, the same contradiction. This proof uses substitution and the closed separation theorem; it assumes no normalization result for open terms.

Encode finite derivation trees by natural numbers. Enumerate those codes, decode each candidate, and check recursively whether every node is an instance of a rule of the recursive signature and whether its root is the requested judgment $\mathrm{\Gamma }⊢t\equiv u:A$. Rule-instance checking and syntactic equality are effective, so each candidate is checked in finite time. If the judgment is derivable, its finite derivation eventually appears and the procedure halts with “yes.” Hence judgmental equality is semidecidable.

This is not a usable equality oracle. On unequal terms the search runs forever, so a type checker cannot reject a failed conversion, report an error, or continue. It also searches a vast space of irrelevant proof trees rather than computing a canonical representative. A kernel needs a total decision procedure, not merely eventual success on positive instances.

Fix effective enumerations of raw syntax and finite derivations. From the latter enumerate all tuples $$(\mathrm{\Delta },u,U,d)\text{with}d:\mathrm{\Delta }⊢u:U.$$ For an input derivation $e:\mathrm{\Gamma }⊢t:A$, scan this enumeration and retain entries whose context and type are syntactically $\mathrm{\Gamma }$ and $A$. Use the assumed equality decision procedure to test $\mathrm{\Gamma }⊢t\equiv u:A$. Return the first $u$ for which the test succeeds; call it $\mathsf{nf}(e)$.

The search terminates constructively. The input derivation $e$ itself is a finite derivation of a represented term equal to $t$ by reflexivity, so its code occurs at a finite position. A successful candidate is therefore guaranteed no later than that position. This is an ordinary terminating search with an explicit termination witness, not an appeal to a classical search principle.

Because the enumeration order is fixed, $\mathsf{nf}(e)$ depends only on the judgmental-equality class of $t$. If $t\equiv t^{\prime }:A$, a candidate $u$ that passes for $t$ satisfies $t\equiv u:A$. Compose the converse $t^{\prime }\equiv t:A$ of the assumed equality with that derivation to obtain $t^{\prime }\equiv u:A$. The converse implication exchanges $t$ and $t^{\prime }$ and uses the converse equality $t\equiv t^{\prime }:A$. Thus a candidate passes for $t$ exactly when it passes for $t^{\prime }$; hence the first successful candidate is the same. Conversely, if the returned syntax trees agree, each input is judgmentally equal to that common representative, so the inputs are judgmentally equal. The successful test also supplies soundness $t\equiv \mathsf{nf}(e):A$. Repeating the construction for well-formed types gives the type component. These maps, together with the stated soundness, completeness, and injectivity properties, form the normalization structure of definition 49.16.

The representatives are least derivation codes, not pleasant beta-eta normal syntax. The construction establishes existence, not efficiency.

We use the definitions of the Kripke domain and evaluation from definition 49.24, definition 49.25.

Restriction. First prove by induction on $T$ that restriction on $[[T]]$ is functorial: $$a{\upharpoonright }_{\mathrm{\Gamma }}=a,(a{\upharpoonright }_{\mathrm{\Delta }}){\upharpoonright }_{\mathrm{\Theta }}=a{\upharpoonright }_{\mathrm{\Theta }}(\mathrm{\Theta }⊒\mathrm{\Delta }⊒\mathrm{\Gamma }).$$ At the base type this is composition of weakening for neutral syntax. At $S\to T$ it follows pointwise from the definition of restriction of a Kripke family and the induction hypothesis for $T$.

Now prove $$\begin{array}{}\text{(}1\text{)}& [[t]](\rho {\upharpoonright }_{\mathrm{\Theta }})=([[t]]\rho ){\upharpoonright }_{\mathrm{\Theta }}\end{array}$$ by structural induction on $t$. For a variable, (1) is the definition of restriction of an environment. For application, use the two induction hypotheses and naturality of a Kripke function. For an abstraction, compare the two semantic functions at every further extension $\mathrm{\Xi }⊒\mathrm{\Theta }$ and argument $a$. Both reduce to $$[[b]](\rho {\upharpoonright }_{\mathrm{\Xi }},x\mapsto a),$$ using functoriality; function extensionality concludes.

Evaluation and substitution. Prove $$\begin{array}{}\text{(}2\text{)}& [[t[s/x]]]\rho =[[t]](\rho ,x\mapsto [[s]]\rho )\end{array}$$ by structural induction on $t$. If $t=x$, both sides are $[[s]]\rho$; if $t=y\ne x$, both are $\rho (y)$. Application follows from the two induction hypotheses. For $t=\lambda y.b$, alpha-rename $y$ fresh for $s$ and $x$. At an extension $\mathrm{\Theta }$ and argument $a$, both functions reduce, using the induction hypothesis for $b$, to $$[[b]](\rho {\upharpoonright }_{\mathrm{\Theta }},x\mapsto [[s]](\rho {\upharpoonright }_{\mathrm{\Theta }}),y\mapsto a).$$ Equation (1) identifies the restricted value of $[[s]]\rho$ with $[[s]](\rho {\upharpoonright }_{\mathrm{\Theta }})$.

Closure under equality on the left. Induct on $T$. At $\iota$, from $t^{\prime }\equiv t$ and $t\equiv u$, transitivity gives $t^{\prime }\equiv u$. At $S\to T$, given a future context and related argument, congruence gives $ts\equiv t^{\prime }s$; the induction hypothesis at $T$ transfers the relation to $t^{\prime }s$.

Closure under restriction. Again induct on $T$. At $\iota$, weaken the equality $t\equiv u$ to the larger context. At $S\to T$, pass to an arbitrary further extension and related argument. Functoriality identifies twice-restricted and directly restricted semantic functions, and the induction hypothesis at $T$ supplies the result relation.

Clause by clause, (2) is lemma 49.11(2): environments are closing instantiations, variables are lookups, abstraction extends an environment, application applies semantic values, and eliminators inspect semantic constructor evidence. Equation (1) is the Kripke analogue of lemma 49.11(1). Thus the computability assignment is an evaluation into a proof-relevant semantic domain.

Prove simultaneously, by induction on the displayed normal and neutral derivations,

For a neutral variable, $\mathcal{E}$ is the definition of the identity environment. For a neutral application $uv$, the induction hypotheses give $$[[u]]{\rho }_{\mathrm{\Gamma }}={\uparrow }^{S\to T}(u),{\downarrow }^S([[v]]{\rho }_{\mathrm{\Gamma }})=v.$$ By the arrow-reflection clause, applying the first value to the second produces ${\uparrow }^T(uv)$, proving $\mathcal{E}(uv)$. Neutral eliminators are identical: evaluation takes the stuck semantic clause, and the induction hypotheses reify every stored minor argument to the original normal syntax.

At a base type, a normal neutral $u$ is handled by $\mathcal{E}(u)$ and the fact that base reification of reflected neutral syntax is the identity. Constructor normal forms are immediate or follow recursively on their normal arguments. For a normal abstraction $\lambda x.b$, reification of its evaluated closure introduces a fresh reflected variable $x$. Applying the closure to that variable evaluates $b$ in the extended identity environment; the induction hypothesis for $b$ reifies the result to $b$. Thus readback returns exactly $\lambda x.b$. Pair and other eta-long cases work componentwise because their readback clauses mirror their normal-form rules. This completes the mutual induction and proves ${\mathsf{nf}}_{\mathrm{\Gamma }}^T(v)=v$.

Existence of a normal representative follows from normalization. For uniqueness, let $v,w$ be normal forms of the same type with $v\equiv w$. Completeness gives $\mathsf{nf}(v)=\mathsf{nf}(w)$, while the result just proved reduces this to $v=w$ as alpha-equivalence classes of syntax. Soundness says every term is judgmentally equal to its normal form. Hence every judgmental-equality class contains exactly one normal form.

Use the disjoint-sum presentation $$[[\mathbf{2}]](\mathrm{\Gamma })=\{{\mathsf{tt}}^{\mathsf{v}},{\mathsf{ff}}^{\mathsf{v}}\}+\{u\mid \mathrm{\Gamma }⊢u\mathsf{ne}\mathbf{2}\},$$ so constructor values cannot be confused with neutral syntax. Restriction fixes the two constructors and weakens a neutral. Reflection embeds a neutral into the third summand, while reification is $${\downarrow }^{\mathbf{2}}({\mathsf{tt}}^{\mathsf{v}})=\mathsf{tt},{\downarrow }^{\mathbf{2}}({\mathsf{ff}}^{\mathsf{v}})=\mathsf{ff},{\downarrow }^{\mathbf{2}}(\mathsf{neu}(u))=u.$$ Evaluation sends the syntactic constructors to their semantic counterparts.

For a non-dependent recursor with result type $T$, define In the last line, readback and reflection are taken in the current context; at function result types this automatically eta-expands the stuck eliminator. Evaluation of a syntactic recursor evaluates its branches and scrutinee and applies this operation. Naturality follows from naturality of reflection and reification.

The two new computation cases in completeness are definitionally true in the semantic domain. For example, With $\mathsf{ff}$, the same calculation returns $[[c_1]]\rho$. Thus the two judgmental computation rules are respected by evaluation.

Extend the value and neutral grammars by Define semantic projections by Evaluation acquires the clauses The semantic typing relation records that the second projection has type $F(d_1)$, where $d_1$ is the first projection.

Reflection at a Sigma type eta-expands a neutral. Put For an arbitrary semantic value $d$, let $d_1={\mathsf{fst}}^{\mathsf{v}}(d)$ and $d_2={\mathsf{snd}}^{\mathsf{v}}(d)$. Reification is $$\begin{array}{}\text{(}2\text{)}& {\downarrow }_{\hat{\mathrm{\Sigma }}(A,F)}^n(d)=({\downarrow }_A^n(d_1),{\downarrow }_{F(d_1)}^n(d_2)).\end{array}$$ Type-code readback gains the corresponding clause for a syntactic Sigma, using a reflected fresh variable to reify the codomain family.

For a semantic constructor pair, the projections establish both beta rules definitionally. For a reflected neutral $e$, equations (1) and (2) read it back as $$({\mathsf{pr}}_1({\mathsf{R}}_{n}e),{\mathsf{pr}}_2({\mathsf{R}}_{n}e)),$$ which is judgmentally equal to ${\mathsf{R}}_{n}e$ by Sigma eta. Hence readback respects beta and eta and always returns eta-long Sigma normal forms.

Define universe equality and element equality simultaneously. Write $$\alpha :c{\approx }_{{\mathcal{U}}_0}{c}^{\prime }@n$$ for a proof-relevant derivation that two semantic values are related universe codes at support world $n$. Let $D_n$ be the values admissible at that support and let ${\mathsf{El}}_n(\alpha )\subseteq D_n\times D_n$ be the PER of their elements, defined by recursion on $\alpha$. A membership derivation contains the two endpoint-admissibility premises; it is not membership in an unindexed relation on raw $D$.

For the closed $\hat{\mathbf{2}}/\hat{\mathrm{\Pi }}$ fragment the generators are as follows.

Boolean code. There is a constructor $${\mathsf{bool}}_n:\hat{\mathbf{2}}{\approx }_{{\mathcal{U}}_0}\hat{\mathbf{2}}@n.$$ Its element PER is the least symmetric and transitive relation containing $$\widehat{\mathsf{tt}}{\mathsf{El}}_n({\mathsf{bool}}_n)\widehat{\mathsf{tt}},\widehat{\mathsf{ff}}{\mathsf{El}}_n({\mathsf{bool}}_n)\widehat{\mathsf{ff}},$$ and, in open contexts, corresponding related neutral Boolean values. It contains no true–false pair.

Dependent-function code. Suppose $\alpha :A{\approx }_{{\mathcal{U}}_0}{A}^{\prime }@n$ has finite support world $n$. For every relational world substitution $\mathit{\sigma }=({\sigma }_0,{\sigma }_1;q):n\Rightarrow m$ and witness $\zeta :d{\mathsf{El}}_m({\mathit{\sigma }}_{\ast }\alpha )d^{\prime }$, require a derivation $${\beta }_{\mathit{\sigma },\zeta }:({\sigma }_{0\ast }F)(d){\approx }_{{\mathcal{U}}_0}({\sigma }_{1\ast }{F}^{\prime })(d^{\prime })@m.$$ Require naturality ${\mathit{\tau }}_{\ast }{\beta }_{\mathit{\sigma },\zeta }={\beta }_{\mathit{\tau }\circ \mathit{\sigma },{\mathit{\tau }}_{\ast }\zeta }$. Then $$\mathsf{pi}(\alpha ,\beta ):\hat{\mathrm{\Pi }}(A,F){\approx }_{{\mathcal{U}}_0}\hat{\mathrm{\Pi }}(A^{\prime },F^{\prime })@n.$$ Define its element PER by The relational substitution carries the support evidence that an arbitrary semantic assignment would lack. Binder extension appends the supplied $\zeta$; formation of that witness gives $d,d^{\prime }\in D_m$. The new values may therefore contain variables from target gaps but no level outside $m$. Hence (1) is required at every future context extension and is stable under composition, not merely at the support world. Symmetry and transitivity of the universe relation, and of every element relation, are defined recursively on these constructors.

The ambiguity is now visible. If universe computability were merely the proposition “$c$ is convertible to a code,” one proof might present $c$ as $\hat{\mathbf{2}}$ and another as $\hat{\mathrm{\Pi }}(A,F)$. Recursing on those proofs would assign incompatible element PERs to $\mathsf{El}(c)$.

The indexed inductive family prevents this by no-confusion for code tags. A $\mathsf{bool}$ derivation relates only two $\hat{\mathbf{2}}$ tags, whereas a $\mathsf{pi}$ derivation relates only two $\hat{\mathrm{\Pi }}$ tags; the tags are disjoint and the Pi tag is injective. Induction on two derivations with the same endpoints proves functionality: $$\begin{array}{}\text{(}2\text{)}& \alpha ,{\alpha }^{\prime }:c{\approx }_{{\mathcal{U}}_0}{c}^{\prime }⟹{\mathsf{El}}_n(\alpha )={\mathsf{El}}_n({\alpha }^{\prime }).\end{array}$$ In the Pi case, (2) follows recursively for the domain and every codomain relation. Equivalently, semantic codes may be records carrying a constructor tag and their element PER; universe relatedness then matches records by tag. Evidence remains proof-relevant, but the PER it carries is coherent and constructor-determined. That is the information a truth-valued predicate would lose.

Reflecting $x:\mathbf{2}\to \mathbf{2}$ produces the semantic function $d\mapsto {\uparrow }_{\mathbf{2}}(x{\downarrow }_{\mathbf{2}}d)$; reification at the function type yields the eta-long normal form $\lambda y.xy$. For the specified middle term, evaluation leaves the exact neutral spine $${\mathsf{ind}}_{\mathbf{2}}(y.\mathbf{2};\mathsf{tt},\mathsf{ff},x)$$ stuck: its principal is the neutral $x$, its constant motive has fiber $\mathbf{2}$, and its two branch values reify to $\mathsf{tt}$ and $\mathsf{ff}$ in that fiber. Reflection at $\mathbf{2}$ stores this spine, and reification at $\mathbf{2}$ returns precisely the same displayed term. For $p:(\mathbf{2}\to \mathbf{2})\to \mathbf{2}$, reflection and reification introduce a fresh function variable $f$ and then eta-expand that variable at its own function type. The result is $$\lambda f.p(\lambda x.fx).$$ The indices $\mathbf{2}\to \mathbf{2}$, the eliminator motive, and $(\mathbf{2}\to \mathbf{2})\to \mathbf{2}$ select the argument reflection, branch readback, and two nested function-readback clauses. An untyped operation cannot know which eta-expansions or motive fibers to use.