# What is the origin of the use of $\Pi$ and $\Sigma$ for dependent function and dependent product types in type theory? [duplicate]

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?

• Maybe from "You're going to have to learn how to think in new terms, so we might as well confuse you with notation" approach? :-) Apr 10 '15 at 9:25
• @AsafKaragila Haha that would be my first guess. I have to admit I've never confused them when actually doing type theory; I think once my brain sees the $x : A$ it gets filed in a completely different folder. Apr 10 '15 at 9:30
• – aws
Apr 10 '15 at 9:40
• @aws Thank you! I've flagged the question as a duplicate, sorry about the inconvenience. Apr 10 '15 at 9:44