\text{CC}_\omega (type theory)

\text{CC}_\omega is a very minimal dependent type theory. It is essentially the negative fragment of the Calculus of Constructions. It is often used as a minimal example for studying syntactic translations.

Like \text{CC}, \text{CC}_\omega has this an impredicative universe. However, it also has a hierarchy of universes (not cumulative). This places it between \text{CC} and Luo's ECC.

Syntax

The type theory has a countable number of universes nested into each other, and an impredicative universe contained in all of them; here they are in Russell-style:

\frac{
  \vdash \Gamma
  \quad
  i < j
}{
  \Gamma \vdash \mathcal{U}_i : \mathcal{U}_j
}
\qquad
\frac{\vdash \Gamma}{\Gamma \vdash \textsf{Prop} : \mathcal{U}_i}

It also has dependent products. These bump up the universe level, except with the \textsf{Prop} universe which is impredicative:

\frac{
  \Gamma \vdash A : \mathcal{U}_i
  \quad
  \Gamma, x : A \vdash \mathcal{U}_j
}{
  \Gamma \vdash (x : A) \to B : \mathcal{U}_{\text{max}(i, j)}
}
\qquad
\frac{
  \Gamma \vdash A : \mathcal{U}_i
  \quad
  \Gamma, x : A \vdash \mathsf{Prop}
}{
  \Gamma \vdash (x : A) \to B : \mathsf{Prop}
}

These come with the usual rules for abstraction and application, and definitional equalities.

References

@inproceedings{jaber_definitional_2016,
	title = {The {Definitional} {Side} of the {Forcing}},
	doi = {10.1145/2933575.2935320},
	booktitle = {Proceedings of the 31st {Annual} {ACM}/{IEEE} {Symposium} on {Logic} in {Computer} {Science}},
	publisher = {Association for Computing Machinery},
	author = {Jaber, Guilhem and Lewertowski, Gabriel and Pédrot, Pierre-Marie and Sozeau, Matthieu and Tabareau, Nicolas},
	year = {2016},
	pages = {367--376},
}