In HoTT book, section 1.5 (Product Types) in order to define the eliminators for the product type it assumes a function of type $g:A \rightarrow B \rightarrow C$ and then goes on to define the eliminator rule ,saying that we can define a function $f:A \times B \rightarrow C $ for any such g by:
$f((a, b)) :\equiv g (a) (b)$.
Then it states that
Note that in set theory, we would justify the above definition of $f$ by the fact that every element of $A \times B$ is an ordered pair, so that it suffices to define $f$ on such pairs. By contrast, type theory reverses the situation: we assume that a function on $A \times B$ is well-defined as soon as we specify its values on pairs, and from this we will be able to prove that every element of $A \times B$ is a pair.
Would you please explain in further detail what the above paragraph is trying to state?