I am reading the article "Introduction to Type Theory" by Herman Geuvers, the chapter explaining the Fitch style of natural inference. I stuck at the exercise 1.3 (first two are simple):
Construct a term of type ((α→β)→α)→(α→α→β)→α
Only abstraction and application rules are allowed.
This math.stackexchange article suggest that to get a term of type α I should assume
| x : (α→β)→α
|-----------------
| | y: α→(α→β)
| |-------------
I have no idea what next.
UPD:
The full answer is:
| x : (α→β)→α
|-----------------
| | y : α→(α→β)
| |-------------
| | | z : α
| | |-----------
| | | yz : α→β
| | | yzz : β
| | λz.yzz : α→β
| | x(λz.yzz) : α
| λy.x(λz.yzz) : α→(α→β)→α
λx.λy.x(λz.yzz) : ((α→β)→α)→(α→(α→β))→α
Thank you Rob
It may help to think of this as an exercise in (functional) programming. You want a function that maps a function $f$ of type $ (\alpha \rightarrow \beta) \rightarrow \alpha$ and a function $g$ of type $\alpha \rightarrow \alpha \rightarrow \beta$ to an element of type $\alpha$. To do this, the only promising approach is to apply $f$ to something and that something must have type $\alpha \rightarrow \beta$. But we can get something of that type using $g$, namely $\lambda x :\alpha \cdot g x x$. So the bottom line of the proof can be the following $\lambda$-expression: $$\lambda f : (\alpha \rightarrow \beta)\rightarrow \alpha\cdot\lambda g : \alpha \rightarrow \alpha \rightarrow \beta\cdot f(\lambda x :\alpha\cdot g x x)$$