Dependent type

Remarks

Example: let $\mathsf{Vec}(n)$ be the type of lists of natural numbers of length $n$, for $n : \N$. It is a type family over $\N$, since for each $n$ it gives a type. The function that builds a list of $n$ zeros has type $\Pi_{n : \N} \mathsf{Vec}(n)$: applied to $3$ it gives $(0, 0, 0) : \mathsf{Vec}(3)$, whose type depends on the argument. The type $\Sigma_{n : \N} \mathsf{Vec}(n)$ is the type of lists of any length, each paired with its length.

Non-example: in the simply typed lambda calculus a type cannot mention a term, so $\mathsf{Vec}(n)$ cannot be formed there.

If $B$ does not depend on $x$, then $\Pi_{x : A} B$ is the function type $A \to B$ and $\Sigma_{x : A} B$ is the product type $A \times B$. Under Curry–Howard, a term of $\Pi_{x : A} B(x)$ is a proof of "for all $x$ in $A$, $B(x)$". A term of $\Sigma_{x : A} B(x)$ is a proof of "there is $x$ in $A$ with $B(x)$" that names a witness.