What is the eta-rule for nat?
I do not understand your notation, but the $\beta$-rule is not right (because you write down abstractions). It is:
\begin{align*}
\mathtt{natrec} \; 0 \; x \; f &amp;= x \\
\mathtt{natrec} \; (\mathtt{succ}\;n) \; x \; f &amp;= f \; n \; (\mathtt{natrec} \; n \; x \; f)
\end{align*}
where $x$ and $f$ are arbitrary (well-typed) terms. (Beware: not every term of a function type is of the form $\lambda x . e$!)

You can read $\beta$ rules as saying what happens when you apply a destructor to a constructor (for instance $\mathtt{fst} (a, b) = a$). An $\eta$-rule says what happens when you destruct a thing and then put it back together (for instance $u = (\mathtt{fst}\;u, \mathtt{snd}\;u)$.

We take numbers apart with $\mathtt{natrec}$ and put them together with $0$ and $\mathtt{succ}$, so the $\eta$-rule would be:
$$\mathtt{natrec} \; n \; 0 \; (\lambda \; x\; m \,.\, \mathtt{succ}\; m) = n.$$