Exercise 6.7
Given $Γ ≡S : ∗, Q : S →S →∗$, we define in λC the expressions:
$M_1 ≡ λx,y : S. ΠR : S →S →∗. ((Πz : S. Rzz) →Rxy)$
$M_2 ≡ λx,y : S. ΠR : S →S →∗.((Πu,v : S. (Quv →Ruv)) →Rxy)$
(a) Give an inhabitant of $Πa : S. M_1 aa$ and a shortened derivation proving your answer.
(b) Give an inhabitant of $Πa,b : S. (Qab →M_2 ab)$ and a shortened derivation proving your answer.
(a) We first establish that $Πa : S. M_1 aa$ is
$$Πa : S. ΠR : S →S →∗. ((Πz : S. Rzz) →Raa)$$
The following derivation proves the inhabitant is
$$\lambda a:S. \lambda R:S \to S \to *.\lambda f:(\Pi z:S.Rzz). fa$$
(b) We first establish that $Πa,b : S. (Qab →M_2 ab)$ is
$$Πa,b : S. (Qab → ΠR : S →S →∗.((Πu,v : S. (Quv →Ruv)) →Rab))$$
The following derivation proves the inhabitant is
$$\lambda a,b:S. \lambda q:Qab . \lambda R:S \to S \to *.\lambda f:(\Pi u,v : S. (Quv \to Ruv)) . fabq$$
