Statman's Hierarchy Theorem

Bram Westerbaan, Bas Westerbaan, Rutger Kuyper +3

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$ an…