Exercise 3.8
Recall that $K ≡λxy. x$ in untyped lambda calculus.
Consider the following types:
$$\begin{align} T1 &≡ Πα,β : ∗. α →β →α \\ \\ T2 &≡ Πα : ∗. α →(Πβ : ∗. β →α) \end{align}$$
Find inhabitants $t1$ and $t2$ of $T1$ and $T2$, which may be considered as different closed λ2-versions of $K$.
An inhabitant of $T1$ is
$$ λα:*.λβ:*.λx:α.λy:β.x $$
This is like $K$ but with each variable typed.
An inhabitant of $T2$ is
$$ λα:*. λx:α . (λβ:*. λy:β. x)$$
This is similar to the previous term but the type of $y$ is delayed until after $x$ is established.
