Exercise 2.14
Find an inhabitant of the type $α →β →γ$ in the following context:
$Γ ≡ x : (γ →β) →α →γ$
Give an appropriate derivation.
The inhabitant we're looking for takes two arguments, and $x$ doesn't match their type, so let's set $ y:α, \; z: β, \; t:γ $.
We construct $λt.z$ which has type $(γ→β)$. If we apply $x$ to this we have $x(λt.z)$ of type $α→γ$. We can apply the combined expression to $y$, which gives us $x(λt.z)y$ which has type $γ$, as desired. All that remains is to abstract on $z$ and then $y$ to give us the following judgement.
$$ x : (γ →β) →α →γ \quad \vdash \quad λy:α.λz:β.x(λt:γ.z)y : α →β →γ$$
The following flag notation proof provides clarity to the above discussion.
