4 ms·

Beware here! There are a couple of different products you can sensibly form on data. So you have to make it very explicit which you mean when you talk about the

by jlouis 12y ago

Beware here! There are a couple of different products you can sensibly form on data. So you have to make it very explicit which you mean when you talk about them. You can't generally interchange them in all contexts, but in some contexts you definitely can. 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)

mmarx 12y ago
Any two of those many products, however, are isomorphic, and hence, while still distinguishable, they are “essentially” the same.
- tel 12y ago
  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.
  - mmarx 12y ago
    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.
    - tel 12y ago
      Yeah I think I just misunderstood your statement: I agree with this extension upon it completely.

by jlouis 12y ago

mmarx 12y ago

Any two of those many products, however, are isomorphic, and hence, while still distinguishable, they are “essentially” the same.

tel 12y ago
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.
- mmarx 12y ago
  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.
  - tel 12y ago
    Yeah I think I just misunderstood your statement: I agree with this extension upon it completely.