Dependent Sums and Products

Question

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

What's the deeper connection?

Answer 1

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.