Statman's Hierarchy Theorem

In the Simply Typed $\lambda$-calculus Statman investigates the reducibility relation ${\le }_{\beta \eta }$ between types: for $A,B\in {\mathbb{T}}^0$, types freely generated using $\to$ and a single ground type $0$, define $A \leq_{\beta\eta} B$ifthereexistsa$\lambda$-definable injection from the closed terms of type $A$ into those of type $B$. Unexpectedly, the induced partial order is the (linear) well-ordering (of order type) $\omega +4$. In the proof a finer relation ${\le }_h$ is used, where the above injection is required to be a B"ohm transformation, and an (a posteriori) coarser relation ${\le }_{h^{+}}$, requiring a finite family of B"ohm transformations that is jointly injective. We present this result in a self-contained, syntactic, constructive and simplified manner. En route similar results for ${\le }_h$ (order type $\omega + 5$)and$\leq_{h^+}$(ordertype$8$) are obtained. Five of the equivalence classes of ${\le }_{h^{+}}$ correspond to canonical term models of Statman, one to the trivial term model collapsing all elements of the same type, and one does not even form a model by the lack of closed terms of many types.