This is an exercise from Lawvere’s Conceptual Mathematics that is stumping me. It relates to constructing a single map from a starting point of primitive recursive data. Any help or tips would be greatly appreciated.
Exercise 3:
‘Primitive recursion data’ for defining a sequence of functions $A \longrightarrow Y$ consist of an initial function $A \xrightarrow{\;f_0\;} Y$ and a rule $\mathbb{N} \times A \times Y \xrightarrow{\;h\;} Y$ for going from one function to the next. Show that for any primitive recursion data there is exactly one $\mathbb{N} × A \xrightarrow{\;f\;} Y$ for which \begin{align*} f(0, a) &= f_0(a) \qquad \text{for all $a$} \\ f(n + 1, a) &= h(n, a, f(n, a)) \qquad \text{for all $n$, $a$} \end{align*} (Hint: Consider a suitable dynamical system whose state space is $X = \mathbb{N} × Y^A$; see Exercise 12, page 186.)
