This is possibly something I've overlooked while reading the HoTT book (section 1.5), on defining the product types and proving the uniqueness principle for it (every element of a product type is a pair). I attach the relevant excerpts from the book and my understanding:
The way to construct pairs is obvious: given $a : A$ and $b : B$, we may
form $(a,b) : A \to B$. … We expect that “every element of $A \to B$
is a pair”, which is the uniqueness principle for products; we do not
assert this as a rule of type theory, but we will prove it later on as
a propositional equality.Now, how can we use pairs, i.e. how can we define functions out of a
product type? Let us first consider the definition of a non-dependent
function $f : A \times B \to C$. Since we intend the only elements of
$A \times B$ to be pairs, we expect to be able to define such a
function by prescribing the result when f is applied to a pair $(a, b)$.
We can prescribe these results by providing a function $g: A \to B \to C$.
Thus, we introduce a new rule (the elimination rule for products),
which says that for any such $g$, we can define a function $f: A \times B \to C$
by $f((a,b)) :\equiv g(a)(b)$.
The first paragraph defines the product type $A \times B$ by providing the single constructor of it. The text emphasises that the statement "every element of $A \to B$ is a pair" is not assumed (as one might expect by simply looking at the single constructor) but rather proven later, by applying the elimination rule defined in the second paragraph to construct a function of type $\textsf{uniq}_{A \times B}: \prod_{x:A \times B} ((\textsf{pr}_1(x), \textsf{pr}_2(x)) =_{A \times B} x)$, which witnesses that every element of $A \times B$ is propositionally equal to some pair, therefore proving that every element of the product type is a pair.
The circularity I'm finding is the formulation of the elimination rule itself. In particular, the rule states that:
For any such $g$, we can define a function $f: A \times B \to C$
by $f((a,b)) :\equiv g(a)(b)$.
The formulation of this rule apparently already assumes that every element of type $A \times B$ can be written in the form of a pair $(a,b)$, as the argument of $f$ is given directly in the form of a pair — this should not have been possible without assuming that 'every element of type $A \times B$ is a pair'. Although intuitively we 'know' that this statement is true as the pair is the only constructor, I'm finding this reasoning awkward since it then defeats the purpose of proving that statement again if we are allowed to resort to that kind of reasoning in the first place.
Best Answer
There's a bit of subtlety with what the HoTT book is saying. When it leaves out the eta rule, it is leaving out a judgmental equality rule:
$$\frac{p : A × B}{(\mathsf{fst}\ p , \mathsf{snd}\ p) \equiv p : A × B}$$
These are the rules that are used for syntactic equality of terms, and generate what it means for two things to be considered 'exactly' equal (for the purpose of checking that things are well-typed and so on). So, by omitting this rule, you cannot freely substitute $p$ for $(\mathsf{fst}\ p, \mathsf{snd}\ p)$, because they are considered distinct terms. And this means that (for example) a variable term $p : A × B$ is not exactly equal to a term built from a constructor $(M , N)$ for any $M$ and $N$. This also has semantic consequences, in that there can be semantic values of $A × B$ that are not produced by the constructor, provided it is possible to say how the various operations on products act on them.
The principle that to define a function $f : A×B → C$, it is sufficient to specify what it does on $(x,y)$, is the analogue of recursion on products (although products are not actually recursive/self-referential). Similarly, a dependently typed version for $f : Π_{p:A×B}\ C(p)$ is analogous to induction. One can instead specify that there is an eliminator $\mathsf{uncurry}$ that takes functions $g : A → B → C$ to functions $\mathsf{uncurry}\ g : A×B → C$, with the computation rule $\mathsf{uncurry}\ g\ (x, y) \equiv g\ x\ y$.
It is typical to justify induction to new students by saying that it asserts, "every product value is built from a constructor." However, since you're reading the HoTT book, you should be suspicious of this explanation, because not long from now you will learn about the identity induction principle:
$$\frac{x:A\quad R : Π_{y:A}x=y → \mathcal{U}\quad r : R\ x\ \mathsf{refl}\quad y:A\quad p : x = y}{\mathsf{J}_{x,R}\ r\ y\ p : R\ y\ p}$$
with compute rule:
$$\mathsf{J}_{x,R}\ r\ x\ \mathsf{refl} \equiv r$$
This is analogous to saying that to define a function:
$$f : \prod_{y:A,p:x = y} R\ y\ p$$
it suffices to give the case for $f\ x\ \mathsf{refl}$ (since $\mathsf{refl}$ is the only constructor). But, the whole point of HoTT is that not every value of the identity type need be $\mathsf{refl}$. There are additional values introduced by the univalence principle and higher inductive types (when you get to those).
So, you should not necessarily think of induction principles as supposing that every value is exactly equal to a constructed value. Rather, for inductive types, explaining how a function works on constructors is sufficient to derive how they work on any values that are not presented by constructors, should they happen to exist.
In the case of products, induction allows proving that there is an identity (as in a value of the identity type) between every value and one given by a constructor. This is what is proved later. But this still doesn't mean that every term is exactly/judgmentally equal to such a term, or that semantically every value is given by a constructor.
In fact, we can even create little models of this within HoTT using the aforementioned higher inductive types. For instance, in Agda I can write (note, Agda uses the opposite convention for $=$ vs $\equiv$ compared to what I was writing above):
So, this type has the usual $(x , y)$, and also a backwards $(y ,, x)$, plus a "higher" constructor declaring that there is an identity between forwards and backwards pairs. But, I can still define the normal-looking induction principle:
(Don't worry too much about the
twistcase.) I've included a (commented) wrong case where we try to define the $(y ,, x)$ case as $f\ x\ y$. This doesn't work, because $C (x, y)$ is not exactly equal to $C (y ,, x)$. But, $C$ must respect identities, not just exact equality, so we can transport the $C(x,y)$ value along the $\mathsf{twist}$ identity to get a corresponding $C(y,,x)$ value. So, even though not every value of $A×B$ here is exactly equal to some $(x,y)$, it suffices to explain what to do on $(x,y)$, because that completely determines what to do on other values. And in fact, we can define projections, and prove the eta identity, even though exact eta equality is simply false:If this part didn't make much sense, don't worry about it. The book doesn't cover this until chapter 6.