Notice that \beta\alpha(\mathbf{A},F)=\beta(\mathbf{N(\mathbf{A},F)})=(\mathbf{sH(N(\mathbf{A},F))},[\![N(A,F)^+]\!]), with \mathbf{sH(N(\mathbf{A},F))} =\{[\![(x,y)]\!] : (x,y)\in N(A,F)\}=
\{[\![(x,y)]\!] : x,y\in A, x\land y=0, x\lor y\in F \}.
We define now \eta_A(x)=[\![(x,x^*)]\!], for each object \mathbf{A} of \mathbf{sHF} and for all x\in A, and we prove that \eta=\{\eta_A\} is a natural isomorphism from id_\mathbf{sHF} to \beta\alpha.
\eta_A is well defined: Since x\land x^*=0 and also \mathcal{D}_s(A)\subseteq F it follows that x\lor x^*\in \mathcal{D}_s(A)\subseteq F. Hence, (x,x^*)\in N(A,F).
\eta_A is surjective: If [\![(x,y)]\!]\in\beta\alpha(A,F), then [\![(x,y)]\!]=[\![(x,x^*)]\!]. Indeed, since (x,y)\to(x,x^*)=(x\Rightarrow x, x\land x^*)=(1,0) and (x,x^*)\to(x,y)=(x\Rightarrow x,x\land y)=(1,0), so by definition we have that [\![(x,y)]\!]=[\![(x,x^*)]\!]. Therefore \eta_A(x)=[\![(x,y)]\!].
\eta_A is injective: If [\![(x,x^*)]\!]=[\![(y,y^*)]\!], then (x,x^*)\to(y,y^*)=(x\Rightarrow y,x\land y^*)=(1,0). Therefore, from x\Rightarrow y=1, using properties of semi-Heyting algebras we obtain x\leq y. Analogously, (y,y^*)\to(x,x^*)= (y\Rightarrow x,y\land x^*)=(1,0) implies y\leq x.
\eta_A is a \mathbf{sHF}-morphism:
\eta_A(x)\cup\eta_A(y)=[\![(x,x^*)]\!]\cup[\![(y,y^*)]\!]=[\![(x,x^*)\sqcup(y,y^*)]\!]=[\![(x\lor y,x^*\land y^*)]\!]=[\![(x\lor y, (x\lor y)^*)]\!]=\eta_A(x\lor y).
\eta_A(x)\cap\eta_A(y)=[\![(x,x^*)]\!]\cap[\![(y,y^*)]\!]=[\![(x,x^*)\sqcap(y,y^*)]\!]=[\![(x\land y,x^*\lor y^*)]\!]. Also, \eta_A(x\land y)=[\![(x\land y,(x\land y)^*)]\!]. Since (x\land y,x^*\lor y^*)\to(x\land y,(x\land y)^*)=((x\land y)\Rightarrow(x\land y),(x\land y)\land(x\land y)^*)=(1,0) and (x\land y,(x\land y)^*)\to(x\land y,x^*\lor y^*)=((x\land y)\Rightarrow(x\land y),(x\land y)\land(x^*\lor y^*))=(1,(x\land y\land x^*)\lor(x\land y \land y^*))=(1,0), we have that \eta_A(x)\cap\eta_A(y)=\eta_A(x\land y).
\eta_A(x)\Rightarrow \eta_A(y)=[\![(x,x^*)]\!]\Rightarrow[\![(y,y^*)]\!]=[\![(x,x^*)\Rightarrow(y,y^*)]\!]=[\![(x\Rightarrow y,x\land y^*)]\!]. Also, \eta_A(x\Rightarrow y)=[\![(x\Rightarrow y,(x\Rightarrow y)^*)]\!]. Since (x\Rightarrow y,x\land y^*)\to(x\Rightarrow y,(x\Rightarrow y)^*)=((x\Rightarrow y)\Rightarrow(x\Rightarrow y),(x\Rightarrow y)\land(x\Rightarrow y)^*)=(1,0) and (x\Rightarrow y,(x\Rightarrow y)^*)\to(x\Rightarrow y,x\land y^*)=((x\Rightarrow y)\Rightarrow(x\Rightarrow y),(x\Rightarrow y)\land (x\land y^*))\underset{SH\ref{infimoeimplicaSH})}{=}(1,x\land (y\land y^*))=(1,0), we have that [\![(x\Rightarrow y,x\land y^*)]\!]=[\![(x\Rightarrow y,(x\Rightarrow y)^*)]\!]. Therefore, we conclude that \eta_A(x)\Rightarrow \eta_A(y)=\eta_A(x\Rightarrow y).
\eta_A(F)\subseteq [\![N(A,F)^+]\!]
If y\in\eta_A(F), then y=\eta_A(x), for some x\in F. Hence, y=[\![(x,x^*)]\!], with x\in F.
We observe that for x\in F, we have that (x,0)\in N(A,F). Besides, [\![(x,x^*)]\!]=[\![(x,0)]\!] because (x,0)\to(x,x^*)=(x\Rightarrow x,x\land x^*)=(1,0) and (x,x^*)\to(x,0)=(x\Rightarrow x,x\land 0)=(1,0).
Therefore, we can write y=[\![(x,0)]\!]. Now, since \sim(x,0)=(0,x)\leq(x,0), it follows that (x,0)\in N(A,F)^+, and hence y\in [\![N(A,F)^+]\!].
Finally, we check the naturality of \eta, that is, the following diagram commutes:
\xymatrix{ A \ar[rr]^{\eta_A}\ar[d]_{f} && \beta\alpha(A) \ar[d]^{\beta\alpha(f)} \\
A' \ar[rr]^{\eta_{A'}} && \beta\alpha(A') }
Notice that since \eta_A is an isomorphism, \eta_A^{-1}([\![(x,y)]\!])=x for every x\in A. Then we have
(\eta_{A'}^{-1}\circ \beta\alpha(f)\circ\eta_A)(x)=\eta_{A'}^{-1}(\beta\alpha(f)([\![(x,0)]\!]))=
=\eta_{A'}^{-1}([\![\alpha(f)(x,0)]\!])=\eta_{A'}^{-1}([\![f(x),0)]\!]=f(x).
Thus f=\eta_{A'}^{-1}\circ \beta\alpha(f)\circ\eta_A, and therefore \eta_{A'}\circ f=\beta\alpha(f)\circ\eta_A.
Now we consider the functor \alpha\beta, which transforms every object \mathbf A of \mathbf{sN} into \mathbf{ N(sH(A),[\![A^+]\!])}. On a morphism f:A\longrightarrow A' it is defined by \alpha\beta(f)([\![x]\!],[\![y]\!])=([\![f(x)]\!],[\![f(y)]\!]). We define for each object \mathbf A of \mathbf{sN}, \delta_A:A\longrightarrow \mathbf{ N(sH(A),[\![A^+]\!])} by \delta_A(x)=([\![x]\!],[\![\sim x]\!]).
\delta_A is well defined: On the one hand, [\![x]\!]\cap[\![\sim x]\!]=[\![x\land\sim x]\!]=[\![0]\!], because (x\land\sim x)\to 0=(x\land\sim x)\to (x\land\sim x\land0)=(x\land\sim x)\mbox{ _N } 0=1 and 0\mbox{ _N } (x\land\sim x)=1 by well known properties of Nelson algebras. On the other hand, using SN?) and De Morgan properties we have \sim(x\lor\sim x)=\sim x\land x\leq x\lor\sim x, so x\lor\sim x\in A^+. Therefore [\![x]\!]\cup[\![\sim x]\!]=[\![x\lor\sim x]\!]\in [\![A^+]\!].
\delta_A is surjective: If ([\![x]\!],[\![y]\!])\in\alpha\beta(A,F), then ([\![x]\!],[\![y]\!])=([\![x]\!],[\![\sim x]\!]). Indeed, this is a consequence of ([\![x]\!],[\![y]\!])\to([\![x]\!],[\![\sim x]\!])=([\![x]\!]\Rightarrow [\![x]\!],[\![x]\!]\cap [\![\sim x]\!])=([\![1]\!],[\![x\land\sim x]\!])=([\![1]\!],[\![0]\!]) and ([\![x]\!],[\![\sim x]\!])\to([\![x]\!],[\![y]\!])=([\![x]\!]\Rightarrow [\![x]\!],[\![x]\!]\cap [\![y]\!])=([\![1]\!],[\![0]\!]). Therefore \delta_A(x)=([\![x]\!],[\![y]\!]).
\delta_A is injective: If ([\![x]\!],[\![\sim x]\!])=([\![y]\!],[\![\sim y]\!]), then [\![x]\!]=[\![y]\!] and [\![\sim x]\!]=[\![\sim y]\!], so we have the following: x\to y=1, y\to x=1, \sim x\to \sim y=1, \sim y\to \sim x=1. By proposition 2.11 (?), we have that x\mbox{ _N } y=1, y\mbox{ _N } x=1, \sim x\mbox{ _N } \sim y=1, \sim y\mbox{ _N } \sim x=1, which implies (see for example [viglizzo99algebras], (1.15)) that x=y.
\delta_A is a \mathbf{sN}-morphism:
\delta_A(x)\sqcup\delta_A(y)=([\![x]\!],[\![\sim x]\!])\sqcup([\![y]\!],[\![\sim y]\!])=([\![x]\!]\cup[\![y]\!],[\![\sim x]\!]\cap[\![\sim y]\!])=([\![x\lor y]\!],[\![\sim x\land\sim y]\!])=([\![x\lor y]\!],[\![\sim (x\lor y)]\!])=\delta_A(x\lor y). In a similar manner we can prove that \delta_A(x)\sqcap\delta_A(y)=\delta_A(x\land y).
\sim\delta_A(x)=\sim([\![x]\!],[\![\sim x]\!])=([\![\sim x]\!],[\![x]\!])=\delta_A(\sim x).
\delta_A(x)\to \delta_A(y)=([\![x]\!],[\![\sim x]\!])\to([\![y]\!],[\![\sim y]\!])=([\![x]\!]\Rightarrow[\![y]\!],[\![x]\!]\cap[\![\sim y]\!])=([\![x\to y]\!],[\![x\land\sim y]\!]).
By SN?) and SN?), we see that [\![x\land\sim y]\!]=[\![\sim(x\to y)]\!]. Hence \delta_A(x)\to \delta_A(y)=([\![x\to y]\!],[\![x\land\sim y]\!])=([\![x\to y]\!],[\![\sim(x\to y)]\!])=\delta_A(x\to y).
Finally, \delta is a natural transformation: to see that this diagram commutes,
\xymatrix{ A \ar[rr]^{\delta_A}\ar[d]_{f} && \alpha\beta(A) \ar[d]^{\alpha\beta(f)} \\
A' \ar[rr]^{\delta_{A'}} && \alpha\beta(A') }
we calculate \alpha\beta(f)\circ\delta_A(x)=\alpha\beta(f)([\![x]\!],[\![\sim x]\!])=([\![f(x)]\!],[\![f(\sim x)]\!])=([\![f(x)]\!],[\![\sim f(x)]\!])=\delta_{A'}\circ f(x).