Exercise 3.5
Let $⊥≡Πα : ∗. α$ and $Γ ≡β : ∗, x : ⊥$.
(a) Show that there is a $t$ such that $⊥: t$.
(b) Find an inhabitant of $β$ in context $Γ$.
(c) Give three not β-convertible inhabitants of $β →β$ in context $Γ$, each in β-normal form.
(d) Prove that the following terms inhabit the same type in context $Γ$:
$$λf : β →β →β. f(xβ)(xβ)$$
$$x((β →β →β) →β)$$
(a) Note that this exercise is updated by the errata, replacing the original.
An initial inspection of $⊥≡Πα : ∗. α$ tells us it takes a type $α$, itself of type $*$, and outputs that type. Therefore $⊥≡Πα : ∗. α$ should have type $*$.
To show this more formally, we use the Formation Rule Definition 3.4.7.
$Γ ⊢ B : ∗$ if $Γ$ is a λ2-context, $B ∈\mathbb{T}2$ and all free type variables in $B$ are declared in $Γ$.
Here we have an empty yet valid λ2-context, and $B$ is $Πα : ∗. α$, a λ2-type with no free variable, and so $\emptyset ⊢ Πα : ∗. α : *$. By the Thinning lemma, we then have for any λ2-context $Γ⊢⊥:*$.
(b) The context is not restricting what the inhabitant of $β$ can be, other that it being of type $*$.
The inhabitant must be a valid term, so we use $x$ to form that term.
The term $xβ$ is of type $β$, and so is an inhabitant of $β$.
(c) Three examples of inhabitants of $β→β$ that aren't β-convertible to each other, and are in β-normal form are as follows.
Example 1
$$λz:β\; .z$$
has type $β→β$. The context defines $β$ so we don't need to in this term.
Example 2
$$λβ \; .xβ$$
has type $β→β$. Both $x$ and $β$ are defined in the context so this term does not need to. This is not β-convertible to $λz:β.z$.
Example 3
$$x (β→β)$$
has type $β→β$. This works because $(β→β)$ has type $*$ by the formation rule. This term is not β-convertible to $λz:β.z$ nor $λβ \; .xβ$.
(d) The following flag notation derivation establishes the type of $λf : β →β →β. f(xβ)(xβ)$ as $(\beta \to \beta \to \beta) \to \beta$ in the context $Γ$:
And the following derivation establishes the type of $x((β →β →β) →β)$ also as $(\beta \to \beta \to \beta) \to \beta$ in the context $Γ$:
Therefore the two terms inhabit the same type in the context $Γ$.
