  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.
