In this series, let us check out the denotational semantics of typed lambda calculus, which uses models to express the meaning of terms.
For most logical systems, a model provides a mechanism for giving mathematical meaning to each well-formed expression, in sufficient detail to determine whether any formula of the logic is true. For logic with variables, it is common to separate the assignment of values to variables from the general notion of model.
For example, an algebra provides a set of possible values for each variable and an interpretation for each function symbol. After choosing values for variables (by selecting an environment), we use the functions given by the algebra to determine the value of an algebra term. By doing this for two terms, we may determine whether an equation between algebra terms holds.
In a model for typed lambda calculus, we require a set of possible values for each variable and an interpretation for each constant symbol that appears in the signature. This means that we need a set of values for each type, and a specific one of these chosen for each constant symbol.
However, that is not all. We have to make sense of application and lambda abstraction. More specifically, suppose $A^{\sigma \to \tau}$ is the set of values of type $\sigma \to \tau$, and $A^{\sigma}$ is similarly the set of values of type $\sigma$. If $f \in A^{\sigma \to \tau}$ and $x \in A^{\sigma}$, then we need to be able to apply $f$ to $x$.
The simplest condition on models that would make this possible is to require that $A^{\sigma \to \tau}$ be a set of functions from $A^{\sigma}$ to $A^{\tau}$. The ordinary function application would give us $f(x)$ in the set of values for type $\tau$.
A subtle issue here is that we also need to be able to interpret every lambda abstraction, which means that every lambda-definable function will exist and must lie in the appropriate set of values. If we impose the stronger requirement that $A^{\sigma \to \tau}$ must be a set of all functions from $A^{\sigma}$ to $A^{\tau}$, then certainly every lambda-definable function will exist in the model, and we can interpret every well-typed lambda term as a value in the correct set.
What makes the model theory of typed lambda calculus complicated is that we need to be relatively flexible about the interpretation of function types. We cannot simply say that in any model $\mathcal{A}$, $A^{\sigma \to \tau}$ must be the set of all functions from $A^{\sigma}$ to $A^{\tau}$. The main reason is that we need to be able to interpret constants such as $fix$, whose equational axiom forces every function to have a fixed point. If $A^\sigma$ has more than one element, then there exists at least one function on $A^\sigma$ without a fixed point. Therefore, if we force $A^{\sigma}$ to $A^{\tau}$ to contain all functions, we cannot have models for PCF, or any other typed lambda theory involving fixed points. This requires us to define models using a more flexible, and more abstract condition on function spaces.
There are several equivalent definitions of “general models,” which we will call Henkin models after Completeness in the theory of types, L Henkin. The definition we use has three parts. We first define typed applicative structures, and then specify two additional conditions that applicative structures must have to be models.
Readers should read the series Easy Foundations for Programming Languages before this article to avoid encountering unknown concepts.
Applicative Structures, Extensionality and Frames
A typed applicative structure $\boldsymbol{\mathcal{A}}$ for $\lambda^\to$ signature $\Sigma$ is a tuple
\[\langle \{ A^\sigma\}, \{ \mathbf{App}^{\sigma,\tau}\} , Const \rangle\]of families of sets and mappings indexed by type expressions over the type constants from $\Sigma$. For each $\sigma$ and $\tau$ we assume the following conditions.
$A^\sigma$ is a set
$\mathbf{App}^{\sigma,\tau}$ is a map $\mathbf{App}^{\sigma,\tau} : A^{(\sigma \to \tau)} \to A^\sigma \to A^\tau$,
$Const$ is a map from term constants of $\Sigma$ to elements of the union of all the $A^\sigma$’s such that if $c:\sigma$, then $Const(c) \in A^\sigma$.
It is hard to understand the concept just by reading this definition. The intuition behind this is that the term of type $\sigma$ will be interpreted as elements of $A^\sigma$. For any $\sigma$ and $\tau$, the application map $\mathbf{App}^{\sigma,\tau}$ lets us use each $a \in A^{\sigma \to \tau}$ as a function from $A^\sigma$ to $A^\tau$. Finally, the map $Const$ gives the meaning of each term constant.
$\mathbf{App}^{\sigma,\tau}$ is used to simulate the function application in lambda calculus. For instance, the expression \(\mathbf{App}^{\sigma,\tau} \: f \: d\) simulates the lambda term \(f \: d\), where $f:\sigma \to \tau$ and $d:\sigma$.
An important part of the definition of Henkin model is that equality between elements of function types must be standard equality of functions. An applicative structure is extensional if it satisfies the condition
- For all $f,g \in A^{\sigma \to \tau}$, if \(\mathbf{App} \: f \: d = \mathbf{App} \: g \: d\) for all $d \in A^\sigma$, then $f=g$.
Extensionality means that $f,g \in A^{\sigma \to \tau}$ are equal iff $\mathbf{App}$ $f$ and $\mathbf{App}$ $g$ are the same function from $A^\sigma$ to $A^\tau$.
Another way of saying this is that the function $\mathbf{App}$ must be one-to-one from $A^{\sigma \to \tau}$ into the functions from $A^\sigma$ to $A^\tau$.
Example 1
Let $\Sigma$ be any lambda signature and let $\mathcal{H}$ be any finite or infinite type assignment \(\mathcal{H} = \{ x_1:\sigma_1, \: x_2:\sigma_2,... \}\). An applicative structure
\[\mathcal{T} = \langle \{ A^\sigma\}, \{ \mathbf{App}^{\sigma,\tau}\} , Const \rangle\]may be defined by letting
\[T^\sigma = \{ M \mid \Gamma\:\triangleright\: M :\tau \text{ some finite } \Gamma \subseteq \mathcal{H}\}\]and defining \(\mathbf{App}^{\sigma,\tau}\: M \: N = M \: N\) for every $M \in T^{\sigma \to \tau}$ and $N \in T^\sigma$. For each term constant from $\Sigma$, we take $Const(c) =c$.
If $\mathcal{H}$ provides variables of each type, then $\mathcal{T}$ is extensional. In contrast, if $\mathcal{H}$ does not then some $T^\sigma$ may be empty. If $T^\sigma$ is empty, then any two elements of $T^{\sigma \to \tau}$ will be extensionally equal (vacuously), so extensionality will fail if $T^{\sigma \to \tau}$ has more than one element.
Example 2
We may construct a “recursive” applicative structure using any enumeration $\phi_0, \phi_1, \phi_2, …$ of the partial recursive functions on natural numbers. In this structure, each type $A^\sigma$ will be a subset of the natural numbers and application will be defined by \(\mathbf{App}^{\sigma,\tau}\: n \: m = \phi_n(m)\).
For each base type $b$, we may choose $A^b$ arbitrarily. However, since $\mathbf{App}$ must be a total function, we must select the elements of function types more carefully.
Recall that a partial function from a set $X$ to a set $Y$ is a function from a subset of (possibly the whole $X$ itself) to $Y$. If $S$ equals $X$, that is, if this function is defined on every element in $X$, then it is said to be a total function.
Specifically, for any function type $\sigma \to \tau$, we let $A^{\sigma \to \tau}$ be the set of all natural numbers that $n \in \mathbb{N}$ such that for all $m \in A^\sigma$, $\phi_n(m)$ is defined as an element of $A^\tau$.
If $A^b$ is the set of all natural numbers, then $A^{b \to b}$ will be the set of all $n$ such that $\phi_n$ is a total recursive function.
In this structure, although application is computable, it may not be decidable whether $n$ is an element of some $A^\sigma$. This application is not extensional, since there will generally be several natural numbers that all code (correspond to) the same recursive function.
Frames
In place of applicative structures, it is possible to use a definition of model that assumes extensionality.
Instead of letting $A^{\sigma \to \tau}$ be any set, and requiring an application map to make elements of $A^{\sigma \to \tau}$ behave like functions, we could require that $A^{\sigma \to \tau}$ actually be some set of functions from $A^{\sigma}$ to $A^{\tau}$.
To be precise, a type frame is an applicative structure \(\langle \{ A^\sigma\}, \{ \mathbf{App}^{\sigma,\tau}\} , Const \rangle\) such that
\[\begin{split} A^{\sigma \to \tau} {\subseteq A^\tau}^{(A^\sigma)}\\ \end{split}\]and \(\mathbf{App}^{\sigma,\tau}\: f \: d = f(d)\). In the formula above, exponentiation $A^B$ denotes the usual set-theoretic collection of all functions from $B$ to $A$.
Since $\mathbf{App}$ is always function application in any type frame, it is common to omit $\mathbf{App}$, writing \(\mathcal{A} = \langle \{ A^\sigma\}, Const \rangle\). If $\Sigma$ has no constants, then we may also drop $Const$, and think of a type frame \(\mathcal{A} = \{ A^\sigma\}\) as simply an indexed family of sets.
Environment Model Condition
One characterization of Henkin model uses the envrionment model condition, which relies on some notions of environment.
As in algebra, an environment $\eta$ for applicative structure $\mathcal{A}$ is a mapping from variables to the union of all $A^\sigma$. If $\Gamma$ is a type assignment, then we say $\eta$ satisfies $\Gamma$, written $\eta \vDash \Gamma$, if $\eta(x) \in A^{\sigma}$ for every $x:\sigma \in \Gamma$. If $\eta$ is any environment for $\mathcal{A}$, and $d \in A^{\sigma}$, then $\eta[x \mapsto d]$ is the environment mapping $x$ to $d$, and $y$ to $\eta(y)$ for $y$ different from $x$.
Recall that if \(\Gamma \:\triangleright\: M:\sigma\) is well-typed, then there is a proof of this using the typing rules. Analogously, we define the meaning \(\mathcal{A} [\![ M ]\!] \eta\) of a well-typed term \(\Gamma \:\triangleright\: M:\sigma\) in environment $\eta \vDash \Gamma$ by following five inductive clauses, corresponding to typing axioms ($var$), ($cst$), and typing rules ($add$ $var$), ($\to$ $\text{Elim}$) and ($\to$ $\text{Intro}$).
\[\begin{align} &\mathcal{A} [\![ \emptyset \:\triangleright\: c:\sigma ]\!] \eta &&= Const(c) \\ &\mathcal{A} [\![ x:\sigma \:\triangleright\: x:\sigma ]\!] \eta &&= \eta(x) \\ &\mathcal{A} [\![ \Gamma,\:x:\sigma \:\triangleright\: M:\tau ]\!] \eta &&= \mathcal{A} [\![ \Gamma \:\triangleright\: M:\tau ]\!] \eta \\ &\mathcal{A} [\![ \Gamma\:\triangleright\: M \: N :\tau ]\!] \eta &&= \mathbf{App}^{\sigma,\tau} \: \mathcal{A} [\![ \Gamma \:\triangleright\: M:\sigma \to \tau ]\!] \eta \: \mathcal{A} [\![ \Gamma \:\triangleright\: N:\sigma ]\!] \eta\\ &\mathcal{A} [\![ \Gamma\:\triangleright\: \lambda x:\sigma .M :\sigma \to \tau ]\!] \eta &&= \text{ the unique } f \ in A^{\sigma \to \tau} \text{ such that } \\ & && \forall d \in A^\sigma \: . \: \mathbf{App}^{\sigma,\tau} \: f \: d = \mathcal{A} [\![ \Gamma ,\:x:\sigma\:\triangleright\: M:\tau ]\!] \eta[x \mapsto d]\\ \end{align}\]These inductive clauses allow us to determine some basic information (such as the type, the free variables of a term and the typing rules) used to eastablish that the term is well-typed.
The main reason for using induction on typing derivation ($\triangleright$) is that in defining the meaning of a lambda abstraction \(\Gamma\:\triangleright\: \lambda x:\sigma .M :\sigma \to \tau\), we need to refer to the meaning of $M$ in typing context $\Gamma,x:\sigma$. If we know that \(\Gamma\:\triangleright\: \lambda x:\sigma .M :\sigma \to \tau\) is typed according to rule ($\to$ $\text{Intro}$), then we are guaranteed that $\Gamma,x:\sigma$ is well-typed, since this must have occurred in the hypothesis of the rule. If we used induction on the structure of terms, then we would have difficulty with a term such as \(x:\sigma \:\triangleright\: \lambda x:\tau .x\), where lambda-bound variable appears in the type assignment.
When the model $\mathcal{A}$ is either irrelevant or clear from context, it is common to write \([\![\Gamma \:\triangleright\: M:\sigma]\!]\eta\) for \(\mathcal{A}[\![\Gamma \:\triangleright\: M:\sigma]\!]\eta\). Similarly, the environment may be ommited if the term is closed.
Example 3
We may define a Henkin model $\mathcal{A}$ for the signature with single base type $nat$ by letting $A^{nat}$ be the usual set of natural numbers and $A^{\sigma \to \tau}$ the set of of all functions from $A^{\sigma}$ to $A^{\tau}$, for all $\sigma$ and $\tau$. This is called the full set-theoretic function hierachy over the natural numbers.
We apply a function $f \in A^{\sigma \to \tau}$ to argument $x \in A^{\sigma}$ as usual by \(\mathbf{App} f \: d = f(d)\). We will work out the meaning of the term \(\lambda x:nat \to nat.\: \lambda y:nat.\:x\:y\). Since this term is closed, it does not matter which environment we choose.
Using the inductive definition of meaning, we can make the following calculation. For typographic simplicity, we omit the types of terms.
\[\begin{split} &[\![\emptyset \:\triangleright\: \lambda x:nat \to nat.\: \lambda y:nat.\:x\:y]\!]\eta \\\\ &=\biggl( \begin{split}\text{the unique } &f \in A^{(nat \to nat) \to nat \to nat} \text{ such that}\\ \forall h \in A^{nat \to nat} \:.\: \mathbf{App}\: f \: &h = [\![x:(nat \to nat) \:\triangleright\: \lambda y:nat \:.\:x\:y]\!]\eta[x\mapsto h] \end{split} \biggr) \end{split}\]The meaning of the lambda term with one less $\lambda$ is defined similarly, and simplified as follows.
\[\begin{split} &[\![x:nat \to nat \:\triangleright\: \lambda y:nat.\:x\:y]\!]\eta [x \mapsto h]\\\\ &=\biggl( \begin{split}\text{the unique } &g \in A^{ nat \to nat} \text{ such that}\\ \forall n \in A^{nat} \:.\: \mathbf{App}\: g \: n = [\![x:n&at \to nat ,\:\lambda y:nat \:\triangleright\:x\:y]\!]\eta[x\mapsto h][y\mapsto n] \end{split} \biggr)\\\\ &=\biggl( \begin{split}\text{the unique } &g \in A^{ nat \to nat} \text{ such that}\\ \forall n \in A^{nat} &\:.\: \mathbf{App}\: g \: n = \mathbf{App}\: h \: n \end{split} \biggr)\\\\ &= h \end{split}\]This allows us to complete our calculation of the meaning of original term.
\[\begin{split} &[\![\emptyset \:\triangleright\: \lambda x:nat \to nat.\: \lambda y:nat.\:x\:y]\!]\eta \\\\ &=\biggl( \begin{split}\text{the unique } &f \in A^{(nat \to nat) \to nat \to nat} \text{ such that}\\ \forall h \in &A^{nat \to nat} \:.\: \mathbf{App}\: f \: h = h \end{split} \biggr) \end{split}\]Thus the meaning of this term is the unique element of $A^{(nat \to nat) \to nat \to nat}$ representing the identity function. We can check this calculation by seeing that, by ($\eta$),
\[x:nat \to nat \:\triangleright\: \lambda y:nat .\:x\: y \: = \: x:nat\]and therefore we can prove the equation
\[\emptyset \:\triangleright\: \lambda x:nat \to nat ,\: \lambda y:nat .\:x\: y \: = \: \lambda x:nat \to nat.\:x.\]Soundness
In typed lambda calculus, there are two proof systems, one for proving typing assertions ($\triangleright$) and one for equations ($\vdash$). As a result, there are two forms of soundness for $\lambda^\to$ and other typed lambda calculi: type soundness and equational soundness
Type Soundness
The type soundness is stated in the following theorem.
(Theorem 1. Type Soundness) Let $\mathcal{A}$ be any Henkin model for signature $\Sigma$, \(\Gamma \:\triangleright\:M:\sigma\) a provable typing assertions, and $\eta \vDash \Gamma$ an environment for $\mathcal{A}$. Then
\[[\![\Gamma \:\triangleright\: M:\sigma]\!]\eta \in A^\sigma.\]This has the usual form for a soundness property: if a typing assertion is provable, then it holds semantically.
The proof is a straightforward induction on typing derivations, so it is omitted.
With a little thought, we may interpret this theorem as saying that well-typed $\lambda^\to$ terms do not contain type errors. In a general framework for analyzing type errors, we would expect to identify certain function applications as erroneous. For example, inthe signature for PCF, we would say that an application of $+$ to two arguments would produce a type error if either of the arguments is not a natural number.
Some Lemmas
Before proving equational soundness, we state some important facts about variables and the meanings of terms.
A simple, preliminary fact is that the meaning of \(\Gamma \:\triangleright\: M:\sigma\) in environment $\eta$ can only depend on $\eta(y)$ if $y$ is free in $M$.
(Lemma 1. Free Variables) Suppose $\eta_1, \eta_2 \vDash \Gamma$ are environments for $\mathcal{A}$ such that $\eta_1(x) = \eta_2(x)$ for every $x \in FV(M)$. Then \([\![\Gamma \:\triangleright\: M:\sigma]\!]\eta_1 = [\![\Gamma \:\triangleright\: M:\sigma]\!]\eta_2\).
The proof is a straightforward inductive arguments, following the proof pattern of Lemma 4 in Easy Foundations for Programming Languages VII — Simply-Typed Lambda Calculus.
Considering that substitution involves renaming of bound variables, we will prove that the names of bound variables does not effect the meaning of a term. To make the inductive proof go through, we need a stronger inductive hypothesis that includes renaming free variables and setting the environment appropriately.
(Lemma 2.) Let \(\Gamma = \{ x_1:\sigma_1,...x_k:\sigma_k \}\) and suppose \(\Gamma \:\triangleright\: M:\sigma\) is a well typed term. Let \(\Gamma' = \{ y_1:\sigma_1,...y_k:\sigma_k \}\) and let $N$ be any term that is $\alpha$-equivalent to $[y_1,…,y_k/x_1,…,x_k]M$. If $\eta’(y_i) = \eta(x_i)$, for $1 \leq i \leq k$, then
\[[\![\Gamma \:\triangleright\: M:\sigma]\!]\eta = [\![\Gamma' \:\triangleright\: N:\sigma]\!]\eta'.\](Proof.) The proof is by induction on the typing derivation of $M$. The only nontrivial case is lambda abstraction (by ($\to$ $\text{Intro}$)). Suppose that \(\Gamma \:\triangleright\: \lambda z:\rho.\:M:\rho \to \tau\) is typed using \(\Gamma,\:z:\rho \:\triangleright\: M:\tau\). The meaning of the lambda term is
\[\begin{split} &[\![\Gamma \:\triangleright\: \lambda z:\rho.\:M:\rho \to \tau]\!]\eta \\\\ &=\biggl( \begin{split}\text{the unique } &f \in A^{\rho \to \tau} \text{ such that}\\ \forall a \in A^{\rho} \:.\: \mathbf{App}\: f \: a &= [\![\Gamma,\:z:\rho \:\triangleright\: M:\tau]\!]\eta[z \mapsto a] \end{split} \biggr) \end{split}\]We must show that this is the same as the meaning of any term obtained by renaming free and bound variabls, in an appropriate environment, such as
\[\begin{split} &[\![\Gamma' \:\triangleright\: \lambda w:\rho.\:M:\rho \to \tau]\!]\eta' \\\\ &=\biggl( \begin{split}\text{the unique } &f \in A^{\rho \to \tau} \text{ such that}\\ \forall a \in A^{\rho} \:.\: \mathbf{App}\: f \: a &= [\![\Gamma',\:w:\rho \:\triangleright\: M:\tau]\!]\eta[w \mapsto a] \end{split} \biggr) \end{split}\]However, by the inductive hypothesis, we know that for any $a \in A^\rho$,
\[[\![\Gamma,\:z:\rho \:\triangleright\: M:\tau]\!]\eta[z \mapsto a] = [\![\Gamma',\:w:\rho \:\triangleright\: N:\tau]\!]\eta'[w \mapsto a].\]This proves the lemma. $\blacksquare$
This brings us to the substitution lemma for $\lambda^\to$.
(Lemma 3. Substitution) Let \(\Gamma,\:x:\sigma \:\triangleright\: M:\tau\) and \(\Gamma\:\triangleright\: N:\sigma\) be terms. Let $\eta \vDash \Gamma$ and \(d = [\![\Gamma\:\triangleright\: N:\sigma]\!]\eta\). Then
\[[\![\Gamma\:\triangleright\: [N/x]M:\tau]\!]\eta = [\![\Gamma,\:x:\sigma \:\triangleright\: M:\tau]\!]\eta[x \mapsto d].\]Like the substitution lemma for algebra (Easy Foundations for Programming Languages IX — Universal Algebra and Algebraic Data Types), this lemma says that the effect of syntactically substituting an expressions $N$ for $x$ is the same as letting $x$ denote the semantic meaning of $N$. The proof is omitted.
Equational Soundness
We say a Henkin model $\mathcal{A}$ and environment $\eta \vDash \Gamma$ satisfy an equation \(\Gamma\:\triangleright\: M=N:\sigma\), written
\[\mathcal{A},\eta \vDash \Gamma\:\triangleright\: M =N:\tau,\]if
\[\mathcal{A}[\![\vDash \Gamma\:\triangleright\: M:\tau]\!]\eta = \mathcal{A}[\![\vDash \Gamma\:\triangleright\: N:\tau]\!]\eta.\]And we say a model $\mathcal{A}$ satisfies an equation \(\Gamma\:\triangleright\: M=N:\sigma\) if $\mathcal{A}$ and environment $\eta$ satisfy this equation, for every $\eta$ satisfying $\Gamma$. Then we can introduce the following theorem.
(Theorem 2. Equational Soundness) If \(\mathcal{E} \vdash \Gamma\:\triangleright\: M =N:\tau\) for any set $\mathcal{E}$ of typed equations, then every Henkin model satisfying $\mathcal{E}$ also satisfies \(\Gamma\:\triangleright\: M =N:\tau\).
(Proof.) The proof is by induction on equational proofs from the set $\mathcal{E}$ of equational hypotheses. The base cases are that $E \in \mathcal{E}$ or $E$ is one of the axioms ($ref$), ($\alpha$), ($\beta$), or ($\eta$). The cases for $E \in \mathcal{E}$ and ($ref$) are trivial. The ($\alpha$) case follows from Lemma 2.
For ($\beta$), we use the substitution lemma (lemma 3), as follows. The meaning of an application is
\[[\![\Gamma\:\triangleright\:(\lambda x:nat .\: M) \: N:\tau]\!]\eta = \mathbf{App}\: f \: a\]where $a$ is the meaning of $N$ and $f$ is the unique element of $A^{\sigma \to \tau}$ satisfying
\[\mathbf{App}\: f \: a' = [\![\Gamma,\: x:\sigma \:\triangleright\:M:\tau]\!]\eta[x \mapsto a']\]for all $a’ \in A^\sigma$.
We must show that the meaning of the application is the same as the meaning of the substitution instance
\[[\![\Gamma \:\triangleright\:[N/x]M:\tau]\!]\eta.\]However, by the substituion lemma we have
\[\mathbf{App}\: f \: a' = [\![\Gamma,\: x:\sigma \:\triangleright\:M:\tau]\!]\eta[x \mapsto a'] = [\![\Gamma \:\triangleright\:[N/x]M:\tau]\!]\eta\]which proves this case of the theorem.
The ($\eta$) case is a routine calculation, similar to Example 3.
There are inductive steps for inference rules ($sym$), ($trans$), ($\xi$) and ($\nu$). The ($sym$) and ($trans$) cases are trivial. The most interesting case is ($\xi$), which is still essentially straightforward. For this rule, we assume that
\[\mathcal{A} \vDash \Gamma,\:x:\sigma\:\triangleright\:M=N:\tau .\]We must show
\[\mathcal{A} \vDash \Gamma\:\triangleright\: \lambda x:\sigma.\:M=\lambda x:\sigma.\:N:\sigma \to \tau .\]This may be calculated as follows, using the induction hypothesis in the second step.
\[\begin{split} &[\![\Gamma \:\triangleright\: \lambda x:\sigma.\:M:\sigma \to \tau]\!]\eta \\\\ &=\biggl( \begin{split}\text{the unique } &f \in A^{\sigma \to \tau} \text{ such that}\\ \forall a \in A^{\sigma} \:.\: \mathbf{App}\: f \: a &= [\![\Gamma,\:x:\sigma \:\triangleright\: M:\tau]\!]\eta[x \mapsto a] \end{split} \biggr)\\\\ &=\biggl( \begin{split}\text{the unique } &f \in A^{\sigma \to \tau} \text{ such that}\\ \forall a \in A^{\sigma} \:.\: \mathbf{App}\: f \: a &= [\![\Gamma,\:x:\sigma \:\triangleright\: N:\tau]\!]\eta[x \mapsto a] \end{split} \biggr)\\\\ &= [\![\Gamma \:\triangleright\: \lambda x:\sigma.\:N:\sigma \to \tau]\!]\eta \end{split}\]The ($\nu$) case is straightforward and omitted. This finishes the proof. $\blacksquare$