The classical viewpoint is that we can found mathematics by specifying a formal system $F$ whose theorems are precisely those of ZFC. However, since $F$ has essentially no support for the concept of a definition, we have to also make use of another system $G$ for managing all our definitions. We write proofs in the (dynamic, extensible) language of $G$, and $G$ then translates our proofs into the language of ZFC so that system $F$ can verify their validity.
Question. How do definitions work in Martin-Lof type theory? Do we still need a second formal system $G$ for managing all our definitions, or does Martin-Lof have some kind of innate support for them?
I guess that the answer to your question is no, but I also believe that a little of explaination is required.
The point is that there is no formal system which is exensible, at least not in the sense that you can throw in new constant.
At the very beginning of defining every formal system you have to specify the basic terms from which you build every other construct in the language (terms, formulas and judgments). Once you have stated what are such constants they are fixed, if you change them you are changing the language, hence the formal system.
What we actually do in set theory is this: we consider an extension of ZFC-language, that has more symbols than ZFC ($\subseteq$,$\cap$,$\cup$,...) and consider ZFC axioms in such extended language. The we add new axioms, the definitions, which usually have the form of equations (for terms' definitions) or of double-implications (for predicates' definitions), the purpose of this axioms is state an equivalence in the formal system that allows to substitue complex terms/formula build in the old language with simpler objects. And that's what definitions are for, allows substitution of complex terms by simpler one.
By the way it can be formally proved that every theorem of such expanded language, which is a formula in ZFC-(non extended)language can be equally proved in ZFC. So this change of formal system doesn't change the deductive power of the system. If you wonder why do we need the non extended system then? the answer is that proving meta-property of any formal system it's easier if the language has the very few primitives.
Type theories of any kind having their own languages cannot escape this fate either.
Hope this helps.