Andrej Bauer

Finitary Type Theories With and Without Contexts

2023 · Journal of Automated Reasoning

Abstract 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 and higher-order logics, and homotopy type theory. …