Confusion about Homotopy Type Theory terminology

I've picked up the Homotopy Type Theory book for leisure. I'm comfortable with strongly typed languages and familiar with dependently typed languages and I enjoy topology, so I thought that the HoTT book was a good opportunity to learn some of the math underlying the type systems (and, by HoTT's reputation, a new way of looking at many other things I know.)

I'd dabbled a bit in formal type theory previous to HoTT. I've long thought of (independent) types like this:

Unit data types are types with only one value, isomorphic to:

data Unity = Unity

You can sum types, creating a type inhabited by as many values as A + B

data Sum a b = Left a | Right b

more commonly known as Either a b in programming circles.

Then there are product types, which house as many types as A × B

data Product a b = Both a b

more commonly known as (a, b).

Finally there are exponential types inhabited by as many values as there are mappings A → B (which is $B^A$). These are more commonly known as functions, and defining them is my day job. The little algebraic type theory I know is founded in those assumptions. (I'm curious what's beyond exponential types in this progression, but that's besides the point.)

The HoTT book starts out by defining the exponential type $\rightarrow$, the dependent function type $\Pi$, the product type $\times$, and the dependent pair type $\Sigma$. The definitions all make sense, but I find the naming confusing. Function types seem pretty exponential to me: why are dependent function types (a generalization of $\rightarrow$) denoted $\Pi$ ('product')?

This doesn't seem like just a silly mistake: the product type $\times$ is generalized to a dependent product type $\Sigma$ ('summation').

Both types are "demoted" when they're generalized (exponential to product, product to sum). There's obviously some reasoning behind this naming, but it's going right over my head.

Why does Homotopy Type Theory use this naming scheme? What's the isomorphism that I'm missing?

The usual names for $\Sigma$-types and $\Pi$-types are dependent sum and dependent product, respectively, but for some reason the Homotopy Type Theory book calls them dependent pair type and dependent function type.

Whatever you call them, they respectively generalise binary products and exponentiation: $X \times Y$ is just the sum of $X$-many copies of $Y$, i.e. $\sum_{x : X} Y$, and $Y^X$ is the product of $X$-many copies of $Y$, i.e. $\prod_{x : X} Y$.