# Tag Info

Accepted

### How do you get the Calculus of Constructions from the other points in the Lambda Cube?

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 ...
• 31.6k

### How do you get the Calculus of Constructions from the other points in the Lambda Cube?

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. ...
• 13.1k
Accepted

### Is MLTT effectively pCiC without Prop?

The short answer is yes, MLTT can reasonably be equated with CIC without impredicative Prop. The main technical issue is that there are dozens of variants when one ...
• 13.1k