 Church numeral arithmetic

Church numeral successor, addition, multiplication, and exponentiation are represented by $\lambda nfx.f(nfx)$, $\lambda mnfx.mf(nfx)$, $\lambda mnfx.m(nf)x$, and $\lambda mnfx.(nm)fx$. The last term takes the base first and the exponent second. Its outer abstractions preserve the usual numeral normal form at exponent zero, implementing $m^0=1$, including $0^0=1$. At base type $A$, exponentiation uses an exponent at Church type $C_{A\to A}$ and a base at $C_A=(A\to A)\to A\to A$.