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 &quot;$\Pi$-type&quot; 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 &quot;sums&quot; 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 &quot;products&quot; 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?
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$:


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