Exercise 3.7
Take $⊥$ as in Exercise 3.5.
Let context $Γ$ be $α : ∗, β : ∗, x : α →⊥, f : (α →α) →α$.
Give a derivation to successively calculate an inhabitant of $α$ and an inhabitant of $β$, both in context $Γ$.
Let's write out the context in an easier to read format.
$$\begin{align}α &: ∗ \\ β& : ∗, \\ x &: α → Πγ:*.γ \\ f &: (α →α) →α \end{align}$$
Let's interpret the meaning of $x$. It is a function that, when supplied with an element of type $α$ returns a function of type $Πγ:*.γ$. That function must be of the form $λγ:*.M$, where $M:γ$. When provided a type $γ$, that function returns a term of type $γ$. So if $m$ has type $ρ$ then $xmα$ has type $α$.
Athough $xmα$ inhabits $α$, there is no $m$ in the context, so we need to abstract it away.
The type of $f$ suggests a term of type $(α→α)$ would be useful. This suggests we try $λm:α.xmα$ which has type $(α→α)$. Now we can easily see that $f(λm:α.xmα)$ has type $α$.
So $f(λm:α.xmα)$ is a term that inhabits $α$, in the given context.
If $m$ has type $ρ$ then $xmβ$ has type $β$. Again we have to abstract $m$ away. Let's try $λm:β.xmβ$ which has type $β→β$. This leads to $f(λm:β.xmβ)$ having type $β$.
So $f(λm:β.xmβ)$ is a term that inhabits $β$, in the given context.
