How do you get the Calculus of Constructions from the other points in the Lambda Cube? The CoC is said to be the culmination of all three dimensions of the Lambda Cube. This isn't apparent to me at all. I think I understand the individual dimensions, and the combination of any two seems to result in a relatively straightforward union (maybe I'm missing something?). But when I look at the CoC, instead of looking like a combination of all three, it looks like a completely different thing. Which dimension do Type, Prop, and small/large types come from? Where did dependent products disappear to? And why is there a focus on propositions and proofs instead of types and programs? Is there something equivalent that does focus on types and programs?

Edit: In case it isn't clear, I'm asking for an explanation of how the CoC is equivalent to the straightforward union of the Lambda Cube dimensions. And is there an actual union of all three out there somewhere I can study (that is in terms of programs and types, not proofs and propositions)? This is in response to comments on the question, not to any current answers.
First, to reiterate one of cody's points, the Calculus of Inductive Constructions (which Coq's kernel is
based on) is very different from the Calculus of Constructions. It is
best thought of as starting at Martin-Löf type theory with universes,
and then adding a sort Prop at the bottom of the type hierarchy.  This 
is a very different beast than the original CoC, which is
best thought of as a dependent version of F-omega. (For instance, CiC 
has set-theoretic models and the CoC doesn't.) 

That said, the lambda-cube (of which the CoC is a member) is typically presented as a pure type system for reasons of economy in the number of typing rules. By treating sorts, types, and terms as elements of the same syntactic category, you can write down many fewer rules and your proofs get quite a bit less redundant as well. 

However, for understanding, it can be helpful to separate out the different categories explicitly. We can introduce three syntactic categories, kinds (ranged over by the metavariable k), types (ranged over by the metavariable A), and terms (ranged over by the metavariable e). Then all eight systems can be understood as variations on what is permitted at each of the three levels.

λ→ (Simply-typed lambda calculus)

 k ::= ∗
 A ::= p | A → B
 e ::= x | λx:A.e | e e


This is the basic typed lambda calculus. There is a single kind ∗, which is the kind of types. The types themselves are atomic types p and function types A → B. Terms are variables, abstractions or applications.

λω_ (STLC + higher-kinded type operators)

 k ::= ∗ | k → k
 A ::= a | p | A → B | λa:k.A | A B
 e ::= x | λx:A.e | e e


The STLC only permits abstraction at the level of terms. If we add it at the level of types, then we add a new kind k → k which is the type of type-level functions, and abstraction λa:k.A and application A B at the type level as well. So now we don't have polymorphism, but we do have type operators.

If memory serves, this system does not have any more computational power than the STLC; it just gives you the ability to abbreviate types.

λ2 (System F)

 k ::= ∗
 A ::= a | p | A → B  | ∀a:k. A 
 e ::= x | λx:A.e | e e | Λa:k. e | e [A]


Instead of adding type operators, we could have added polymorphism. At the type level, we add ∀a:k. A which is a polymorphic type former, and at the term level, we add abstraction over types Λa:k. e and type application e [A].

This system is much more powerful than the STLC -- it is as strong as second-order arithmetic.

λω (System F-omega)

 k ::= ∗ | k → k 
 A ::= a | p | A → B  | ∀a:k. A | λa:k.A | A B
 e ::= x | λx:A.e | e e | Λa:k. e | e [A]


If we have both type operators and polymorphism, we get F-omega. This system is more or less the kernel type theory of most modern functional languages (like ML and Haskell). It is also vastly more powerful than System F -- it is equivalent in strength to higher order arithmetic.

λP (LF)

 k ::= ∗ | Πx:A. k 
 A ::= a | p | Πx:A. B | Λx:A.B | A [e]
 e ::= x | λx:A.e | e e


Instead of polymorphism, we could have gone in the direction of dependency from simply-typed lambda calculus. If you permitted the function type to let its argument be used in the return type (ie, write Πx:A. B(x) instead of A → B), then you get λP. To make this really useful, we have to extend the set of kinds with a kind of type operators which take terms as arguments Πx:A. k , and so we have to add a corresponding abstraction Λx:A.B and application A [e] at the type level as well. 

This system is sometimes called LF, or the Edinburgh Logical Framework.

It has the same computational strength as the simply-typed lambda calculus.

λP2 (no special name)

 k ::= ∗ | Πx:A. k 
 A ::= a | p | Πx:A. B | ∀a:k.A | Λx:A.B | A [e]
 e ::= x | λx:A.e | e e | Λa:k. e | e [A]


We can also add polymorphism to λP, to get λP2. This system is not often used, so it doesn't have a particular name. (The one paper I've read which used it is Herman Geuvers' Induction is Not Derivable in Second Order Dependent Type Theory.)

This system has the same strength as System F.

λPω_ (no special name)

 k ::= ∗ | Πx:A. k | Πa:k. k'
 A ::= a | p | Πx:A. B | Λx:A.B | A [e] | λa:k.A | A B 
 e ::= x | λx:A.e | e e 


We could also add type operators to λP, to get λPω_. This involves adding a kind Πa:k. k' for type operators, and corresponding type-level abstraction Λx:A.B and application A [e]. 

Since there's again no jump in computational strength over the STLC, this system should also make a fine basis for a logical framework, but no one has done it. 

λPω (the Calculus of Constructions)

 k ::= ∗ | Πx:A. k | Πa:k. k'
 A ::= a | p | Πx:A. B | ∀a:k.A | Λx:A.B | A [e] | λa:k.A | A B 
 e ::= x | λx:A.e | e e | Λa:k. e | e [A]


Finally, we get to λPω, the Calculus of Constructions, by taking λPω_ and adding a polymorphic type former ∀a:k.A and term-level abstraction Λa:k. e and application e [A] for it. 

The types of this system are much more expressive than in F-omega, but it has the same computational strength.