From projection function to recursor and viceversa In the HoTT book, page 37, the authors are defining a way to work with product types. They first define
$$pr_1 : A \times B \to A, \quad pr_1 ((a,b)):\equiv a $$
$$pr_2 : A \times B \to B, \quad pr_2 ((a,b)):\equiv b $$
Then they try an alternative way to obtain this result. They consider the functions
$$f:A\times B \to C \qquad g : A \to B \to C$$
Then they define a recursor
$$rec_{A\times B} : \Pi_{(C : \mathcal{U})} (A \to B \to C) \to (A \times B) \to C$$
$$rec_{A\times B} (C, g, (a,b)) :\equiv g(a)(b)$$
In this way, they can define
$$pr_1 :\equiv rec_{A \times B} (A, \lambda a . \lambda b . a)$$ and also $pr_2$ with the same method. 
Finally the authors asks:

We leave it as a simple exercise to show that the recursor can be derived from the projections and vice versa.

Which I think it's the same request you can find in exercise 1.2 at page 71:

Exercise 1.2. Derive the recursion principle for products rec A × B using
  only the projections, and verify that the definitional equalities are valid.
  [Do the same for Σ-types.]

The first request seems to me straighforward:
$$rec_{A \times B} (C, g, (a,b)) :\equiv g(\, pr_1((a,b)), pr_2((a,b)) \,)$$
which should be correct according to these solutions. (is it what they wants? am I cheating?)
But the second request, derive projection from recursor, isn't exactly what they have done above?
 A: Your definition of $rec_{A\times B}$ is slightly incorrect (maybe you have a typo). It's not even type correct as written. The correct definition is: $$rec_{A\times B}(C, g, p):\equiv g(pr_1(p))(pr_2(p))$$
where I've replaced $(a,b)$ with $p$, but the important change is $g$ is a function that returns a function; it only takes one argument. In other words, $rec_{A\times B}$ uncurries $g$. (Well, technically you'd need to lambda abstract $p$ to get the uncurried function.) At the top of the page they mention this distinction, though they also mention that they will (abusively) not make such a distinction later in the book. If you're using that abuse of notation, then your definition is correct, but the logic here is what makes that abuse of notation tolerable, so it doesn't make sense to rely on the abuse of notation when explaining the logic behind it.
You are correct that the book has given the definitions of $pr_1$ and $pr_2$ in terms of $rec_{A\times B}$, but that is only part of the exercise. You need to prove that these definitions of $pr_1$ and $pr_2$ actually satisfy the laws they are expected to satisfy. Similarly, going the other direction with the definition of $rec_{A\times B}$, it's not enough to simply give a definition, you need to prove that it satisfies the laws that $rec_{A\times B}$ should.
