<p>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.</p>

<p>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 <em>the calculus of inductive constructions with universes</em>. 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.</p>

<p>I won't give a full overview of Pure Type Systems here, but the important rule (for <em>functional PTSes</em> like the CoC) is the following</p>

<p>$$\frac{\Gamma\vdash A:s\qquad \Gamma,x:A\vdash B:k}{\Gamma\vdash \Pi x:A.B\ :\ k}\ (s,k)\in R $$</p>

<p>where $s,k$ are elements of a fixed set $S$ of <em>sorts</em>, and the pair $(s,k)$ is in a fixed set $R$ of pairs of $S$, called the <em>rules</em>.</p>

<p>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!</p>

<p>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)\} $$</p>

<p>And so we have 4 rules which correspond to 4 different purposes:</p>

<ul>
<li><p>$(*,*)$: Function types</p></li>
<li><p>$(\square,\square)$: Type families, or types with parameters</p></li>
<li><p>$(\square,*)$: Polymorphic types</p></li>
<li><p>$(*,\square)$: Dependent types</p></li>
</ul>

<p>I'll explain each of these in more detail.</p>

<hr>

<p>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.</p>

<p><strong>Function types</strong>: 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 <em>proof irrelevance</em> 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.</p>

<p><strong>Type families</strong>: 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.</p>

<p><strong>Polymorphism</strong>: 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).</p>

<p>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.</p>

<p>In fact, polymorphism is so powerful, that adding inductive types with "large elimination" (the ability to define things in $*$ by recursion) <strike>implies the excluded middle</strike> is <a href="https://github.com/FStarLang/FStar/issues/360" rel="nofollow noreferrer">inconsistent with the excluded middle</a>! 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 <em>is</em> consistent with the law of excluded middle.</p>

<p>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.</p>

<p><strong>Dependent types</strong>: This is how you get the <em>propositions-as-types</em> 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)$.</p>

<p>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 <em>a fortiori</em> no rules involving those types. A pretty natural thing to do is to <em>index</em> $\square$ by a natural number, getting $\square_i$ for $i=1,2,3,\ldots$ and having $\square_i:\square_{i+1}$.</p>

<p>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 <em>subsumption rule</em>
$$ \frac{\Gamma\vdash A:\square_i}{\Gamma\vdash A:\square_j}\ i\leq j$$</p>

<p>With these extra sorts and rules, you get something that is <em>not</em> a PTS, but something close. This is (almost) the <em>Extended Calculus of Constructions</em>, which is closer to the basis of Coq. The big missing piece here is the inductive types, which I won't discuss here.</p>

<p><strong>Edit:</strong> 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:</p>

<p><a href="https://www.microsoft.com/en-us/research/wp-content/uploads/1997/01/henk.pdf" rel="nofollow noreferrer">Henk: A Typed Intermediate Language</a>, S. P. Jones &amp; E. Meijer.</p>

CC BY-SA 3.0
2016-06-28T07:02:47.790Z
Advanced Topics in Types and Programming Languages, [S2.6](https://books.google.ca/books?id=A5ic1MPTvVsC&pg=PA64) and [S2.7](https://books.google.ca/books?id=A5ic1MPTvVsC&pg=PA71).
Kaveh
CC BY-SA 3.0
2016-06-28T10:28:03.497Z
BTW "Type families" are often also called higher-kinded types.
Martin Berger
CC BY-SA 4.0
2019-09-02T14:04:27.860Z
PTS were a good idea 20 years ago but things have moved on since.
Thorsten Altenkirch
CC BY-SA 4.0
2019-09-03T13:00:52.700Z
@ThorstenAltenkirch no need for exclusionism, Thorsten! There are still some fun things to consider involving PTSes, e.g. Bernardy's work on internalized parametricity comes to mind.
cody
CC BY-SA 4.0
2019-09-06T15:58:15.440Z
@cody No exclusionism intended but we shouldn’t get stuck in the past of syntactic type theory. Bernardi’s work is excellent and can be done better using universes.
Thorsten Altenkirch
CC BY-SA 3.0
2016-06-27T16:13:43.097Z
2017-11-16T13:48:48.283Z
2017-11-16T13:48:48.283Z
cody
<p>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.) </p>

