1
$\begingroup$

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?

$\endgroup$
4
  • 2
    $\begingroup$ 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? :-) $\endgroup$
    – Asaf Karagila
    Apr 10 '15 at 9:25
  • $\begingroup$ @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. $\endgroup$ Apr 10 '15 at 9:30
  • 1
    $\begingroup$ See math.stackexchange.com/a/459007/59213 $\endgroup$
    – aws
    Apr 10 '15 at 9:40
  • $\begingroup$ @aws Thank you! I've flagged the question as a duplicate, sorry about the inconvenience. $\endgroup$ Apr 10 '15 at 9:44

Browse other questions tagged or ask your own question.