In the type theory I have read (e.g. homotopy type theory) I have seen the following notion used for dependent function types:
$$\prod_{x : A} B(x)$$
and the following for dependent product types:
$$\sum_{x : A} B(x)$$
I am curious as to the origin of this notation; given the use of $\prod$ for indexed products in algebra, I would have guessed that it would be used for the product type. It is also strange because I generally see independent products expressed as $A \times B$ (which is consistent with cartesian products in set theory), and coproducts expressed as $A + B$ (which is consistent with the $\oplus$ notation for categorical coproducts). Based on this, you would expect $\sum_{x : A} B(x) = A + B$ when $B$ is independent of $x$, not $A \times B$.
Does anyone know where these notations come from?