No; lookup Calculus of Construction. Dependent types allows you to specify an dependence between different values in your type directly within your type system; which has great implications for type safety and so on.
A classic example is that you can specify the 2-vectors on the unit circle as "{ (x,y) : x,y in R | x^2 + y^2 = 1 }" (read as "the set of real 2-tuples, where their norm is equal to 1".) This is not possible in most languages; the closest you can get in most languages is "{ (x,y) : x,y in R }".
My personal pet peeve with dependent types and proof-driven programming in general is the wealth of options in formulating propositions. I've seen at least five different ways of defining equivalency.
The example normally given is, for instance, being able to define a function whose return type depends of the value (not the type) of its argument – for example, a function which takes in a natural number and returns an array with exactly the length of that natural number.
Dependent types are one of the axes in the Lambda Cube: https://en.wikipedia.org/wiki/Lambda_cube – types have terms the way sets have elements (roughly speaking) and so you can [1] relate types with types (type operators), you can [2] relate terms with types (polymorphism), and lastly [3] types with terms (dependent types) – giving a three-dimensional type theoretic space.
(Btw, I don't know if it even makes sense to talk about relating terms with terms or what feature of type theory captures this notion – so don't ask me!)
