<p>I'll compliment Neel's (excellent, as usual) answer with a bit more exposition on why levels are used in practice.</p>

<p>The first important limitation of CoC is that it is trivial! A surprising observation is that there is no type for which you can <em>prove</em> that it has more than one element, much less an infinite number of them. Adding just 2 universes gives you the natural numbers with provably infinitely many elements, and all "simple" datatypes.</p>

<p>The second limitation is the computation rules: CoC only supports <em>iteration</em>, i.e. the recusive functions do not have access to the sub-terms of their arguments. For this reason, it is more convenient to add inductive types as a primitive construction, giving rise to the CIC. But now another problem arises: the most natural induction rule (called <em>elimination</em> in this context) is inconsistent with the Excluded Middle! These problems don't appear if you restrict the induction rule to predicative types with universes.</p>

<p>In conclusion, it appears that CoC has neither the expressiveness nor the robustness wrt consistency that you would like in a foundational system. Adding universes solves many of these problems.</p>

CC BY-SA 4.0
2018-06-23T03:52:26.230Z
Do you have some references for the first limitation? If not, could you give hints on how does the second universe helps to prove the (propositional? meta?) inequality?
Łukasz Lew
CC BY-SA 4.0
2018-07-03T22:18:10.047Z
@ŁukaszLew It's actually a simple consequence of the "proof irrelevant" model, which can be somewhat easily googled for. In that model no type has more than 1 element. Having 2 universes prevents that model from existing. Alexandre Miquel's thesis provides a reference for a type with infinite number of elements with 2 universes.
cody
CC BY-SA 3.0
2014-06-02T01:53:22.483Z
2014-06-02T01:53:22.483Z
cody
<p>Actually, the approach of the CoC is more expressive -- it permits arbitrary impredicative quantification. For example, the type $\forall a.\; a \to a$ can be instantiated with itself to get $(\forall a.\; a \to a) \to (\forall a.\; a \to a)$, which is not possible with a universe hierarchy.</p>

<p>The reason it is not widely used is because impredicative quantification is incompatible with classical logic. If you have it, you cannot give a model of type theory where types are interpreted as sets in the naive way --- see John Reynolds's famous paper <a href="http://hal.inria.fr/docs/00/07/62/61/PDF/RR-0296.pdf"><em>Polymorphism is Not Set-theoretic</em></a>. </p>

<p>Since many people want to use type theory as a way to machine-check ordinary mathematical proofs, they are generally unenthusiastic about type-theoretic features which are incompatible with the usual foundations. In fact, Coq  originally supported impredicativity, but they have steadily abandoned it. </p>

CC BY-SA 3.0
2014-05-30T19:49:17.047Z
2014-05-30T19:49:17.047Z
Neel Krishnaswami
<p>Coq, Agda, and Idris have an infinite type hierarchy (Type 1 : Type 2 : Type 3 : ...). But why not do it instead like λC, the system in the lambda cube that's closest to the calculus of constructions, which has only two sorts, $*$ and $◽$, and these rules?</p>

<p>$$\frac {} {∅ ⊢ * : ◽}$$</p>

<p>$$\frac {Γ ⊢ T _ 1 : s _ 1 \qquad Γ, \: x : T _ 1 ⊢ t : T _ 2} {Γ ⊢ (λ \: x : T _ 1, \: t) : (Π \: x : T _ 1, \: T _ 2)}$$</p>

<p>$$\frac {Γ ⊢ T _ 1 : s _ 1 \qquad Γ, \: x : T _ 1 ⊢ T _ 2 : s _ 2} {Γ ⊢ (Π \: x : T _ 1, \: T _ 2) : s _ 2}$$</p>

<p>This seems simpler. Does this system have important limitations?</p>

<coq><dependent-type><calculus-of-constructions>
Why an infinite type hierarchy?
Rui Baptista
# Why an infinite type hierarchy?

(Asked by: username_0 on 2014-05-30)

Coq, Agda, and Idris have an infinite type hierarchy (Type 1 : Type 2 : Type 3 : ...). But why not do it instead like λC, the system in the lambda cube that's closest to the calculus of constructions, which has only two sorts, $\*$ and $◽$, and these rules?

$$\frac {} {∅ ⊢ \* : ◽}$$

$$\frac {Γ ⊢ T \_ 1 : s \_ 1 \qquad Γ, \: x : T \_ 1 ⊢ t : T \_ 2} {Γ ⊢ (λ \: x : T \_ 1, \: t) : (Π \: x : T \_ 1, \: T \_ 2)}$$

$$\frac {Γ ⊢ T \_ 1 : s \_ 1 \qquad Γ, \: x : T \_ 1 ⊢ T \_ 2 : s \_ 2} {Γ ⊢ (Π \: x : T \_ 1, \: T \_ 2) : s \_ 2}$$

This seems simpler. Does this system have important limitations?

**Tags:** coq, dependent-type, calculus-of-constructions

---

## 2 answers

### Answer by username_3 on 2014-05-30. Score: 20 | Accepted answer

Actually, the approach of the CoC is more expressive -- it permits arbitrary impredicative quantification. For example, the type $\forall a.\; a \to a$ can be instantiated with itself to get $(\forall a.\; a \to a) \to (\forall a.\; a \to a)$, which is not possible with a universe hierarchy.

The reason it is not widely used is because impredicative quantification is incompatible with classical logic. If you have it, you cannot give a model of type theory where types are interpreted as sets in the naive way --- see John Reynolds's famous paper [*Polymorphism is Not Set-theoretic*](http://hal.inria.fr/docs/00/07/62/61/PDF/RR-0296.pdf).

Since many people want to use type theory as a way to machine-check ordinary mathematical proofs, they are generally unenthusiastic about type-theoretic features which are incompatible with the usual foundations. In fact, Coq originally supported impredicativity, but they have steadily abandoned it.


---

### Answer by username_1 on 2014-06-02. Score: 9

I'll compliment Neel's (excellent, as usual) answer with a bit more exposition on why levels are used in practice.

The first important limitation of CoC is that it is trivial! A surprising observation is that there is no type for which you can *prove* that it has more than one element, much less an infinite number of them. Adding just 2 universes gives you the natural numbers with provably infinitely many elements, and all "simple" datatypes.

The second limitation is the computation rules: CoC only supports *iteration*, i.e. the recusive functions do not have access to the sub-terms of their arguments. For this reason, it is more convenient to add inductive types as a primitive construction, giving rise to the CIC. But now another problem arises: the most natural induction rule (called *elimination* in this context) is inconsistent with the Excluded Middle! These problems don't appear if you restrict the induction rule to predicative types with universes.

In conclusion, it appears that CoC has neither the expressiveness nor the robustness wrt consistency that you would like in a foundational system. Adding universes solves many of these problems.

> **Comments:**
> **username_2**: Do you have some references for the first limitation? If not, could you give hints on how does the second universe helps to prove the (propositional? meta?) inequality?  
> **username_1**: @ŁukaszLew It's actually a simple consequence of the "proof irrelevant" model, which can be somewhat easily googled for. In that model no type has more than 1 element. Having 2 universes prevents that model from existing. Alexandre Miquel's thesis provides a reference for a type with infinite number of elements with 2 universes.  

---

