What is the role of "universe" types in intuitionistic type theory?
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.