Nuprl-Style Computational Type Theory and Realizability

Proof. Proceed simultaneously by stratum. Within one stratum prove four separate statements by induction on closure derivations: assigned relations are PERs, type equality is symmetric, composable type equalities are transitive, and two derivations with the same endpoints assign logically equivalent relations. Evaluation saturation uses determinism: the endpoints have unique canonical heads. Constructor no-confusion then selects the same generator, and constructor injectivity aligns its premises.

For integers, symmetry and transitivity are the corresponding properties of (91.1). For functions, suppose $R_{\mathrm{\Pi }}(f,g)$ and $R_{\mathrm{\Pi }}(g,h)$. The PER laws applied to $R_A(a,c)$ give $R_A(c,c)$. By the first hypothesis at $(a,c)$, $R_B^{a,c}(fa,gc)$, and by the second at $(c,c)$, $R_B^{c,c}(gc,hc)$. Definition 91.5 identifies these fiber PERs; their transitivity gives $R_B^{a,c}(fa,hc)$. For symmetry, take $R_A(a,a^{\prime })$. Symmetry of the domain relation gives $R_A(a^{\prime },a)$, so the original function relation at $(a^{\prime },a)$, followed by symmetry in $R_B^{a^{\prime },a}$, gives $R_B^{a^{\prime },a}(ga,f{a}^{\prime })$. A second use of functional family invariance transports this fact from $R_B^{a^{\prime },a}$ to $R_B^{a,a^{\prime }}$, as required for $R_{\mathrm{\Pi }}(g,f)$.

For dependent pairs, the two hypotheses evaluate their common middle program to two pair values. By determinism, those values are the same pair. Transitivity of $R_A$, definition 91.5, and transitivity of the fiber PER then relate the outer components. Symmetry reverses the two evaluations and uses symmetry in both component PERs.

For an equality type, the assigned relation is empty when $R_A(a,b)$ fails. When it holds, every related term evaluates to $\mathsf{axiom}$, so symmetry and transitivity follow from determinism. For a set type, transitivity of $R_A$ relates the endpoints. Definition 91.5 identifies the predicate PERs at the three related inputs, so a witness of the middle predicate transports to a witness at the composite endpoints. The same identification proves symmetry.

For symmetry of type equality, reverse the domain premise and every functional fiber premise, then rebuild the same generator. For transitivity, canonicalize the common middle type. No-confusion forces the two derivations to have the same constructor tag; apply type transitivity recursively to the domain and fibers and rebuild that generator. For unique valuation, no-confusion and injectivity again align the two derivations. By the induction hypotheses, their domain and fiber PERs are logically equivalent, so the defining formulas equation 91.2, equation 91.3, equation 91.4, equation 91.5 are logically equivalent. This proves the three type-system properties rather than inferring them from the element-PER proof.

Finally, (91.6) uses all four induction hypotheses one stratum lower. Symmetry of ${\mathcal{C}}_i$ gives symmetry of $R_{{\mathcal{U}}_i}$. For transitivity, choose ${\mathcal{C}}_i(A,B,R)$ and ${\mathcal{C}}_i(B,D,S)$. Symmetry followed by type transitivity gives both ${\mathcal{C}}_i(B,B,R)$ and ${\mathcal{C}}_i(B,B,S)$. Unique valuation at the common endpoints $(B,B)$ identifies $R$ and $S$; only after this identification does type transitivity compose the two original closure triples to ${\mathcal{C}}_i(A,D,R)$. Thus $R_{{\mathcal{U}}_i}$ is a PER. The same unique valuation argument makes the relation selected by any universe witness independent of that witness, and constructor no-confusion handles the universe generator. These cases exhaust the generators of definition 91.7. ◻

Proof. We prove both directions simultaneously with a strengthened induction hypothesis. Let $P(h)$ and $R(h)$ be the two conclusions for every finite compatible reduction whose known evaluation derivation has height at most $h$. Use strong induction on $h$, and inside it induction on the length of the reduction. The strong form is essential: substitution may duplicate a redex, so the residual tail can contain more contractions than the incoming reduction, but its evaluation derivation is strictly shorter.

