What is the role of "universe" types in intuitionistic type theory? According to the Wikipedia article on intuitionsitic type theory:


  The universe types allow proofs to be written about all the types created with the other type constructors. Every term in the universe type $U_0$ can be mapped to a type created with any combination of $0, 1, 2, \Sigma, \Pi, =$, and the inductive type constructor.


Would you please explain and elaborate further on how the universe types allow proofs to be written about other types?
In ordinary set theory one can write statements about all sets using the universal quantifier "$\forall x$" to have $x$ range over all sets.

In type theory without universes there is nothing that allows you to make a type that refers to all types. For example, the statement


  "For all types $A$ and $B$, $A \times B$ and $B \times A$ are equivalent types."


is not a judgement in type theory. It is a meta-statement in which $A$ and $B$ are schematic symbols. In order to express it as a judgement in type theory, we need something else. One solution is to have a universe (and another to have polymorphism a la System $F$). With a universe $U$, we can use "$\prod_{A : U}$" to make a product type that ranges over "for all types $A$ (in the universe $U$)", inside type theory. For instance, the type
$$\prod_{A : U} \prod_{B : U} (A \times B \simeq B \times A),$$
where $X \simeq Y$ is the type of equivalences from $X$ to $Y$, is how one would express the above statement using types.