[Supplemental: I rewrote the answer so that any shred of vagueness is gone, as it was evoking religuous zeal, and I would prefer to stick to math. Everything is explained in terms of a widely accepted and general idea of models of computation, namely (typed) realizability theory. There are of course other ways of modeling computation, and anyone else is welcome to present a coherent mathematically mature alternative picture in their own answer.]
We work with typed partial combinatory algebras as models of computation. These include a host of examples, ranging from Turing machines, Turing machines with oracles, $\lambda$-calculi of various kinds, programming languages, topological models based on Scott domains, topological models based on the Baire space, etc.
My notes on realizability cover all the material needed to understand the following definitions and theorems. I shall refer to theorems and definitions therein.
I shall call typed partial combinatory algebras (tpca)"models of computation". We shall also assume that all tpcas under consideration have numerals (Definition 2.6.3 of the notes.)
Kleene's first algbra $\mathbb{K}_1$ is the untyped pca whose elements are natural numbers and application is defined by $m \bullet n = \phi_m(n)$, where $\phi$ is a standard enumeration of partial computable maps.
Definition 1: A model of computation $\mathbb{A}$ is computable if it can be simulated by Turing machines, i.e., there exists a decidable simulation $\mathbb{A} \to \mathbb{K}_1$.
(See Definition 2.8.8 for definition of decidable simulation.)
From definition 1 it follows that any total function $\mathbb{N} \to \mathbb{N}$ realized (Definition 2.8.16) in a computable model is Turing computable.
Definition 2: A model of computation $\mathbb{A}$ is Turing-complete if there exists a decidable simulation $\mathbb{K}_1 \to \mathbb{A}$.
(Note: An alternative definition of Turing completeness of a tpca is given in the notes as 2.8.16. I will leave it as an exercise to think about what happens with the alternative definition.)
Martin-Löf type theory (MLTT) is a model of computation $\mathbb{M}$ whose types are the closed types of MLTT, and the elements of a type $T$ are the closed terms of type $T$, quotiented by definitional equality. (This is a standard way of turning a $\lambda$-calculus into a tpca, see John Longley's PhD for variations, such as using open terms.)
We have the following:
Theorem 3: Suppose $\mathbb{A}$ is a computable total typed combinatory algebra, with a decidable simulation $\gamma : \mathbb{A} \to \mathbb{K}_1$, such that the set $\{n \in \mathbb{N} \mid \exists \mathtt{t} \in |\mathbb{A}_{\mathtt{nat} \to \mathtt{nat}}| .\, \gamma(\mathtt{t}, n)\}$ is computably enumerable. Then $\mathbb{A}$ it is not Turing complete.
Proof. It may help to think of $\{n \in \mathbb{N} \mid \exists \mathtt{t} \in |\mathbb{A}_{\mathtt{nat} \to \mathtt{nat}}| .\, \gamma(\mathtt{t}, n)\}$ as the set of Gödel codes of elements of $\mathbb{A}$ of type $\mathtt{nat} \to \mathtt{nat}$.
Let $e : \mathbb{N} \to \{n \in \mathbb{N} \mid \exists \mathtt{t} \in |\mathbb{A}_{\mathtt{nat} \to \mathtt{nat}}| .\, \gamma(\mathtt{t}, n)\}$ be a computable enumeration. It suffices to find a Turing-computable total map $f : \mathbb{N} \to \mathbb{N}$ which is not realized by $\mathbb{A}$. Such a map $f$ is obtained by diagonalization against $e$: given $n \in \mathbb{N}$, there is $\mathtt{t} \in |\mathbb{A}_{\mathtt{nat} \to \mathtt{nat}}|$ such that $e(n) = \mathtt{t}$, and $f$ can compute (using $\gamma$) $k \in \mathbb{N}$ such that $\mathtt{t}\,\overline{n} + 1 = \overline{k}$. If $f$ were realized by some $\mathtt{f} \in |\mathbb{A}_{\mathtt{nat} \to \mathtt{nat}}|$, it would follow that $\mathtt{f} \, m = \mathtt{f} \, m + 1$ for some $m \in \mathbb{N}$ such that $\gamma(\mathtt{f}, e(m))$. $\Box$
Corollary 4: MLTT qua typed combinatory algebra $\mathbb{M}$ is not Turing complete.
Proof. Obviously, $\mathbb{M}$ is a total tpca. We may define a decidable simuation $\gamma : \mathbb{M} \to \mathbb{K}_1$ by setting $\gamma(\mathtt{t})$ to be the Gödel code of $\mathtt{t}$. The set featuring in the statement of Theorem 3 is computably enumerable because it is decidable whether a given number $n$ encodes a closed term of type $\mathtt{nat} \to \mathtt{nat}$ in MLTT. $\Box$
Remark: Corollary 4 applies to many variations of MLTT, such as MLTT with coinductive types, inductive types, etc, so long as it is decidable whether a given number encodes a closed term of type $\mathtt{nat} \to \mathtt{nat}$.
In type theory we often model computation by a monad, such as the delay monad (or Agda's $\mathtt{IO}$ monad suggested by Guillaume Allais). The basic idea is that the computable partial maps $\mathbb{N} \rightharpoonup \mathbb{N}$ are represented as closed terms of type $\mathtt{nat} \to \mathtt{Delay} \; \mathtt{nat}$, where $\mathtt{Delay}$ is a monad defined in an otherwise total type theory.
This sort of approach essentially corresponds to representing partial computable maps via the Kleene normal form theorem. The so-called "fuel" of the delay monad corresponds to Kleene's use the minimization operator in the normal form theorem.
Can we reintrpret a type theory with such a delay monad as a typed partial combinatory algebra? It seems so, although someone would have to check the details. The idea is to define the function type $\mathtt{t} \to \mathtt{u}$ of the corresponding tpca to be the type $\mathtt{t} \mathtt{Delay} \; \mathtt{u}$ of the type theory, and use the monadic bind to set up the tpca application operation. This should give a Turing-complete model of computation.
However, this is not at all useful to gauge the computational power of a type theory, because we can play the exact same trick with System T already (define $\mathtt{Delay} \; \mathtt{t} = \mathtt{nat} \to \mathtt{t}$ and use the input as fuel).
forloop is awhileloop in practice...) $\endgroup$