MLTT not being Turing Complete
It is a general feature of reasonable total programming languages that they do not have self-interpreters, but interpreters for reasonable programming languages are Turing-computable. So, a concrete example of a total computable function which is not definable in a total programming language is an interpreter for that programming language.

See Definition 2.1, Theorem 2.2, and Corollary 2.3 of this note. It proves that a self-interpreter for Gödel's T is not definable in Gödel's T. You can use the exact same proof for MLTT.

It is generally well known that a confluent terminating normalization system such as that of MLTT leads to a Turing-computable normalization procedure.