Statman's Hierarchy Theorem.

In the Simply Typed A-calculus [Hin97, BDS13] Statman investigates the reducibility relation <=(beta eta)0, between types: for A, B is an element of T-0, types freely generated -> using and a single ground type 0, define A <=(beta eta) B if there exists a 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, see [Sta80a, Sta80b, Sta81, BDS13]. In the proof a finer relation <=(h) is used, where the above injection is required to be a Bohm transformation ([Bar84]), and an (a posteriori) coarser relation <=(h+), requiring a finite family of Bohm transformations that is jointly injective. We present this result in a self-contained, syntactic, constructive and simplified manner. En route similar results for <= h (order type w + 5) and <= h(+) (order type 8) are obtained. Five of the equivalence classes of <= 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, [BDS13].