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 , has this an impredicative universe. However, it also has a hierarchy of universes (not cumulative). This places it between and Luo's ECC.
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:
It also has dependent products. These bump up the universe level, except with the universe which is impredicative:
These come with the usual rules for abstraction and application, and definitional equalities.
Jaber, Guilhem, Gabriel Lewertowski, Pierre-Marie Pédrot, Matthieu Sozeau, and Nicolas Tabareau. 2016. ‘The Definitional Side of the Forcing’. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 367–76. Association for Computing Machinery. https://doi.org/10.1145/2933575.2935320.
@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},
}