Error in solution in Types and Programming Languages?
If $power2~m~n$ stands for $m^n$, then it should be

$$power2=λm.λn.n~m$$

Let's try it on $0^1$:
$$
\begin{array}{ll}
&amp; power2~c_0~c_1 \\
= &amp; (λm.λn.n~m)~c_0~c_1 \\
\rightarrow &amp; c_1~c_0 \\
= &amp; (λs.λz.s~z)~c_0 \\
\rightarrow &amp; λz.c_0~z \\
= &amp; λz.(λs.λz.z)~z \\
\rightarrow &amp; λs.λz.z \\
= &amp; c_0
\end{array}
$$
Works fine.

Let's try it on $1^0$:
$$
\begin{array}{ll}
&amp; power2~c_1~c_0 \\
= &amp; (λm.λn.n~m)~c_1~c_0 \\
\rightarrow &amp; c_0~c_1 \\
= &amp; (λs.λz.z)~c_1 \\
\rightarrow &amp; λz.z
\end{array}
$$

Wait, we should have got $c_1$.

Although syntactically $λz. z$ is different from it, but it has the same behavior as $c_1$.
In fact, you can use the function $equal$ (ex. 5.2.7) to prove it:
$$
equal = λm. λn.~and~(iszro~(m~prd~n))~~~(iszro~(n~prd~m))
$$

By the way, another form of the power function, given in the solution to this exercise have the arguments swapped:

$$power1 = λm. λn. m~(times~n)~c_1$$.