Usually when formalizing a system of type theory, from what I've seen, authors usually either simply take the basic ideas of working with derivations, rules, and judgements as basic notions, explaining them informally, and define the type theory by giving a list of relevant rules, or formalize it in set theory (e.x. "a type theory consists of a set R of rules such that...").
However, oftentimes people will talk about models of type theories, for example, from ncatlab:
The models of ML type theory depend crucially on whether one considers the variant of extensional type theory or that of intensional type theory.
The models of the extensional version are (just) locally cartesian closed categories.
What is meant by this? Presumably, there is some way of actually formalizing type theory as an honest to goodness model-theoretic theory (either first order, or perhaps second order I imagine), so that a model of the system of type theory in question means the usual thing in model theory.
My question is: Are there any common approaches in the literature for defining type theory as an honest to goodness theory, and thus making the use of the term "model" the same as the model-theorists notion, or does "model of a type theory" mean something different? Is there even a formal definition of what "model of a type theory" or "theory of type theories" means in general in the literature, or are these definitions simply understood in an ad-hoc way, and only fully specified when talking about specific type theories (i.e. "models of MLTT", "models of HOTT")? If the latter is the case, restricting to particular type theories, have notions like "the theory of MLTT" or "the theory of HOTT", for example, been formalized in the usual model-theoretic context?