Exercise 5.10
Consider the following context:
$$\begin{align}Γ ≡ S &: ∗, \\ P &: S →∗, \\ f &: S →S, \\ g &: S →S, \\ u &: Πx : S. (P(fx) →P(gx)), \\ v &: Πx,y : S. ((Px →Py) →P(fx))\end{align}$$
(cf. Notation 3.4.2).
Let $$M ≡ λx : S. v(fx)(gx)(ux)$$
(a) Make a guess at which type $N$ may satisfy $Γ ⊢ M : N$.
(b) Demonstrate that the proof object $M$ does indeed code a proof of the proposition $N$ you have guessed, by elaborating the λP-derivation corresponding to $M$.
(a) Let's rename $x$ to $z$ in the definition of $M$ to aid readability.
$$M ≡ λz : S. v \; (fz) \; (gz) \; (uz)$$
- We start by noting the type of $f$ and $g$ is $S \to S$. So if the type of $z$ is $S$, then the type of $fz$ and $gz$ is $S$.
- The function $v$ takes two arguments of type $S$, and indeed these are $fx$ and $gz$ in the definition of $M$.
- This means $v(fx)(gz)$ has type $((P(fz) →P(gz)) →P(f(fz)))$.
Let's now focus on $(uz)$:
- $u$ is a function that takes one argument of type $S$, and in the definition of $M$ it is applied to $z$ which indeed has type $S$.
- So $(uz)$ has type $(P(fz) →P(gz))$.
Bring it together, we have
- $v(fx)(gz)$ has type $((P(fz) →P(gz)) →P(f(fz)))$, and is applied to $uv$ which has a compatible type $(P(fz) →P(gz))$.
- This means $v(fx)(gz)(uz)$ has type $P(f(fz))$
To conclude, $$N \equiv \Pi z:S . P(f(fz))$$
(b) The following is a λP derivation of $Γ⊢M:N$.
