We show that restricting the elimination principle of the natural numbers type in Martin-L\"of Type Theory (MLTT) to a universe of types not containing $\Pi$-types ensures that all definable functions are primitive recursive. This extends the concept of primitive recursiveness to general types. We discuss extensions to univalent type theories and other notions of computability. We are inspired by earlier work by Martin Hofmann, work on Joyal's arithmetic universes, and Hugo Herbelin and Ludovic Patey's sketched Calculus of Primitive Recursive Constructions. We define a theory Tpr that is a subtheory of MLTT with two universes, such that all inductive types are finitary and the lowest universe is restricted to not contain $\Pi$-types. We prove soundness such that all functions $\mathbb{N}\to\mathbb{N}$ are primitive recursive. The proof requires that Tpr satisfies canonicity, which we easily prove using synthetic Tait computability.

翻译：我们证明，在马丁-洛夫类型论（MLTT）中，将自然数类型的消解原则限制在一个不包含Π-类型的类型宇宙上，能确保所有可定义的函数均为原始递归。这一结论将原始递归性的概念扩展至一般类型。我们讨论了这一方法在单值类型论及其他可计算性概念上的推广。本工作受到马丁·霍夫曼的早期研究、若伊算术宇宙的相关工作，以及雨果·赫伯林与卢多维克·帕泰所勾勒的原始递归构造演算的启发。我们定义了一个理论Tpr，它是MLTT的一个子理论，包含两个宇宙，其中所有归纳类型均为有限型，且最低层宇宙被限制为不包含Π-类型。我们证明了该理论的可靠性，即所有函数N→N均为原始递归。该证明要求Tpr满足规范性，而这一性质可借助合成泰特可计算性方法轻松证得。