The required residual calculation is structural induction on the program with capture-avoiding renaming at binders: The first implication contains one residual for every free occurrence of $x$; if $x$ is absent it is reflexive. Iterating the two equations handles a finite reduction of either the body or the argument.

We use one further decomposition, proved by induction on the compatible contexts in the reduction trace. Relative to the next lazy rule, every step is either in its demanded principal argument, is that root rule, or is disjoint from the demanded position. Disjoint steps commute past the demand; after beta or spread their residuals are exactly those in (91.7), (91.8). Hence a finite trace factors into a trace on the demanded argument, at most one demanded root contraction, and a finite trace on the evaluation tail. This demand–residual decomposition also holds in reverse: reinsert the same root contraction and commute disjoint steps back across it. The proof uses no confluence claim; it is a case analysis on beta, spread, and the four displayed integer schemes.

Now inspect the known evaluation. If its source is canonical, no root rule applies. Every compatible step is below the same constructor, so the target is canonical and definition 91.9 holds for all stored components, including lambda bodies, dependent fibers, equality endpoints, and set predicates.

For an application, first apply $P(h^{\prime })$ or $R(h^{\prime })$, with , to the evaluation of its operator. The resulting lambda bodies are computationally convertible. The demand–residual decomposition and the two substitution equations make the beta tails $b[a/x]$ and $b^{\prime }[a^{\prime }/x]$ computationally convertible by a finite sequence in the required direction. The given evaluation of the first tail is a strict subderivation, so the strong hypothesis applies again and gives the same component-convertible observation. The spread case is identical with the two tail programs $c[a/x,b/y]$ and $c^{\prime }[a^{\prime }/x,b^{\prime }/y]$. This is why the proof does not claim that the tails are syntactically the same.

For an integer operation, apply the strong hypothesis successively to the demanded operands. Component conversion of integer observations is literal integer equality, so the same displayed arithmetic or comparison rule fires. A step in an undemanded program is carried into the shorter tail by the decomposition. A discarded beta argument gives the reflexive, zero-residual case. These cases exhaust the frozen program contexts and root contractions. They establish $P(h)$; reading the same decomposition from target to source and using $R(h^{\prime })$ on each strict evaluation subderivation establishes $R(h)$. Strong induction proves both conclusions. ◻

Proof. Choose the finite zigzag of compatible contractions and reverse contractions that generates $t{\equiv }_{\mathcal{L}}u$. Starting with $t\Downarrow v$, apply the preservation clause of lemma 91.10 at a forward edge and its reflection clause at a reverse edge. Induction on the zigzag length produces an observation at every vertex. The same induction preserves the canonical outer tag and composes the immediate component conversions. Congruence under every canonical constructor shows that component conversion implies conversion of the whole canonical programs. Its final vertex is $u$, which gives the required $w$. ◻

Proof. Proceed simultaneously by stratum, closure derivation, and generation of ${\equiv }_{\mathcal{L}}$. It suffices to treat one compatible contraction; symmetry and transitivity then give arbitrary conversions. A contraction at a type root is removed or inserted by evaluation saturation. A contraction inside a canonical type constructor is handled by the induction hypothesis on the corresponding domain, endpoint, or fiber premise, after which the same generator rebuilds the closure triple. When a contraction exposes a canonical root, lemma 91.11 gives the matching observation. Constructor no-confusion ensures that no other root case occurs.