<p>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. </p>

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

<h3>λ→ (Simply-typed lambda calculus)</h3>

<pre><code> k ::= ∗
 A ::= p | A → B
 e ::= x | λx:A.e | e e
</code></pre>

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

<h3>λω_ (STLC + higher-kinded type operators)</h3>

<pre><code> k ::= ∗ | k → k
 A ::= a | p | A → B | λa:k.A | A B
 e ::= x | λx:A.e | e e
</code></pre>

<p>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 <code>k → k</code> which is the type of type-level functions, and abstraction <code>λa:k.A</code> and application <code>A B</code> at the type level as well. So now we don't have polymorphism, but we do have type operators.</p>

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

<h3>λ2 (System F)</h3>

<pre><code> k ::= ∗
 A ::= a | p | A → B  | ∀a:k. A 
 e ::= x | λx:A.e | e e | Λa:k. e | e [A]
</code></pre>

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

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

<h3>λω (System F-omega)</h3>

<pre><code> 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]
</code></pre>

<p>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>

<h3>λP (LF)</h3>

<pre><code> k ::= ∗ | Πx:A. k 
 A ::= a | p | Πx:A. B | Λx:A.B | A [e]
 e ::= x | λx:A.e | e e
</code></pre>

<p>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 <code>Πx:A. B(x)</code> instead of <code>A → B</code>), 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 <code>Πx:A. k</code> , and so we have to add a corresponding abstraction <code>Λx:A.B</code> and application <code>A [e]</code> at the type level as well. </p>

<p>This system is sometimes called LF, or the Edinburgh Logical Framework.</p>

<p>It has the same computational strength as the simply-typed lambda calculus.</p>

<h3>λP2 (no special name)</h3>

<pre><code> 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]
</code></pre>

<p>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' <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.26.957" rel="noreferrer"><em>Induction is Not Derivable in Second Order Dependent Type Theory</em></a>.)</p>

<p>This system has the same strength as System F.</p>

<h3>λPω_ (no special name)</h3>

<pre><code> 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 
</code></pre>

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

<p>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>

<h3>λPω (the Calculus of Constructions)</h3>

<pre><code> 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]
</code></pre>

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

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

