Dependent types allow quantifiers over values, which is very important in describing propositions. This is impossible in, for example, simple type theory (on the other hand, it is not necessary to represent propositions using types. You may use a separate language for propositions).
For example, $\forall a\in\mathbb N.\forall b\in\mathbb N.a+b=b+a$ is a dependent type (well, this assumes a type-theoretical definition of $=$), which is a dependent function type with two parameters of type $\mathbb N$, that can be applied (just like normal function application). For example, applying an argument $0$ to it results in another dependent function of type $\forall b\in\mathbb N.0+b=b+0$.
Apart from forall quantifiers, mathematical structures such as groups, rings, categories can also be represented by a dependent type (a dependent tuple type). For example, $\exists A\in \mathcal U. a\in A$ represents a pointed set (the symbol $\mathcal U$ contains all small sets).