Finitary type theories with and without contexts

Philipp G. Haselwarter, Andrej Bauer

We give a definition of finitary type theories that subsumes many examples of dependent type theories, such as variants of Martin-Löf type theory, simple type theories, first-order…