Why are dependent sums and products called sums and products?

Question

The immediate impetus for this is watching this video by Mario Carneiro; around the 8:05 mark he mentions dependent type theory. That reminded me of a question I first had years ago about why dependent products and sums are named the way they are.

A dependent product is a type of the following form $\Pi x : A \mathop. B(x) $. Its terms are functions that convert an $A$ called $x$ into a $B(x)$. If $B$ does not depend on $x$ then you get an ordinary function type.

A dependent sum is a type of the following form $\Sigma x : A \mathop. B(x)$. I do not have any practical experience with these types besides using poking existentials in Rocq with tactics, but I think its terms are basically pairs $(x, y)$ where $x$ is of type $A$ and $y$ is of type $B(x)$. If $B$ does not depend on $x$, then you get a non-dependent product type.

Naively, it seems to make more sense to call $\Pi$-types "dependent exponential types" and $\Sigma$-types "dependent product types" since their degenerate forms appear to be exponentials and products.

The standard terminology must have been chosen for a reason, though. What is it?

Answer 1

We don't call $$\sum_{n=1}^k 3$$ a "product" but rather a "sum", even though it is the same as $k \times 3$, a product. So it shares a name with the operation $+$. In the same way, we call the $\Sigma$-type the sum type, so it shares a name with the type constructor $+$, even though the degenerate case of $\Sigma$ is isomorphic to $\times$, the product. To distinguish the two types, we call $+$ the binary sum, and $\Sigma$ the dependent sum. This is however pretty confusing, so in my opinion it's best to refer to them simply as $\Sigma$ and $\Pi$-types.