For the member relation, lemma 91.11 preserves the unique integer observed by (91.1). In the function case, congruence gives $fu{\equiv }_{\mathcal{L}}{f}^{\prime }u$ and $g{u}^{\prime }{\equiv }_{\mathcal{L}}{g}^{\prime }{u}^{\prime }$; the fiber induction hypothesis applied in (91.2) proves the equivalence. In the dependent-pair case, let $p,q,p_0,q_0$ be closed programs satisfying $R_{\mathrm{\Sigma }}(p,q)$, $p{\equiv }_{\mathcal{L}}{p}_0$, and $q{\equiv }_{\mathcal{L}}{q}_0$. Write the original observations as $$p\Downarrow (a,b),q\Downarrow (a^{\prime },b^{\prime }),$$ with $R_A(a,a^{\prime })$ and $R_B^{a,a^{\prime }}(b,b^{\prime })$. Lemma 91.11 gives observations $p_0\Downarrow (a_0,b_0)$ and $q_0\Downarrow (a_0^{\prime },b_0^{\prime })$, where corresponding components are computationally convertible. Stability of $R_A$ gives $R_A(a_0,a_0^{\prime })$. The PER laws first give $R_A(a,a)$ and $R_A(a^{\prime },a^{\prime })$; applying stability to one endpoint at a time then gives $R_A(a,a_0)$ and $R_A(a^{\prime },a_0^{\prime })$. Functionality of the family therefore identifies $R_B^{a,a^{\prime }}$ with $R_B^{a_0,a_0^{\prime }}$. Stability of that fiber relation transports $R_B^{a,a^{\prime }}(b,b^{\prime })$ to $R_B^{a_0,a_0^{\prime }}(b_0,b_0^{\prime })$. These are exactly the witnesses required by (91.3) for $p_0,q_0$. In the equality case, the same lemma preserves evaluation to $\mathsf{axiom}$. In the set case, apply the domain induction hypothesis to the ambient conjunct. If that conjunct holds, the PER laws give $R_A(t,t)$ and $R_A(u,u)$. The induction hypothesis for the ambient relation then gives $R_A(t,t^{\prime })$ and $R_A(u,u^{\prime })$ for converted representatives $t^{\prime },u^{\prime }$. Functionality identifies the two predicate-fiber PERs, so their inhabitance agrees. Finally, a universe member relation is a lower-stratum closure triple by (91.6); apply the closure-assignment half of the simultaneous induction one stratum lower. These are all generators of definition 91.7. ◻

Proof. Use closure induction on the well-founded generated derivation. An evaluation saturation step over canonical endpoints has, by determinism, the same canonical heads, so apply the induction hypothesis to its smaller premise. At the generating step, constructor no-confusion selects the unique matching generator and constructor injectivity recovers its arguments. Its premises and its defining PER clause are therefore exactly those in definition 91.7.

For transport, symmetry turns the cross derivation around without changing its assigned relation up to logical equivalence. Compose the two directions through $B$ and through $A$ to obtain self-endpoint derivations. Unique valuation at the identical endpoint pairs identifies their relations with $R_A$ and $R_B$, respectively. ◻

Proof. By definition 91.14, the left side of (91.9) says that some relation assigned to the self-pair $({\mathcal{U}}_i,{\mathcal{U}}_i)$ at level $i+1$ relates $A$ and $B$. Unique valuation in theorem 91.8 identifies that relation with $R_{{\mathcal{U}}_i}$. Unfolding (91.6) now gives $$R_{{\mathcal{U}}_i}(A,B)⟺\mathrm{\exists }R.{\mathcal{C}}_i(A,B,R),$$ which is exactly ${\mathsf{TyEq}}_i(A,B)$.

The integer generator gives ${\mathcal{C}}_0(\mathsf{Int},\mathsf{Int},R_{\mathbb{Z}})$, so the equivalence at $i=0$ puts $\mathsf{Int}$ in ${\mathcal{U}}_0$ at level $1$. The universe generator gives ${\mathcal{C}}_{i+1}({\mathcal{U}}_i,{\mathcal{U}}_i,R_{{\mathcal{U}}_i})$; applying the equivalence at $i+1$ puts ${\mathcal{U}}_i$ in ${\mathcal{U}}_{i+1}$ at level $i+2$. Finally, ${\mathcal{C}}_j$ extends ${\mathcal{C}}_i$ when $j\ge i$, so every witness for type or member equality at level $i$ is also a witness at level $j$. ◻

