Exercise 3.14
We may also introduce the polymorphic booleans in λ2:
$Bool ≡Πα : ∗. α →α →α$
$True ≡λα : ∗. λx,y : α. x$
$False ≡λα : ∗. λx,y : α. y$
Construct a λ2-term $Neg : Bool →Bool$ such that $Neg \; True=_β False$ and $Neg False=_β True$. Prove the correctness of your answer
Let's remind ourselves of the untyped $not := λz. z \; false \; true$. We can generalise this to a λ2 term as follows.
$$Neg ≡ λz:Bool. λα:*. z (Bool)(False)(True)$$
Let's check $Neg \; False=_β True$.
$$\begin{align} Neg \; True & \equiv λz:Bool. λα:*. z (Bool) (False)(True) (False) \\ \\ & \to_\beta (False )(Bool)(False)(True) \\ \\ &\to_\beta (λα : ∗. λx,y : α. y)(Bool)(False)(True) \\ \\ &\to_\beta (λx,y : Bool. y)(False)(True) \\ \\ &\to_\beta True \tag*{$\Box$} \end{align}$$
For completeness, let's check $Neg \; True=_β False$.
$$\begin{align} Neg \; True & \equiv λz:Bool. λα:*. z (Bool) (False)(True) (True) \\ \\ & \to_\beta (True )(Bool)(False)(True) \\ \\ &\to_\beta (λα : ∗. λx,y : α. x)(Bool)(False)(True) \\ \\ &\to_\beta (λx,y : Bool. x)(False)(True) \\ \\ &\to_\beta False \tag*{$\Box$} \end{align}$$
