[proofplan] We construct the categorical interpretation by structural induction on typing derivations, using the chosen left-associated products for contexts. Variables and substitutions are handled by explicitly defined product projections and product pairings, while lambda abstraction and application are interpreted through the exponential transpose and evaluation map. The main technical point is the substitution lemma, proved simultaneously with the interpretation by induction on terms. Finally, the $\beta$- and $\eta$-equations are sound because they are exactly the uniqueness laws for products, the uniqueness of maps into the terminal object, and the triangular identities for the exponential adjunction. [/proofplan] [step:Define context projections and substitution morphisms for left-associated products] Write $T$ for the chosen terminal object of $\baseC$. For every object $X$ of $\baseC$, let \begin{align*} !_X:X\to T \end{align*} denote the unique morphism to $T$. For a context $\Gamma=(x_1:A_1,\dots,x_n:A_n)$, define the object $\llbracket\Gamma\rrbracket$ as in the statement. For each variable declaration $x_i:A_i$ in $\Gamma$, define the variable projection \begin{align*} p_{\Gamma,x_i}:\llbracket\Gamma\rrbracket\to\llbracket A_i\rrbracket \end{align*} recursively as follows. If $\Gamma=\Gamma',x:A$, then \begin{align*} p_{\Gamma,x}=\pi_2^{\llbracket\Gamma'\rrbracket,\llbracket A\rrbracket}. \end{align*} If $y:B$ is a variable in $\Gamma'$, then \begin{align*} p_{\Gamma,y}=p_{\Gamma',y}\circ \pi_1^{\llbracket\Gamma'\rrbracket,\llbracket A\rrbracket}. \end{align*} Thus each variable is interpreted by the projection from the fixed left-associated product which extracts its coordinate. A syntactic substitution $\sigma:\Delta\Rightarrow\Gamma$, where $\Gamma=(x_1:A_1,\dots,x_n:A_n)$, is a tuple of terms \begin{align*} \sigma=(s_1,\dots,s_n) \end{align*} with $\Delta\vdash s_i:A_i$ for each $i$. Its interpretation is the morphism \begin{align*} \llbracket\sigma\rrbracket:\llbracket\Delta\rrbracket\to\llbracket\Gamma\rrbracket \end{align*} defined recursively by product pairing. For the empty target context $\varnothing$, set \begin{align*} \llbracket\sigma\rrbracket=!_{\llbracket\Delta\rrbracket}:\llbracket\Delta\rrbracket\to T. \end{align*} If $\Gamma=\Gamma',x:A$ and $\sigma=(\sigma',s)$, where $\sigma':\Delta\Rightarrow\Gamma'$ and $\Delta\vdash s:A$, set \begin{align*} \llbracket\sigma\rrbracket=\langle \llbracket\sigma'\rrbracket,\llbracket s\rrbracket_\Delta\rangle:\llbracket\Delta\rrbracket\to\llbracket\Gamma'\rrbracket\times\llbracket A\rrbracket. \end{align*} The product pairing is the unique morphism with first projection $\llbracket\sigma'\rrbracket$ and second projection $\llbracket s\rrbracket_\Delta$. For morphisms $g:Z\to X$ and $h:Z\to Y$, the notation $\langle g,h\rangle:Z\to X\times Y$ always denotes this chosen product pairing. When a product of morphisms is needed, we define it by pairing after projections: for $u:X\to X'$ and $v:Y\to Y'$, set \begin{align*} u\times v=\langle u\circ\pi_1^{X,Y},v\circ\pi_2^{X,Y}\rangle:X\times Y\to X'\times Y'. \end{align*} [/step] [step:Interpret every typing derivation as a morphism] We define $\llbracket t\rrbracket_\Gamma:\llbracket\Gamma\rrbracket\to\llbracket A\rrbracket$ by induction on the derivation of $\Gamma\vdash t:A$. For the variable rule, if $t=x$ and $x:A$ occurs in $\Gamma$, set \begin{align*} \llbracket x\rrbracket_\Gamma=p_{\Gamma,x}. \end{align*} For the unit introduction rule, if $\Gamma\vdash \star:1$, set \begin{align*} \llbracket\star\rrbracket_\Gamma=!_{\llbracket\Gamma\rrbracket}:\llbracket\Gamma\rrbracket\to T. \end{align*} For pairing, if $\Gamma\vdash r:A$ and $\Gamma\vdash s:B$, define \begin{align*} \llbracket \langle r,s\rangle\rrbracket_\Gamma=\langle \llbracket r\rrbracket_\Gamma,\llbracket s\rrbracket_\Gamma\rangle:\llbracket\Gamma\rrbracket\to\llbracket A\rrbracket\times\llbracket B\rrbracket. \end{align*} For projections, if $\Gamma\vdash u:A\times B$, define \begin{align*} \llbracket \pi_1 u\rrbracket_\Gamma=\pi_1^{\llbracket A\rrbracket,\llbracket B\rrbracket}\circ \llbracket u\rrbracket_\Gamma \end{align*} and \begin{align*} \llbracket \pi_2 u\rrbracket_\Gamma=\pi_2^{\llbracket A\rrbracket,\llbracket B\rrbracket}\circ \llbracket u\rrbracket_\Gamma. \end{align*} For abstraction, suppose $\Gamma,x:A\vdash r:B$. Since \begin{align*} \llbracket\Gamma,x:A\rrbracket=\llbracket\Gamma\rrbracket\times\llbracket A\rrbracket, \end{align*} the induction hypothesis gives \begin{align*} \llbracket r\rrbracket_{\Gamma,x:A}:\llbracket\Gamma\rrbracket\times\llbracket A\rrbracket\to\llbracket B\rrbracket. \end{align*} Let \begin{align*} \Lambda_{\llbracket\Gamma\rrbracket,\llbracket A\rrbracket,\llbracket B\rrbracket} \end{align*} denote the exponential transpose bijection \begin{align*} \operatorname{Hom}_{\baseC}(\llbracket\Gamma\rrbracket\times\llbracket A\rrbracket,\llbracket B\rrbracket)\cong \operatorname{Hom}_{\baseC}(\llbracket\Gamma\rrbracket,\llbracket B\rrbracket^{\llbracket A\rrbracket}). \end{align*} Define \begin{align*} \llbracket \lambda x:A.\,r\rrbracket_\Gamma=\Lambda_{\llbracket\Gamma\rrbracket,\llbracket A\rrbracket,\llbracket B\rrbracket}(\llbracket r\rrbracket_{\Gamma,x:A}). \end{align*} For application, if $\Gamma\vdash f:A\to B$ and $\Gamma\vdash a:A$, define \begin{align*} \llbracket f\,a\rrbracket_\Gamma=\operatorname{ev}_{\llbracket A\rrbracket,\llbracket B\rrbracket}\circ \langle \llbracket f\rrbracket_\Gamma,\llbracket a\rrbracket_\Gamma\rangle. \end{align*} Weakening is included by composition with the projection from the enlarged context. If $\Gamma\vdash r:A$ and $\Gamma,y:B$ is the weakened context, then \begin{align*} \llbracket r\rrbracket_{\Gamma,y:B}=\llbracket r\rrbracket_\Gamma\circ \pi_1^{\llbracket\Gamma\rrbracket,\llbracket B\rrbracket}. \end{align*} Each clause produces a morphism with the required domain and codomain, so the interpretation exists for every derivable typing judgment. [/step] [step:Prove substitution soundness by induction on terms] We prove that for every derivation $\Gamma\vdash t:A$ and every substitution $\sigma:\Delta\Rightarrow\Gamma$, \begin{align*} \llbracket t[\sigma]\rrbracket_\Delta=\llbracket t\rrbracket_\Gamma\circ\llbracket\sigma\rrbracket. \end{align*} The proof is by induction on the construction of $t$. For a variable $x_i:A_i$ in $\Gamma=(x_1:A_1,\dots,x_n:A_n)$, the substituted term is $s_i$. By the recursive definition of $\llbracket\sigma\rrbracket$ and the uniqueness part of the product universal property, \begin{align*} p_{\Gamma,x_i}\circ\llbracket\sigma\rrbracket=\llbracket s_i\rrbracket_\Delta. \end{align*} Hence \begin{align*} \llbracket x_i[\sigma]\rrbracket_\Delta=\llbracket x_i\rrbracket_\Gamma\circ\llbracket\sigma\rrbracket. \end{align*} For the unit term, both sides are morphisms $\llbracket\Delta\rrbracket\to T$, so they are equal by terminal uniqueness. For pairs, suppose $t=\langle r,s\rangle$. The induction hypotheses give \begin{align*} \llbracket r[\sigma]\rrbracket_\Delta=\llbracket r\rrbracket_\Gamma\circ\llbracket\sigma\rrbracket \end{align*} and \begin{align*} \llbracket s[\sigma]\rrbracket_\Delta=\llbracket s\rrbracket_\Gamma\circ\llbracket\sigma\rrbracket. \end{align*} By the defining uniqueness of product pairing, \begin{align*} \llbracket \langle r,s\rangle[\sigma]\rrbracket_\Delta=\langle \llbracket r\rrbracket_\Gamma,\llbracket s\rrbracket_\Gamma\rangle\circ\llbracket\sigma\rrbracket. \end{align*} This is exactly $\llbracket\langle r,s\rangle\rrbracket_\Gamma\circ\llbracket\sigma\rrbracket$. For projections, the result follows by composing the induction hypothesis for the projected term with the corresponding product projection. For application, suppose $t=f\,a$. The induction hypotheses give the substitution identities for $f$ and $a$. Therefore \begin{align*} \llbracket (f\,a)[\sigma]\rrbracket_\Delta=\operatorname{ev}_{\llbracket A\rrbracket,\llbracket B\rrbracket}\circ\langle \llbracket f\rrbracket_\Gamma\circ\llbracket\sigma\rrbracket,\llbracket a\rrbracket_\Gamma\circ\llbracket\sigma\rrbracket\rangle. \end{align*} By the product universal property, \begin{align*} \langle \llbracket f\rrbracket_\Gamma\circ\llbracket\sigma\rrbracket,\llbracket a\rrbracket_\Gamma\circ\llbracket\sigma\rrbracket\rangle=\langle \llbracket f\rrbracket_\Gamma,\llbracket a\rrbracket_\Gamma\rangle\circ\llbracket\sigma\rrbracket. \end{align*} Thus \begin{align*} \llbracket (f\,a)[\sigma]\rrbracket_\Delta=\llbracket f\,a\rrbracket_\Gamma\circ\llbracket\sigma\rrbracket. \end{align*} For abstraction, suppose $t=\lambda x:A.\,r$ with $\Gamma,x:A\vdash r:B$. Let $\sigma^+:\Delta,x:A\Rightarrow\Gamma,x:A$ be the extended substitution whose first components are $\sigma$ weakened to $\Delta,x:A$ and whose last component is the variable $x$. Its interpretation is \begin{align*} \llbracket\sigma^+\rrbracket=\langle \llbracket\sigma\rrbracket\circ\pi_1^{\llbracket\Delta\rrbracket,\llbracket A\rrbracket},\pi_2^{\llbracket\Delta\rrbracket,\llbracket A\rrbracket}\rangle:\llbracket\Delta\rrbracket\times\llbracket A\rrbracket\to\llbracket\Gamma\rrbracket\times\llbracket A\rrbracket. \end{align*} By the induction hypothesis applied to $r$ and $\sigma^+$, \begin{align*} \llbracket r[\sigma^+]\rrbracket_{\Delta,x:A}=\llbracket r\rrbracket_{\Gamma,x:A}\circ\llbracket\sigma^+\rrbracket. \end{align*} The substituted abstraction is $\lambda x:A.\,r[\sigma^+]$, after alpha-renaming if necessary to keep $x$ fresh. Taking exponential transposes, and using the naturality of exponential transposition in the parameter object, gives \begin{align*} \llbracket (\lambda x:A.\,r)[\sigma]\rrbracket_\Delta=\llbracket \lambda x:A.\,r\rrbracket_\Gamma\circ\llbracket\sigma\rrbracket. \end{align*} This proves the substitution lemma. [guided] We prove substitution soundness by following the syntax of the term. The target identity is \begin{align*} \llbracket t[\sigma]\rrbracket_\Delta=\llbracket t\rrbracket_\Gamma\circ\llbracket\sigma\rrbracket, \end{align*} where $\Gamma\vdash t:A$ and $\sigma:\Delta\Rightarrow\Gamma$ is a tuple of terms in context $\Delta$. This identity says that substituting first and then interpreting gives the same morphism as interpreting first and then precomposing by the morphism determined by the tuple of substituted terms. For a variable $x_i:A_i$ in $\Gamma=(x_1:A_1,\dots,x_n:A_n)$, the substitution $\sigma=(s_1,\dots,s_n)$ sends $x_i$ to $s_i$. The interpretation of $\sigma$ was defined precisely so that its $x_i$-coordinate is $\llbracket s_i\rrbracket_\Delta$. In categorical terms, this means \begin{align*} p_{\Gamma,x_i}\circ\llbracket\sigma\rrbracket=\llbracket s_i\rrbracket_\Delta. \end{align*} Since $\llbracket x_i\rrbracket_\Gamma=p_{\Gamma,x_i}$ and $x_i[\sigma]=s_i$, we obtain \begin{align*} \llbracket x_i[\sigma]\rrbracket_\Delta=\llbracket x_i\rrbracket_\Gamma\circ\llbracket\sigma\rrbracket. \end{align*} This is the reason for defining substitutions by recursive product pairing: the projections recover exactly the substituted components. For the unit term $\star:1$, both $\llbracket \star[\sigma]\rrbracket_\Delta$ and $\llbracket\star\rrbracket_\Gamma\circ\llbracket\sigma\rrbracket$ are morphisms from $\llbracket\Delta\rrbracket$ to the terminal object $T$. The defining property of $T$ gives a unique such morphism, so the two morphisms are equal. For a pair $t=\langle r,s\rangle$, the induction hypotheses state \begin{align*} \llbracket r[\sigma]\rrbracket_\Delta=\llbracket r\rrbracket_\Gamma\circ\llbracket\sigma\rrbracket \end{align*} and \begin{align*} \llbracket s[\sigma]\rrbracket_\Delta=\llbracket s\rrbracket_\Gamma\circ\llbracket\sigma\rrbracket. \end{align*} The interpretation of the substituted pair is the pairing of these two morphisms: \begin{align*} \llbracket \langle r,s\rangle[\sigma]\rrbracket_\Delta=\langle \llbracket r[\sigma]\rrbracket_\Delta,\llbracket s[\sigma]\rrbracket_\Delta\rangle. \end{align*} Substituting the two induction identities gives \begin{align*} \llbracket \langle r,s\rangle[\sigma]\rrbracket_\Delta=\langle \llbracket r\rrbracket_\Gamma\circ\llbracket\sigma\rrbracket,\llbracket s\rrbracket_\Gamma\circ\llbracket\sigma\rrbracket\rangle. \end{align*} The product universal property identifies this last pairing with \begin{align*} \langle \llbracket r\rrbracket_\Gamma,\llbracket s\rrbracket_\Gamma\rangle\circ\llbracket\sigma\rrbracket. \end{align*} Therefore \begin{align*} \llbracket \langle r,s\rangle[\sigma]\rrbracket_\Delta=\llbracket\langle r,s\rangle\rrbracket_\Gamma\circ\llbracket\sigma\rrbracket. \end{align*} For projections, consider $\pi_1 u$; the second projection is identical with $\pi_2$ in place of $\pi_1$. The induction hypothesis gives \begin{align*} \llbracket u[\sigma]\rrbracket_\Delta=\llbracket u\rrbracket_\Gamma\circ\llbracket\sigma\rrbracket. \end{align*} Composing both sides with the product projection $\pi_1^{\llbracket A\rrbracket,\llbracket B\rrbracket}$ gives \begin{align*} \llbracket (\pi_1 u)[\sigma]\rrbracket_\Delta=\pi_1^{\llbracket A\rrbracket,\llbracket B\rrbracket}\circ\llbracket u\rrbracket_\Gamma\circ\llbracket\sigma\rrbracket. \end{align*} The right-hand side is $\llbracket\pi_1 u\rrbracket_\Gamma\circ\llbracket\sigma\rrbracket$, so substitution commutes with projections. For application $t=f\,a$, the induction hypotheses give \begin{align*} \llbracket f[\sigma]\rrbracket_\Delta=\llbracket f\rrbracket_\Gamma\circ\llbracket\sigma\rrbracket \end{align*} and \begin{align*} \llbracket a[\sigma]\rrbracket_\Delta=\llbracket a\rrbracket_\Gamma\circ\llbracket\sigma\rrbracket. \end{align*} The interpretation of application is evaluation after pairing the interpreted function and argument: \begin{align*} \llbracket (f\,a)[\sigma]\rrbracket_\Delta=\operatorname{ev}_{\llbracket A\rrbracket,\llbracket B\rrbracket}\circ\langle \llbracket f\rrbracket_\Gamma\circ\llbracket\sigma\rrbracket,\llbracket a\rrbracket_\Gamma\circ\llbracket\sigma\rrbracket\rangle. \end{align*} The product universal property says that pairing commutes with precomposition: \begin{align*} \langle \llbracket f\rrbracket_\Gamma\circ\llbracket\sigma\rrbracket,\llbracket a\rrbracket_\Gamma\circ\llbracket\sigma\rrbracket\rangle=\langle \llbracket f\rrbracket_\Gamma,\llbracket a\rrbracket_\Gamma\rangle\circ\llbracket\sigma\rrbracket. \end{align*} Thus \begin{align*} \llbracket (f\,a)[\sigma]\rrbracket_\Delta=\llbracket f\,a\rrbracket_\Gamma\circ\llbracket\sigma\rrbracket. \end{align*} The abstraction case is the only place where variable binding matters. Suppose $t=\lambda x:A.\,r$ and $\Gamma,x:A\vdash r:B$. We alpha-rename bound variables if needed so that $x$ is fresh for $\Delta$ and for the terms in $\sigma$. Define the extended substitution \begin{align*} \sigma^+:\Delta,x:A\Rightarrow\Gamma,x:A \end{align*} by applying $\sigma$ to the old variables of $\Gamma$ and leaving the new variable $x$ as itself. Categorically this is the morphism \begin{align*} \llbracket\sigma^+\rrbracket=\langle \llbracket\sigma\rrbracket\circ\pi_1^{\llbracket\Delta\rrbracket,\llbracket A\rrbracket},\pi_2^{\llbracket\Delta\rrbracket,\llbracket A\rrbracket}\rangle. \end{align*} The induction hypothesis applied to the body $r$ gives \begin{align*} \llbracket r[\sigma^+]\rrbracket_{\Delta,x:A}=\llbracket r\rrbracket_{\Gamma,x:A}\circ\llbracket\sigma^+\rrbracket. \end{align*} Now interpret the substituted abstraction by transposition: \begin{align*} \llbracket (\lambda x:A.\,r)[\sigma]\rrbracket_\Delta=\Lambda(\llbracket r[\sigma^+]\rrbracket_{\Delta,x:A}). \end{align*} The exponential transpose is natural in the parameter object: precomposing the curried map by $\llbracket\sigma\rrbracket$ corresponds exactly to precomposing the uncurried map by $\llbracket\sigma\rrbracket\times \operatorname{id}_{\llbracket A\rrbracket}$, which is the morphism $\llbracket\sigma^+\rrbracket$ under our chosen left-associated context product. Therefore \begin{align*} \Lambda(\llbracket r\rrbracket_{\Gamma,x:A}\circ\llbracket\sigma^+\rrbracket)=\Lambda(\llbracket r\rrbracket_{\Gamma,x:A})\circ\llbracket\sigma\rrbracket. \end{align*} Since $\Lambda(\llbracket r\rrbracket_{\Gamma,x:A})=\llbracket\lambda x:A.\,r\rrbracket_\Gamma$, this gives \begin{align*} \llbracket (\lambda x:A.\,r)[\sigma]\rrbracket_\Delta=\llbracket\lambda x:A.\,r\rrbracket_\Gamma\circ\llbracket\sigma\rrbracket. \end{align*} This completes the induction and proves substitution soundness for every term former. [/guided] [/step] [step:Verify the product and unit beta eta equations] For product beta, let $\Gamma\vdash r:A$ and $\Gamma\vdash s:B$. By the definition of pairing and the product projection law, \begin{align*} \llbracket \pi_1\langle r,s\rangle\rrbracket_\Gamma=\pi_1^{\llbracket A\rrbracket,\llbracket B\rrbracket}\circ\langle \llbracket r\rrbracket_\Gamma,\llbracket s\rrbracket_\Gamma\rangle=\llbracket r\rrbracket_\Gamma. \end{align*} Similarly, \begin{align*} \llbracket \pi_2\langle r,s\rangle\rrbracket_\Gamma=\llbracket s\rrbracket_\Gamma. \end{align*} For product eta, let $\Gamma\vdash u:A\times B$. The interpretation of $\langle \pi_1 u,\pi_2 u\rangle$ is the unique morphism to $\llbracket A\rrbracket\times\llbracket B\rrbracket$ whose first projection is $\pi_1^{\llbracket A\rrbracket,\llbracket B\rrbracket}\circ\llbracket u\rrbracket_\Gamma$ and whose second projection is $\pi_2^{\llbracket A\rrbracket,\llbracket B\rrbracket}\circ\llbracket u\rrbracket_\Gamma$. The morphism $\llbracket u\rrbracket_\Gamma$ has the same two projections. By uniqueness in the product universal property, \begin{align*} \llbracket \langle \pi_1u,\pi_2u\rangle\rrbracket_\Gamma=\llbracket u\rrbracket_\Gamma. \end{align*} For the unit eta equation, if $\Gamma\vdash u:1$, then both $\llbracket u\rrbracket_\Gamma$ and $\llbracket\star\rrbracket_\Gamma$ are morphisms $\llbracket\Gamma\rrbracket\to T$. By terminal uniqueness, \begin{align*} \llbracket u\rrbracket_\Gamma=\llbracket\star\rrbracket_\Gamma. \end{align*} [/step] [step:Verify the function beta eta equations using the exponential adjunction] For function beta, suppose $\Gamma,x:A\vdash r:B$ and $\Gamma\vdash a:A$. Let \begin{align*} h=\llbracket r\rrbracket_{\Gamma,x:A}:\llbracket\Gamma\rrbracket\times\llbracket A\rrbracket\to\llbracket B\rrbracket. \end{align*} The interpretation of $(\lambda x:A.\,r)\,a$ is \begin{align*} \operatorname{ev}_{\llbracket A\rrbracket,\llbracket B\rrbracket}\circ\langle \Lambda(h),\llbracket a\rrbracket_\Gamma\rangle. \end{align*} The counit identity for the exponential adjunction says \begin{align*} \operatorname{ev}_{\llbracket A\rrbracket,\llbracket B\rrbracket}\circ(\Lambda(h)\times\operatorname{id}_{\llbracket A\rrbracket})=h. \end{align*} Composing this identity with $\langle \operatorname{id}_{\llbracket\Gamma\rrbracket},\llbracket a\rrbracket_\Gamma\rangle:\llbracket\Gamma\rrbracket\to\llbracket\Gamma\rrbracket\times\llbracket A\rrbracket$ gives \begin{align*} \llbracket (\lambda x:A.\,r)\,a\rrbracket_\Gamma=h\circ\langle \operatorname{id}_{\llbracket\Gamma\rrbracket},\llbracket a\rrbracket_\Gamma\rangle. \end{align*} Let $\tau:\Gamma\Rightarrow\Gamma,x:A$ be the syntactic substitution whose components on the variables of $\Gamma$ are those variables themselves and whose last component is $a$. By the recursive definition of substitution morphisms, the restriction of $\llbracket\tau\rrbracket$ to the old variables has the same projections as $\operatorname{id}_{\llbracket\Gamma\rrbracket}$, hence is $\operatorname{id}_{\llbracket\Gamma\rrbracket}$ by repeated product uniqueness. Therefore \begin{align*} \llbracket\tau\rrbracket=\langle \operatorname{id}_{\llbracket\Gamma\rrbracket},\llbracket a\rrbracket_\Gamma\rangle:\llbracket\Gamma\rrbracket\to\llbracket\Gamma\rrbracket\times\llbracket A\rrbracket. \end{align*} The morphism on the right is $\llbracket r[a/x]\rrbracket_\Gamma$ by the substitution lemma applied to $r$ and $\tau$. Hence the function beta equation is sound. For function eta, suppose $\Gamma\vdash f:A\to B$. Let \begin{align*} k=\llbracket f\rrbracket_\Gamma:\llbracket\Gamma\rrbracket\to\llbracket B\rrbracket^{\llbracket A\rrbracket}. \end{align*} In the extended context $\Gamma,x:A$, the interpretation of $f\,x$ is \begin{align*} \operatorname{ev}_{\llbracket A\rrbracket,\llbracket B\rrbracket}\circ\langle k\circ\pi_1^{\llbracket\Gamma\rrbracket,\llbracket A\rrbracket},\pi_2^{\llbracket\Gamma\rrbracket,\llbracket A\rrbracket}\rangle. \end{align*} This is the uncurried morphism corresponding to $k$. By the unit identity for the exponential adjunction, transposing it returns $k$. Therefore \begin{align*} \llbracket \lambda x:A.\,f\,x\rrbracket_\Gamma=\llbracket f\rrbracket_\Gamma. \end{align*} The function eta equation is sound. [/step] [step:Conclude soundness for the beta eta equational theory] Each generating $\beta$- or $\eta$-equation for products, the unit type, and functions has equal interpretations by the preceding steps. The interpretation is compatible with substitution by the substitution lemma, and it is compatible with each syntactic term former by its inductive definition: pairing, projection, abstraction, and application are interpreted by functorial composition with the corresponding categorical universal constructions. Therefore equality of interpretations is preserved under all congruence rules of the syntactic equational theory. An induction on derivations of $\Gamma\vdash s\equiv t:A$ in the $\beta\eta$-equational theory gives \begin{align*} \llbracket s\rrbracket_\Gamma=\llbracket t\rrbracket_\Gamma:\llbracket\Gamma\rrbracket\to\llbracket A\rrbracket. \end{align*} Together with the construction of $\llbracket t\rrbracket_\Gamma$ for every typing derivation and the substitution identity \begin{align*} \llbracket t[\sigma]\rrbracket_\Delta=\llbracket t\rrbracket_\Gamma\circ\llbracket\sigma\rrbracket, \end{align*} this proves the stated soundness theorem. [/step]