Exercise 2.17
Prove Lemma 2.10.9 (the ‘Uniqueness of Types Lemma’).
(Hint: use Lemma 2.10.7 (the ‘Generation Lemma’).)
The Uniqueness of Types Lemma 2.10.9 is:
Assume $Γ ⊢M : σ$ and $Γ ⊢M : τ$. Then $σ ≡τ$.
The Generation Lemma 2.10.8 is:
(1) If $Γ ⊢x : σ$, then $x : σ ∈ Γ$
(2) If $Γ ⊢MN : τ$, then there is a type $σ$ such that $Γ ⊢ M : σ →τ$ and $Γ ⊢N : σ$
(3) If $Γ ⊢λx : σ. M : ρ$, then there is $τ$ such that $Γ, x : σ ⊢M : τ$ and $ρ ≡σ →τ$.
All λ-terms are the result of being constructed by one of the (var), (appl) or (abst) rules, as per the Derivation rules of Definition 2.4.5. This means we can use structural induction for each of these three modes of constructing an arbitrary λ-term.
(var)-rule
If $Γ⊢x:α$ and $Γ⊢x:β$ are the results of the (var) rule, then the context $Γ$ must contain $x:α$ and $x:β$, by the Generation Lemma.
To be well-formed, there can only be one $x$ in $Γ$ and so $x:α \equiv x:β$, which means $α \equiv β$.
(appl)-rule
If $Γ⊢AB:α$ and $Γ⊢AB:β$ are the results of the (appl) rule, then as premises to the (appl) rule we must have, by the Generation Lemma,
$$Γ⊢A:γ→α \quad \text{and} \quad Γ⊢B:γ$$
$$Γ⊢A:σ→β \quad \text{and} \quad Γ⊢B:σ$$
As an induction hypotheses we assume the uniqueness of types applies to these premises. That means
$$γ→α \equiv σ→β$$
$$γ \equiv σ$$
The first gives us $α \equiv β$. Thus we have shown that the type of $AB:α$ and $AB:β$ are the same.
(abst)-rule
If $Γ⊢λx:σ.M:α$ and $Γ⊢λx:σ.M:β$ are the results of the (abst) rule, then the premises to the (abst) rule must be, by the Generation Lemma,
$$Γ, x:σ⊢M:γ \qquad \text{and} \qquad {α \equiv σ→γ}$$
$$Γ, x:σ⊢M:ρ \qquad \text{and} \qquad {β \equiv σ→σ}$$
As an induction hypotheses we assume the uniqueness of types for these premises. This gives us $ γ \equiv ρ $, which immediately gives us $α \equiv β$.
Thus $Γ⊢λx:σ.M:α$ and $Γ⊢λx:σ.M:β$ have the same type.
By showing the uniqueness lemma holds for each mode of construction, we have shown it holds for arbitrary λ-terms.
