I've often wanted to try and summarize each dimension of the $\lambda$-cube and what they represent, so I'll give this one a shot.
But first, one should probably try to dis-entangle various issues. The Coq interactive theorem prover is based on an underlying type theory, sometimes lovingly called the calculus of inductive constructions with universes. You'll note that this is more of a mouthfull than simply "Calculus of Constructions", and indeed, there are a lot more things in there than just the CoC. In particular, I think you're confused about exactly which features are in CoC proper. In particular, the Set/Prop distinction and universes do not appear in CoC.
I won't give a full overview of Pure Type Systems here, but the important rule (for functional PTSes like the CoC) is the following
$$\frac{\Gamma\vdash A:s\qquad \Gamma,x:A\vdash B:k}{\Gamma\vdash \Pi x:A.B\ :\ k}\ (s,k)\in R $$
where $s,k$ are elements of a fixed set $S$ of sorts, and the pair $(s,k)$ is in a fixed set $R$ of pairs of $S$, called the rules.
The crucial insight is that careful choices of $S$ and $R$ make huge differences in what the product type $\Pi x:A.B$ actually represents!
In particular, in the calculus of constructions, the set of sorts $S$ is
$$ \{*, \square\}$$
Often called Prop and Type (though this terminology is a bit confusing to a Coq user for reasons I'll talk about later), and the full set of rules:
$$R=\{(*,*),(\square,\square),(\square,*),(*,\square)\} $$
And so we have 4 rules which correspond to 4 different purposes:
$(*,*)$: Function types
$(\square,\square)$: Type families, or types with parameters
$(\square,*)$: Polymorphic types
$(*,\square)$: Dependent types
I'll explain each of these in more detail.
First note that I'll write $A\rightarrow B$ instead of $\Pi x:A.B$ when $x$ doesn't appear in $B$. This notation is much more suggestive, but can hide some important intuition.
Function types: elements of type $*$ are the "ordinary" types and propositions. They would include $\mathrm{nat}$, $\mathrm{bool}$, and things like the proposition $x=y$ for $x$ and $y$ of a given type. In the CoC. these "basic types" and propositions are all mixed together, as they still are in systems like Agda. Coq tends to separate them into two sorts, often called Set and Prop or Type and Prop. This facilitates extraction, and allows us to assume proof irrelevance for things in Prop if we want to (we definitely don't want it for things in Set). The ability to form pi-types at sort $*$ gives us the usual higher-order functions you enjoy in any functional programing language, i.e. the ability to pass functions into other functions.
Type families: This gives you the ability to talk about the familly $\mathrm{list}$ on its own, indeed as a well typed term $\mathrm{list}:*\rightarrow *$, rather than just the instances $\mathrm{list}_{\mathrm{nat}}, \mathrm{list}_{\mathrm{bool}}$, etc. Note that simply forming the type $*\rightarrow *$ requires using the $(\square,\square)$ rule.
Polymorphism: This is controversial, but very useful, and a source of great power in the CoC. The usual motivation is the desire to write the type
$$\Pi t:*.\ t\rightarrow t $$
to be able to type the polymorphic identity $\lambda (t:*)(x:t).x$. Here the quantification $\Pi t:*.\_$ is possible thanks to the $(\square, *)$ rule (though the $t\rightarrow t$ only uses the $(*,*)$ rule).
But it's an interesting fact that we can express all the usual logical operators using this quantifier! Here are a few:
$$A\wedge B := \Pi t:*.\ (A \rightarrow B\rightarrow t)\rightarrow t$$
$$A\vee B := \Pi t:*.\ (A \rightarrow t)\rightarrow(B\rightarrow t)\rightarrow t$$
$$\bot := \Pi t:*.\ t$$
$$\top := \Pi t:*.\ t\rightarrow t$$
$$ \exists x:A.\ P(x):= \Pi t:*.\ (\Pi y: A.\ P(y)\rightarrow t)\rightarrow t$$
That last one actually also uses dependent types (the $(*,\square)$ rule), but this should give you an idea of the power of polymorphism.
In fact, polymorphism is so powerful, that adding inductive types with "large elimination" (the ability to define things in $*$ by recursion) implies the excluded middle is inconsistent with the excluded middle! That's why in Coq, Prop (the analogue of $*$) has some restrictions: no large eliminations, and datatypes should live in Set or Type, which don't have the analogue of the $(\square, *)$ rule. Prop without large eliminations is consistent with the law of excluded middle.
Useful to note: in the presence of $(\square,\square)$, you can even write things like:
$$\Pi c:*\rightarrow *.\ \ c\ \mathrm{nat}\rightarrow c\ \mathrm{nat} $$
if you like, which is useful for, say, writing generic code over a monad, as often happens in Haskell.
Dependent types: This is how you get the propositions-as-types paradigm to work. Indeed, you want to have a type that represents all possible proofs of, say $0=1$. To make sense of this, you want equality to be of type
$$ =\ :\ \mathrm{nat}\rightarrow\mathrm{nat}\rightarrow *$$
or you might want to be polymorphic
$$ =\ :\ \Pi t:*.\ t\rightarrow t\rightarrow *$$
In any case, you can't write $\mathrm{nat}\rightarrow\mathrm{nat}\rightarrow *$ without the rule $(*,\square)$.
Ok, but what about universes? It turns out that in the CoC, you can't actually write things like $\square \rightarrow \square$, because there are no types to give $\square$ and a fortiori no rules involving those types. A pretty natural thing to do is to index $\square$ by a natural number, getting $\square_i$ for $i=1,2,3,\ldots$ and having $\square_i:\square_{i+1}$.
What rules do we want for this? One natural rule is $(\square_i, \square_i)$, but that rule isn't very useful in the absence of the subsumption rule
$$ \frac{\Gamma\vdash A:\square_i}{\Gamma\vdash A:\square_j}\ i\leq j$$
With these extra sorts and rules, you get something that is not a PTS, but something close. This is (almost) the Extended Calculus of Constructions, which is closer to the basis of Coq. The big missing piece here is the inductive types, which I won't discuss here.
Edit: There's a rather nice reference that describes various features of programing languages in the framework of PTSes, by describing a PTS which is a good candidate for an intermediate representation of a functional programing language:
Henk: A Typed Intermediate Language, S. P. Jones & E. Meijer.
soft-question. I do not see an actualy technical question here. Perhaps you can be a bit more specific as to what you're asking? $\endgroup$