# 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 dependent 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 about dependent exponentials?

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$. – Emil Jeřábek Sep 24 '14 at 9:29

## 1 Answer

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 $P(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.