一句话：通过限制 Martin-Löf 类型论的自然数消去与宇宙，构造 Tpr 理论，使可定义函数均为原始递归。
本文研究如何在依赖类型论中刻画原始递归可定义性。作者把 Martin-Löf 类型论中自然数类型的消去原则限制到不含 Π-类型的宇宙，并定义子理论 Tpr：两个宇宙 U0 : U1，所有归纳类型有穷，且 U0 不含 Π-类型。论文证明 Tpr 可靠，使所有 N → N 可定义函数都是原始递归；证明依赖 Tpr 的 canonicity，并用 synthetic Tait computability 得出。作者还讨论向 univalent 类型论和其他可计算性概念的扩展。
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 ####II-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 [18], work on Joyal's arithmetic universes [27], and Hugo Herbelin and Ludovic Patey's sketched Calculus of Primitive Recursive Constructions [16]. We define a theory Tpr that is a subtheory of MLTT with two universes U0 : U1, such that all inductive types are finitary and U0 is restricted to not contain ####II-types: [EQUATION] We prove soundness such that all functions N → N are primitive recursive. The proof requires that Tpr satisfies canonicity, which we easily prove using synthetic Tait computability [36].