Any two of those many products, however, are isomorphic, and hence, while still distinguishable, they are “essentially” the same.
If I'm reading the op right, this is incorrect. Oftentimes "products" in various contexts are "categorical products cut down by some sensible quotienting". In any category the categorical product will always be the largest (this is essentially what its definition entails) and only by careful choice of category will that correspond to some of the less formal "products" available.
No, altough the wording might have been misleading—I was refering to the second paragraph, while you seem to have applied it to the first. I hope this clarifies the situation a bit:
For any category, the product A * B of two objects A, B (if it exists) is unique only up to isomorphism (this follows from the universal mapping property).
In general, products A * B and C * D need not be isomorphic (and seldomly are), and neither do products from different categories. Many of the commonly-used products actually arise from a product in a suitable category, the cartesian product, for example, is a product in the category of sets.
In Type theory, the product is a product in the sense of category theory, which is a very abstract notion of product indeed. The idea is that given objects, here types, A and B; you can form their product, A * B and that is also a valid object in the category. The diagram then universally identifies the A * B element as the one where you can project out of it via the 1st and 2nd projection such the at given diagram commutes, etc. And it is important to stress there are many products for which this property hold.
(Edited a bit to appease the automatic formatter at HN)