Dependent Sum vs Product Types I just want to clarify the distinction & how dependent sum (sigma) types generalize dependent product types.
Often we see vectors used in examples. So for instance, a product type is introduced with mapping from a given natural number $n$ to an $n$-tuple.
Is it true to say that that dependent sums are more general because we could have a mapping from $n$ to say, an $m$-tuple where $n \neq m $, for any $m, n$?
Thanks.
 A: Dependent sums, i.e. sigma types, don't generalize dependent products, i.e. pi types.  Maybe you meant that they generalize pairs which is true simply via $\Sigma\ \_\!:\!A.B \cong A\times B$. (Similarly, $\Pi\ \_\!:\!A.B \cong A \to B$.)  In fact, these are usually the definitions of $A\times B$ and $A\to B$ in dependent type theories.  
$\mathsf{Vec}\ n\ A$ can be defined as $\Pi n\!:\!\mathbb{N}.\mathsf{Fin}\ n\to A$ which, via a direct generalization of the currying isomorphism, is isomorphic to $(\Sigma n\!:\!\mathbb{N}.\mathsf{Fin}\ n) \to A$.  Here $\mathsf{Fin}\ n$ is the type with exactly $n$ values.  You could view it as $\mathsf{Fin}\ n \cong \{m\in\mathbb{N}\mid m < n\}$. With this perspective $$\Sigma n\!:\!\mathbb{N}.\mathsf{Fin}\ n \cong \{(n,m)\in \mathbb{N}\times\mathbb{N}\mid m < n\}$$ Indeed, if $<$ is proposition-valued, meaning $m < n$ is inhabited by at most one value, then the subset types above can be cast as dependent sums, e.g. $$\{(n,m)\in \mathbb{N}\times\mathbb{N}\mid m < n\} \cong \Sigma (n,m)\!:\!\mathbb{N}\times\mathbb{N}.m < n$$