CC BY-SA 3.0
2016-06-29T12:21:49.417Z
Of course, technically CoC (without axioms) has at least as many set-theoretic models as the CiC, they just aren't very good at modelling the situation we want, which is the CoC with axioms for the natural numbers (say, $0 \neq 1$).
cody
CC BY-SA 3.0
2016-06-29T12:23:33.910Z
I'd also really appreciate a reference on the conservativity of $\lambda\omega\_$ over the STLC. This seems non-obvious.
cody
CC BY-SA 3.0
2016-06-29T13:16:06.067Z
@cody: I don't know a reference -- Kevin Watkins sketched the proof for me on a whiteboard!  The idea is that you take a term typed in λω_, put all the types into beta-normal eta-long form, and then embed it into STLC by introducing a fresh atomic type for each distinct normal form in the original program. Then it's obvious the reduction sequences must line up one-to-one.
Neel Krishnaswami
CC BY-SA 3.0
2016-06-29T17:57:18.153Z
It's probably useful to note that type level variables can't get instantiated by new terms at reduction time, like in $F_\omega$, in which this proof *shouldn't* work.
cody
CC BY-SA 3.0
2017-12-14T14:46:21.877Z
@cody do you have a reference for 0 !=1 in pure CC without axioms?
user833970
CC BY-SA 3.0
2017-12-15T11:21:52.520Z
@user833970 $0\neq 1$ is *not* provable in CC without axioms (maybe that wasn't clear in the way I said it). Did you want a reference for that fact?
cody
CC BY-SA 3.0
2017-12-15T13:26:14.860Z
@cody I did. After posting I found "Induction Is Not Derivable in Second Order Dependent Type Theory" and "An interpretation of martin-lof’s type theory in a type-free theory of propositions" that someone cited for MLTT without universes.  I hear this fact mentioned a lot, but I need to look into the details since it seems to heavily depend on the encoding of the nats.  It's also never been really clear why this is a "bad" property of CC.
user833970
CC BY-SA 3.0
2017-12-18T20:39:44.267Z
@user833970 the fact that $0\neq 1$ is not derivable is actually much more simple than those other facts you mention, and has nothing to do with the encoding of $\mathrm{nat}$: it comes from the fact that there is a *proof irrelevant* model of CC, in which types have *at most one element*. This is a bad property if you want a logic in which there is a type with more than one element (say, nat). A reference is: *The not so simple proof irrelevant model of CC*, by Miquel and Werner.
cody
CC BY-SA 4.0
2019-09-02T14:03:25.090Z
You say that Fw is "vastly more powerful" than System F. Have you got a reference for this? In particular is there a function on the natural numbers that is provable total in Fw but not in F?
Thorsten Altenkirch
CC BY-SA 4.0
2019-09-03T21:07:36.197Z
Joining Thorsten, I thought that System Fw being stronger than System F was an open question. Urzycyn conjectured that every pure lambda term typable in Fw is typable in F.
András Kovács
CC BY-SA 4.0
2019-09-08T20:45:44.410Z
@ThorstenAltenkirch  No, I don't have a reference! I just remembered that (n+1)-th order classical logic is stronger than n-th order classical logic in the "standard" model, and naively assumed that this applied to F and F-omega as well. If you can tell me the Urzycyn ref then I can edit the post.
Neel Krishnaswami
CC BY-SA 3.0
2016-06-29T10:11:57.947Z
2017-05-03T08:43:23.653Z
2017-05-03T08:43:23.653Z
Neel Krishnaswami
<p>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?</p>

<p>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.</p>

CC BY-SA 3.0
2016-06-27T09:40:29.067Z
At the very least this should be a `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?
Andrej Bauer
CC BY-SA 3.0
2016-06-27T12:21:39.870Z
@AndrejBauer Isn't the question: What is the relationship between the Barendregt-cube/PTS presentation of the CoC and the original presentation by Coquand & Huet?
Martin Berger
CC BY-SA 3.0
2016-06-27T12:24:40.787Z
@AndrejBauer : The question also seems to be asking about the difference in the presentation of CoC (in either guise) and the emphasis on certain features in practice.  It is true that the PTS-oriented version of CoC emphasizes some features as important, while the practice of Coq emphasizes others.  I do agree that it ought to have the soft-question tag.
Jacques Carette
CC BY-SA 3.0
2016-06-27T14:53:14.037Z
I am glad to see someone will be able to answer this.
Andrej Bauer
<lambda-calculus><type-systems><typed-lambda-calculus><calculus-of-constructions>
How do you get the Calculus of Constructions from the other points in the Lambda Cube?
sleepytea
# How do you get the Calculus of Constructions from the other points in the Lambda Cube?

(Asked by: username_0 on 2016-06-26)

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.

**Tags:** lambda-calculus, type-systems, typed-lambda-calculus, calculus-of-constructions
> **Comments:**
> **username_1**: At the very least this should be a `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?  
> **username_2**: @AndrejBauer Isn't the question: What is the relationship between the Barendregt-cube/PTS presentation of the CoC and the original presentation by Coquand & Huet?  
> **username_3**: @AndrejBauer : The question also seems to be asking about the difference in the presentation of CoC (in either guise) and the emphasis on certain features in practice.  It is true that the PTS-oriented version of CoC emphasizes some features as important, while the practice of Coq emphasizes others.  I do agree that it ought to have the soft-question tag.  
> **username_1**: I am glad to see someone will be able to answer this.  

---

## 2 answers

### Answer by username_7 on 2016-06-29. Score: 37 | Accepted answer

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.

> **Comments:**
> **username_4**: Of course, technically CoC (without axioms) has at least as many set-theoretic models as the CiC, they just aren't very good at modelling the situation we want, which is the CoC with axioms for the natural numbers (say, $0 \neq 1$).  
> **username_4**: I'd also really appreciate a reference on the conservativity of $\lambda\omega\_$ over the STLC. This seems non-obvious.  
> **username_7**: @cody: I don't know a reference -- Kevin Watkins sketched the proof for me on a whiteboard!  The idea is that you take a term typed in λω_, put all the types into beta-normal eta-long form, and then embed it into STLC by introducing a fresh atomic type for each distinct normal form in the original program. Then it's obvious the reduction sequences must line up one-to-one.  
> **username_4**: It's probably useful to note that type level variables can't get instantiated by new terms at reduction time, like in $F_\omega$, in which this proof *shouldn't* work.  
> **username_8**: @cody do you have a reference for 0 !=1 in pure CC without axioms?  
> **username_4**: @user833970 $0\neq 1$ is *not* provable in CC without axioms (maybe that wasn't clear in the way I said it). Did you want a reference for that fact?  
> **username_8**: @cody I did. After posting I found "Induction Is Not Derivable in Second Order Dependent Type Theory" and "An interpretation of martin-lof’s type theory in a type-free theory of propositions" that someone cited for MLTT without universes.  I hear this fact mentioned a lot, but I need to look into the details since it seems to heavily depend on the encoding of the nats.  It's also never been really clear why this is a "bad" property of CC.  
> **username_4**: @user833970 the fact that $0\neq 1$ is not derivable is actually much more simple than those other facts you mention, and has nothing to do with the encoding of $\mathrm{nat}$: it comes from the fact that there is a *proof irrelevant* model of CC, in which types have *at most one element*. This is a bad property if you want a logic in which there is a type with more than one element (say, nat). A reference is: *The not so simple proof irrelevant model of CC*, by Miquel and Werner.  
> **username_6**: You say that Fw is "vastly more powerful" than System F. Have you got a reference for this? In particular is there a function on the natural numbers that is provable total in Fw but not in F?  
> **username_9**: Joining Thorsten, I thought that System Fw being stronger than System F was an open question. Urzycyn conjectured that every pure lambda term typable in Fw is typable in F.  
> **username_7**: @ThorstenAltenkirch  No, I don't have a reference! I just remembered that (n+1)-th order classical logic is stronger than n-th order classical logic in the "standard" model, and naively assumed that this applied to F and F-omega as well. If you can tell me the Urzycyn ref then I can edit the post.  

---

### Answer by username_4 on 2016-06-27. Score: 23

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](https://github.com/FStarLang/FStar/issues/360)! 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](https://www.microsoft.com/en-us/research/wp-content/uploads/1997/01/henk.pdf), S. P. Jones & E. Meijer.

> **Comments:**
> **username_5**: Advanced Topics in Types and Programming Languages, [S2.6](https://books.google.ca/books?id=A5ic1MPTvVsC&pg=PA64) and [S2.7](https://books.google.ca/books?id=A5ic1MPTvVsC&pg=PA71).  
> **username_2**: BTW "Type families" are often also called higher-kinded types.  
> **username_6**: PTS were a good idea 20 years ago but things have moved on since.  
> **username_4**: @ThorstenAltenkirch no need for exclusionism, Thorsten! There are still some fun things to consider involving PTSes, e.g. Bernardy's work on internalized parametricity comes to mind.  
> **username_6**: @cody No exclusionism intended but we shouldn’t get stuck in the past of syntactic type theory. Bernardi’s work is excellent and can be done better using universes.  

---

