Definition 1.2.13 (Height). The height function is the recursively defined map $h:\mathrm{\Pi }\to \mathbb{N}$ that maps a type variable to $0$, and a function type $\sigma \to \tau$ to $1+\max (h(\sigma ),h(\tau ))$.

We extend the height function from types to $\beta$-redexes by taking the height of its $\lambda$-abstraction.