One way to interpret the (simply typed) lambda calculus is via coherence spaces (Proofs and Types, chapter 8).  For example, we can consider the space containing token element ($\mathbf{1}$) and the space containing two incoherent tokens ($\mathbf{Bool}$).  These are given as follows:$$  \mathbf{1} = \{\emptyset, \{0\}\}\\  \mathbf{Bool} = \{\emptyset, \{t\}, \{f\}\}$$We can then consider the stable functions from $\mathbf{1}$ to itself:$$    F_1(\emptyset) = \emptyset, F_1(\{0\}) = \emptyset\\    F_2(\emptyset) = \emptyset, F_2(\{0\}) = \{0\}\\    F_3(\emptyset) = \{0\}, F_3(\{0\}) = \{0\}$$The trails of these functions are as follows:$$    \mathcal{Tr}(F_1) = \emptyset\\    \mathcal{Tr}(F_2) = \{(\{0\}, 0)\}\\    \mathcal{Tr}(F_3) = \{(\emptyset, 0)\}$$This again forms a coherence space$$    \mathbf{1 \Rightarrow 1} = \{\emptyset, \{(\{0\}, 0)\}, \{(\emptyset, 0)\}\}$$Which, just like $\mathbf{Bool}$, has two incoherent tokens.  As far as I can see, the two should be equivalent, and there exists a stable function of type $\mathbf{(1 \Rightarrow 1) \Rightarrow Bool}$ which maps $F_2$ to $f$ and $F_3$ to $t$.Can this function be expressed in the lambda calculus?  If not, why is it part of the interpretation?  Can we see $\mathbf{Bool}$ and $\mathbf{1 \Rightarrow 1}$ as the same due to the similarity in coherence space?
How do stable functions 1 => 1 relate to Bool?
lambda calculus;semantics