Dependent Sums and Products

I'm trying to understand the connections between a few different concepts fundamental to dependent type theory.

• Dependent functions ($$\Pi$$-types)
• Including non-dependent functions ($$A \rightarrow B$$)
• Dependent pairs ($$\Sigma$$-types)
• Including non-dependent products ($$A \times B$$)
• Coproducts ($$A + B$$)

Homotopy Type Theory says the following about $$\Sigma$$s and $$\Pi$$s:

[ $$\Sigma$$ ] is called a dependent pair type, or $$\Sigma$$-type, because in set theory it corresponds to an indexed sum (in the sense of a coproduct or disjoint union) over a given type.

The name "$$\Pi$$-type" is used because this type can also be regarded as the cartesian product over a given type

(I don't think I fully understand this point)

In a non-dependent setting I'm accustomed to calling coproducts "sums" because the number of inhabitants of a coproduct is the sum of its constituent types' inhabitants - $$|A+B| = |A| + |B|$$. Likewise I call pairs "products" because $$|(A,B)| = |A| \cdot |B|$$. Also functions can be called exponentials - $$|A \rightarrow B| = |B|^{|A|}$$!

Now for the question.

Why does it make sense in Type Theory to use $$\Sigma$$ for products and $$\Pi$$ for exponentials? It seems like everything is shifted between non-dependent and dependent types.

• sums approximately correspond to dependent coproducts
• products approximately correspond to dependent sums
• exponentials approximately correspond to dependent products

What's the deeper connection?

• Isn't this is in perfect analogy to usual arithmetic? $nm=\sum_{i=1}^mn$, $n^m=\prod_{i=1}^mn$. Sep 24 '14 at 9:29
• The accepted answer is an excellent explanation. I have seen papers that use the notation "dependent function space" and "dependent pair space" instead of "product" and "sum" to avoid this confusion, since the intuition isn't clear if you're not familiar with the underlying theory, particularly for dependently typed programming Oct 30 '21 at 19:20

I think what's confusing you is that $$A \times B$$ is both a product and a coproduct:

• It is the product of two factors, namely $$A$$ and $$B$$.
• It is the coproduct of $$A$$-many copies of $$B$$.

Once you realize this, you will see that we can obtain $$A \times B$$ as both a $$\sum$$ and a $$\prod$$:

1. Take $$P : \mathtt{bool} \to \mathsf{Type}$$ where $$P(\mathtt{false}) = A$$ and $$P(\mathtt{true}) = B$$. Then $$\sum_{b : \mathtt{bool}} P(b) \simeq A + B$$ and $$\prod_{b : \mathtt{bool}} P(b) \simeq A \times B$$

2. Take $$Q : A \to \mathsf{Type}$$ where $$Q(x) = B$$ for all $$x : A$$. Then $$\sum_{x : A} Q(x) \simeq A \times B$$ and $$\prod_{x : A} Q(x) \simeq (A \to B)$$

We should therefore not pay attention to $$A \times B$$ when deciding on a good naming scheme for these two constructs.

The dependent exponential is exactly a dependent product.

• Typo: should be "Q:A->Type where Q(x) = B for all x:A". Oct 29 '21 at 15:15
• Thanks, fixed it. You know, you can edit other people's answers around here. Oct 29 '21 at 20:58