Pairs in general (ie binary products) are always sums. A pair type `X * Y` is a multiplication, which is equivalent to `enum {Y y_x0,Y y_x1,Y y_x2,...}` or `Y + Y + Y + ...`, effectively a sum type where the descriminant of the enum is a X, and each case of the enum contains a Y. This is equivalent to how 3 * 7 = 7 + 7 + 7, where you have three terms of size seven.

Similarly, functions in general (ie (binary) exponentiations) are always products. A function type `X -> Y` (or `Y ^ X`) is a exponentiation, which is equivalent to `struct {Y y_x0,Y y_x1,Y y_x2,...}` or `Y * Y * Y * ...`, effectively a product (or latent array) type where the index of the 'array' is a X, and each element of the 'array' is a Y. This is equivalent to how 7 ^ 3 = 7 * 7 * 7, where you have three factors of size seven. (Note that functions have the exponent/argument first and the base/result second.)

All of the above applies without dependent types. Dependent types let the `Y` type depend on which value of type X is involved. (That is, the Y type depends on the X value.)