$\def\opn{\operatorname}$
In Martin-Löf's dependent type theory, a notion of equality is said to be "intensional" if it distinguishes objects based on their particular definitions, and "extensional" if it does not distinguish objects that have the same observable behaviour.
Therefore, intensional type theory is so named because its judgmental equality $x \equiv y$ is an intensional equality : it says essentially that $x$ and $y$ have the same definition. By contrast, the propositional equality $x =_A y$ is more of an extensional equality. Hence, extensional type theory is so named because it does not admit any purely intensional equality by assuming a reflection rule that forces the judgmental equality to coincide with the more extensional identity type $$\frac{\Gamma \vdash p : \opn{Id}_A(x, y)}{\Gamma \vdash x \equiv y}$$
Regarding Martin-Löf's constructive type theory, we can see that
- In its intensional form, it has sufficient computational content to function as a programming language.
- At the same time, it has identity types whose presence shows that one is really dealing with a form of homotopy type theory.
It appears that homotopy type theory has been revealed to be a practical tool when working with $\infty$-groupoids, because we do not need to define it (describing such structure in set theory is notoriously known to be a difficult task). Instead, we exploit the fact that every type in type theory is an $\infty$-groupoid, with the structure of morphisms, $2$-morphism, $3$-morphisms, … given by the identity type propositional (therefore extensional) equality.
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):
data _×_ (A B : Type) : Type where
_,_ : A -> B -> A × B
_,,_ : B -> A -> A × B
twist : ∀ x y → (x , y) ≡ (y ,, x)
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:
uncurry : ((x : A) -> (y : B) -> C (x , y)) -> (p : A × B) -> C p
uncurry f (x , y) = f x y
-- wrong: C (y ,, x) is not exactly equal to C (x , y)
-- uncurry f (y ,, x) = f x y
uncurry {C = C} f (y ,, x) = subst C (twist x y) (f x y)
uncurry {C = C} f (twist x y i) =
transp (λ j → C (twist x y (i ∧ j))) (~ i) (f x y)
(Don't worry too much about the twist case.) 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:
fst : A × B -> A
fst = uncurry (λ x _ → x)
snd : A × B -> B
snd = uncurry (λ _ y → y)
eta : ∀(p : A × B) → p ≡ (fst p , snd p)
eta = uncurry λ x y → refl
If this part didn't make much sense, don't worry about it. The book doesn't cover this until chapter 6.
Best Answer
The implicit point is that $e_*(s_f)=s_g$ is equivalent to the type of equalities from the left-hand pasting diagram to the right-hand pasting diagram. That is, the two aren't pasted together with each other: the results of the two individual pastings are equated to each other in the type $(s_C \circ Pg) =_{(PW \to C)} (f\circ s_W)$. Thus, constructing an equality between those two diagrams is equivalent to showing $e_*(s_f)=s_g$, which as you noted is what we obviously need to show $(f,s_f) = (g,s_g)$.