Deducing propositional uniqueness for product types

[tbrs2]

In basics.tex, line 1372 (proof of 2.6.4 in the book), the proof concludes with

  Thus, it remains to show $x = (\proj1 x, \proj2x)$.
  But this is the propositional uniqueness principle for product types, which, as we remarked above, follows from \cref{thm:path-prod}.
\end{proof}

where "thm:path-prod" is Theorem 2.6.2, and is being used to deduce the propositional uniqueness principle for product types.

Is it really necessary to invoke 2.6.2 to do this? Is the uniqueness principle for product types not a more elementary fact that can be proved just using induction on the product type, rather than 2.6.2 which also uses induction on identity types? Like in Coq below (definition and setup borrowed from https://github.com/HoTT/HoTT/blob/master/theories/Basics/Datatypes.v).

Record prod (A B : Type) := pair { fst : A ; snd : B}.

Arguments pair {A B} _ _.
Arguments fst {A B} _ / .
Arguments snd {A B} _ / .

Scheme prod_rect := Induction for prod Sort Type.

Lemma propositional_uniqueness A B (x: prod A B) : x = pair (fst x) (snd x).
Proof.
induction x.
simpl.
reflexivity.
Qed.

Thanks,

Tom

[mikeshulman]

Indeed, the propositional uniqueness principle for products was proved in that way in section 1.5.