Proof. The integer generator assigns $R_{\mathbb{Z}}$ to $\mathsf{Int}$. If $R_{\mathbb{Z}}(t,u)$, both programs evaluate to one integer $z$. The two predicate programs ${\mathsf{Le}}_{\mathbb{Z}}(0,t)$ and ${\mathsf{Le}}_{\mathbb{Z}}(0,u)$ therefore evaluate to the same canonical equality type: ${\mathsf{Eq}}_{\mathsf{Int}}(0,0)$ when $z\ge 0$ and ${\mathsf{Eq}}_{\mathsf{Int}}(0,1)$ otherwise. The equality-type generator and evaluation saturation assign the same PER to those fibers. This verifies definition 91.5; the set generator applied to (91.10) derives ${\mathsf{Ty}}_i(\mathbb{N})$. ◻

Proof. By lemma 91.17, the set generator assigns a PER to $\mathbb{N}$. Unfold the set clause (91.5). Its first conjunct is the integer relation (91.1); it gives an integer $n$ to which the programs evaluate. Its second conjunct says that ${\mathsf{Le}}_{\mathbb{Z}}(0,n)$ is inhabited. By definition 91.16, this happens exactly when $n\ge 0$. This proves both directions of (91.12); the reflexive instance is (91.11). Determinism gives the uniqueness of $n$. ◻

Proof. Induct on $\mathrm{\Gamma }$. For the empty telescope, its unique substitution is self-equal. For an extension, write the final components as $a,b$. By the induction hypothesis, each prefix is self-equal. The cross-extension premise relates $a,b$ in the PER assigned to the left type instance. PER symmetry and transitivity give self-relations for $a$ and $b$. By pointwise functionality, the left and right type instances are equal, and the transport clause of corollary 91.13 identifies their assigned PERs. Consequently the self-relation for $a$ extends the left prefix and the self-relation for $b$ extends the right prefix. ◻

Proof. This is the imported lemma sequent_true_eq_VR in the pinned per/sequents.v. Its proof is the chain $$\begin{array}{c}\mathtt{\text{sequent\_true\_eq\_KC}},\mathtt{\text{sequent\_true\_KC\_eq\_AN}},\\ \mathtt{\text{AN\_sequent\_true\_eq\_VR}}.\end{array}$$ The intermediate KC and AN meanings account for the artifact’s full records, including coverage and the functionality condition on hypotheses. This is an external theorem of the pinned source, not a local induction on the fixed-level relation. Every relation in the chain is the global artifact relation; no quotient clause and no indexed ${\mathcal{C}}_i$ is used. ◻

Proof. The first claim is a change of representation: lists and their simultaneous substitutions determine one another componentwise, and local similarity was defined to be ${\equiv }_{\mathrm{\Gamma }}$. The two displayed conjuncts are therefore exactly (91.14).

For the binary claim, fix $\sigma {\equiv }_{\mathrm{\Gamma }}\tau$. By lemma 91.20, both endpoint substitutions are self-equal. Write $R$ for the PER assigned to the equal instances of $A$. The three indicated instances of binary open equality give $$R(a[\sigma ],b[\sigma ]),R(a[\sigma ],b[\tau ]),R(a[\tau ],b[\tau ])$$ by using respectively $(\sigma ,\sigma )$, $(\sigma ,\tau )$, and $(\tau ,\tau )$. Symmetry and transitivity give $R(a[\sigma ],a[\tau ])$ and $R(b[\sigma ],b[\tau ])$. The equality-former case of corollary 91.13, together with its transport clause, identifies these endpoint relations with the cross assignment used by the equality-type generator. Hence the two equality-type instances are equal, and the same-substitution first relation makes $\mathsf{axiom}$ a member by (91.4).

Conversely, local truth gives $R(a[\sigma ],b[\sigma ])$. By the equality type conjunct and corollary 91.13, $R(b[\sigma ],b[\tau ])$ holds after transport to the ambient assignment. Their transitive composite is $R(a[\sigma ],b[\tau ])$, the member equality required by the binary open judgment. The ambient type equality is already a premise of the equality type generator. ◻

