Primitive Recursive Dependent Type Theory

Ulrik Buchholtz, Johannes Schipp von Branitz

We show that restricting the elimination principle of the natural numbers type in Martin-Löf Type Theory (MLTT) to a universe of types not containing $\Pi$-types ensures that all def…