The confusion arises from using similar terminology for the structure of a Σ type and for how its values look like.

A **value** of *Σ(x:A) B(x)* is a **pair** *(a,b)* where *a∈A* and *b∈B(a)*. The type of the second element depends on the value of the first one.

If we look at the **structure** of *Σ(x:A) B(x)*, it’s a **disjoint union** (coproduct) of *B(x)* for all possible *x∈A*.

If *B(x)* is constant (independent of *x*) then *Σ(x:A) B* will be just *|A|* copies of *B*, that is *A⨯B* (a product of 2 types).

If we look at the **structure** of *Π(x:A) B(x)*, it’s a **product** of *B(x)* for all possible *x∈A*. Its **values** could be viewed as *|A|*-tuples where *a*-th component is of type *B(a)*.

If *B(x)* is constant (independent of *x*) then *Π(x:A) B* will be just *A→B* – functions from *A* to *B*, that is *Bᴬ* (*B* to *A*) using the set-theory notation – the product of *|A|* copies of *B*.

So *Σ(x∈A) B(x)* is a *|A|*-ary coproduct indexed by the elements of *A*, while *Π(x∈A) B(x)* is a *|A|*-ary product indexed by the elements of *A*.