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.
How do you get the Calculus of Constructions from the other points in the Lambda Cube?
lambda calculus;type systems;typed lambda calculus;calculus of constructions
First, to reiterate one of cody's points, the Calculus of Inductive Constructions (which Coq's kernel isbased on) is very different from the Calculus of Constructions. It isbest thought of as starting at Martin-Lof 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 isbest 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 eThis 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 eThe 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 eInstead 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. 