Let $\perp\equiv\Pi\alpha:\ast.\alpha$ and $\Gamma\equiv\beta:\ast,x:\perp$.
(a) Prove that $\perp$ is legal. (in $\lambda2$)
(b) Find an inhabitant of $\beta$ in contex $\Gamma$.
(c) Give three not $\beta$-convertible inhabitants of $\beta\to\beta$ in context $\Gamma$, each in $\beta$-normal form.
(d) Prove that the following terms inhabit the same tyoe in context $\Gamma$:
$\lambda:\beta\to\beta\to\beta.f(x\beta)(x\beta)$, $x((\beta\to\beta\to\beta)\to\beta)$.
This does not make any sense to me. First, $\perp$ is not a $\lambda2$-term but a $\lambda2$-type and only terms can be legal or illegal. Second, $\beta$ is of type $\ast$ (i.e. of type "type") so what does it mean for beta to be inhabited?
Type $\beta$ is inhabited when there exists at least one term whose type is $\beta$. See chapter 2.9 on term finding in $\lambda\rightarrow$.
In this exercise the most important thing is realizing that $\bot$ is a type of terms that given any type produce a term inhabiting that type. So if $x : \bot$ then $x\beta : \beta$ by (appl$_2$) derivation rule. The existence of $\bot$ means that every type can be inhabited - cf. paragraph on impredicativity on top of page 81. If you're familiar with Haskell programming language, then $\bot$ is an equivalent of
undefined- it inhabits every type.