In more expressive calculi such as System F, the Church numerals, by virtue of their design, allow for iteration over an arbitrary type.  Can this effect be replicated in the simply typed case?To be precise, consider the simply typed lambda calculus with a single base type $0$, giving the Church numerals the type $\mathsf{N} := (0 \rightarrow 0) \rightarrow 0 \rightarrow 0$.  For any type $\sigma$, can we find a closed term $\mathsf{it}_\sigma : \mathsf{N} \rightarrow (\sigma \rightarrow \sigma) \rightarrow \sigma \rightarrow \sigma$ with the property that$$\mathsf{it}_\sigma \underline{n} f x \rightsquigarrow f^nx$$?
Does the simply typed lambda calculus have general iteration?
lambda calculus;typed lambda calculus