Basic Definition of Dependent Types? I'm looking at the wikipedia page for Dependent Types and I am getting stuck trying to understand the definition. 
It says, 

... given a type $A:U$ in a universe of types $U$, one may have a
  family of types $B:A\rightarrow U$ which [sic] assigns to each term $a:A$ a type $B(a):U$.

So far, so good. I read from this that a "family of types" $B$ is an ordinary function from a type $A$ to a universe of types $U$, and I deduce that the members $a$ of a type $A$ are called "terms." I get horked on the next sentence:

A function whose codomain varies depending on its argument is a dependent function, ...

As I read it, $B$ cannot be such a function because its codomain $U$ does not vary depending on its argument. The value of $B(a)$, of course, varies depending on its argument $a$, but not the codomain of $B$, which is always the same universe $U$. Perhaps the writer means that the value $B(a)$ at input $a$ is, in turn, the "function whose codomain varies depending on its argument." If so, then $B(a)=u$ is a function whose codomain varies depending on its argument, and that would mean that each type $u$ in $U$ is a function whose codomain varies depending on its argument, but now I'm lost, because I don't know enough about types, in general, to complete the thought.
 A: The article is trying to explain the notion of a dependent product, but the passage you quote is not very precise. To use set-theoretic terms, if $A$ is a set and $B$ is a set-valued function on $A$, the dependent product:
$$
\prod_{x:A} B(x)
$$
denotes the set of all functions $f: A \rightarrow U$, where $U$ is the union of the sets $B(x)$, such that for each $x \in A$, $f(x) \in B(x)$. A member of the dependent product, which the wikipedia article calls a dependent function, is a function equipped with a fine-grained description of its codomain giving a "bound" $B(x)$ on the value of $f(x)$ for each $x$ in its domain.
A: I'm not an expert in type theory, but I agree that the Wikipedia article does not separate the different notions very clearly, at least as far as I understand things.
First, there is the notion of a dependent type, which is a type expression involving free variables from other types. Given such a type expression $t$ involving a free variable $a$ of type $A$, one may - if the type system allows that - form the $\lambda$-abstraction $\lambda _{a:A}.t$, which is a type valued function on $A$, i.e. a term of type $A\to U$ with $U$ the universe of types. Conversely, a type valued function $B: A\to U$ on $A$, $B a$ is a dependent type with free variable $a$ of type $A$. 
If a dependent type $t$ involving a parameter $a:A$ is given, its dependent product type $\prod_{a:A} t$ is another type which has as its terms the $\lambda$-abstractions of terms which have type $t$ in context $a:A$, and these can be understood as dependent functions with their codomain varying depending on the argument. So:
$\left[\text{(dependent type)}\leftrightarrow\text{(type valued function)}\right]\leadsto\text{(dependent product type)}\ni\text{(dependent functions)}$