Proof. Fix $\sigma {\equiv }_{\mathrm{\Gamma }}\tau$ throughout. For C-$\mathrm{\Pi }$-I, choose $u,u^{\prime }$ related in the self-assignment for $A[\sigma ]$. Extend the substitutions by $x\mapsto u$ and $x\mapsto u^{\prime }$. By the introduction premise, $$R_B^{u,u^{\prime }}(b[\sigma ,u/x],b^{\prime }[\tau ,u^{\prime }/x]).$$ Here the superscript denotes the fiber relation recovered by the $\mathrm{\Pi }$-case of corollary 91.13; its transport clause moves the premise’s left-self assignment to that fiber relation. This is exactly the pointwise obligation in (91.2). The function generator applied to the functional domain and codomain families first establishes ${\mathsf{TyEq}}_i((\prod _{x:A}B)[\sigma ],(\prod _{x:A}B)[\tau ])$. Beta contraction turns the applications of the two lambdas into the terms in the displayed fiber relation. By theorem 91.12, that relation therefore holds of the two applications, as required by (91.2).

For C-$\mathrm{\Pi }$-E, invert the function premise with corollary 91.13. Its member conjunct is the function PER of (91.2). By the argument premise at $(\sigma ,\tau )$, $$R_A(a[\sigma ],a^{\prime }[\tau ]),$$ in the left domain assignment, so the function PER gives the required output relation after fiber transport. In the conclusion’s type-equality conjunct, the right endpoint still substitutes $a$, not $a^{\prime }$. The required pair is exactly $${\mathsf{TyEq}}_i(B[a/x][\sigma ],B[a/x][\tau ]).$$ Endpoint self-equality permits the argument-premise instance at $(\tau ,\tau )$, so $R_A(a[\tau ],a^{\prime }[\tau ])$. Inverting this edge gives $R_A(a^{\prime }[\tau ],a[\tau ])$; composing it after the cross edge $R_A(a[\sigma ],a^{\prime }[\tau ])$ gives $R_A(a[\sigma ],a[\tau ])$. Hence $$\sigma [a[\sigma ]/x]{\equiv }_{\mathrm{\Gamma },x:A}\tau [a[\tau ]/x].$$ By functionality of $B$, the displayed type equality holds.

For C-$\mathrm{\Sigma }$-I, the Sigma generator establishes the conclusion-type equality, and both pair terms are canonical without evaluating their components. By the first premise, $R_A(a[\sigma ],a^{\prime }[\tau ])$. The second premise is stated in the left substituted fiber; functionality and the transport clause of corollary 91.13 identify its assigned PER with $R_B^{a[\sigma ],a^{\prime }[\tau ]}$. This is the final fiber conjunct of (91.3). For elimination, invert the Sigma member premise with corollary 91.13. Equation (91.3) then gives $$p[\sigma ]\Downarrow (a,b),q[\tau ]\Downarrow (a^{\prime },b^{\prime }),$$ with $R_A(a,a^{\prime })$ and $R_B^{a,a^{\prime }}(b,b^{\prime })$. Extend $\sigma ,\tau$ by the two components and use the branch premise; the transport clause of corollary 91.13 aligns its member relation with the cross-assignment for $C((a,b))$ and $C((a^{\prime },b^{\prime }))$. After the displayed evaluations expose the pair values, the root contractions are By theorem 91.12, the branch equality transports across these contractions to the two eliminator terms while they remain in the self-assignment for $C((a,b))$. The same theorem transports that closure assignment along $$C(p)[\sigma ]{\equiv }_{\mathcal{L}}C((a,b)),$$ and unique valuation identifies the resulting member relation with the self-assignment for $C(p)[\sigma ]$. For the conclusion’s type-equality conjunct, the Sigma premise at $(\tau ,\tau )$, together with its cross instance, symmetry, and transitivity, relates $p[\sigma ]$ to $p[\tau ]$. Functionality of the open family $C$ therefore gives the exact conclusion ${\mathsf{TyEq}}_i(C(p)[\sigma ],C(p)[\tau ])$.

This computation premise is essential. If $fx$ is a neutral program with no pair value, then $\mathsf{spread}(fx;y,z.y)$ has no spread contraction; the eliminator does not project through a neutral merely because its result type is a dependent pair. ◻