Why product type is a dependent SUM?

Question

It might just be a stupid question but I simply see no obvious reason why dependent sum type is a generalized form of product type. Concretely, the sigma type $\Sigma(x:S)T$ degenerates to a product type if $T$ does not depend on $x$ and is expressed to be $S\times T$ in this case.

Where the SUM part in dependent sum type is coming from? Also, the type of dependent functions is called dependent PRODUCT type. Might I ask why it's called product type as well? I kind of sense that it has something to do with algebraic data type but I can't get through it.

Answer 1

Let's do products first. The usual cartesian product $A \times B$ is also called a binary product because we are making a product of two sets. We could make a ternary product $A \times B \times C$. What is the most general case? Well, to have an index set $I$ and a family of sets $X_i$, one for each $i \in I$, and then we make the product of all these $X_i$'s. This is written as $\prod_{i \in I} X_i$. When $I$ is infinite, it is called an infinitary product. Other products are a special case, for example if we take $I = \{1, 2\}$, $X_1 = A$ and $X_2 = B$ then $\prod_{i \in \{1,2\}} X_i = A \times B$, so a binary product is a special case of the general product.

We can do the previous paragraph in type theory, as there is nothing specific to sets there. Given a type family $i : I \vdash X(i) \ \mathsf{type}$, we may form the type $\prod (i : I) X(i)$. To get a binary product $A \times B$ as a special case, take $I = \mathsf{Bool}$, set $X(\mathsf{false}) = A$ and $X(\mathsf{true}) = B$.

Now let's try sums. I will assume you understand the sum of two sets or types, $A + B$. We could have a ternary sum, $A + B + C$. Again, there is a general case: take a family of sets $(X_i)_{i \in I}$ and form their disjoint sum, or coproduct. In set theory it is written as $\coprod_{i \in I} X_i$, while in type theory it is written as $\sum (i : I) X(i)$ and called dependent sum. One way to see why people call it a sum is to consider how many elements it has. If $A$ has $a$ elements and $B$ has $b$ elements, then $A + B$ has $a + b$ elements. In general, if $X_i$ has $x_i$ elements, then $\sum (i : I) X_i$ has $\sum_i x_i$ elements.

We saw that the binary product is a special case of a general product. But it is also a special case of a dependent sum. Suppose $A = \{0, 1, 2\}$. Then $A \times B = B + B + B$. In general, if we want $A$-many copies of $B$, then that's $$A \times B = \underbrace{B + B + \cdots + B}_{A}$$ Of course, such notation is silly, so we prefer to take $I = A$ and $X_i = B$ and then the same thing is written as $$A \times B = \sum_{i \in I} X_i$$ or to confuse beginners $$A \times B = \sum_{a \in A} B.$$ This just says that $A$ times $B$ is the same thing as adding $A$-many $B$'s together. It's the first thing we're told about multiplication, except that here it's about sets, not numbers (but that's irrelevant, really).