Explicit set of types and terms in MLTT Whenever I read a presentation of MLTT, especially in the context of the correspondence of MLTT with LCCCs (eg. Seely's paper), they say "the type constructors/formation rules are..." and then list a bunch of rules, and at least one of the rules will refer to terms. For example, in Seely, you have:


  If $F$ is a type-valued function constant, and $a_1, a_2, \dots a_n$
  are terms of the appropriate types, then $F(a_1, \dots , a_n)$ is a
  type.


And then after, you get the term formation rules, which refer to types. This is supposed to represent some sort of mutual induction, but if you naively interpret a paper as being a sort of short-hand for formal definitions and proofs in set theory + FOL, then the definition given is circular.

Later, you get,


  Let $C(M)$ be the category whose objects are all closed types of M, and morphisms $\mathrm{hom}(A,B)$ are closed terms of type $A \to B$.


A category consists of a set of objects (modulo size issues) and a set of morphisms between each object. Lets say for the sake of argument that I am skeptical that the mutual inductive definitions like Seely's actually give a well-defined set. How do you actually construct the sets of types and terms (more) formally in set theory, and convince me that these actually do form a set?

Not just for the sake of argument, I'm skeptical that the sort of dependent type theory that you can implement on a computer and program with is the same sort of dependent type theory that has this relationship with locally cartesian closed categories.
How do you actually construct the sets of types and terms (more) formally 
  in set theory, and convince me that these actually do form a set?


It's essentially the same argument that BNF grammars define sets.


Start with the set of untyped terms (conventionally dubbed the preterms), and the set of untyped contexts (sequences $x_1:A_1, \ldots, x_n:A_n$ where the $x_i$ are variables and $A_i$ are preterms).
Think of each judgement form as a predicate. Think of $\Gamma \vdash e : A$ as a three-argument predicate on precontexts, preterms, and preterms, $\Gamma \vdash A \mbox{ type}$ as a two-argument predicate on preterms, $\Gamma \vdash e \equiv e' : A$ as a four-place predicate and so on. 
Interpret each rule of MLTT as a predicate transformer. 
So a rule like 
$$
  \frac{\displaystyle \Gamma \vdash e : \Sigma x:A.B}
       {\displaystyle \Gamma \vdash \pi_1 e : A}
  $$
is defining a new predicate $\vdash'(\_, \_, \_)$ from the old predicate $\vdash(\_, \_, \_)$ such that $\vdash'(\Gamma, \pi_1 e, A)$ holds when  $\vdash(\Gamma, e, \Sigma x:A.B)$ holds. 
Observe that every rule is a Horn clause without negation. 
As a result, the predicate transformer induced by the interpretation of a rule is monotone on the inclusion order on the lattice of sets of terms (or tuples of contexts and terms; or tuples of contexts, terms and terms; and so on). 
Furthermore, the pointwise union of monotone predicate transformers is also monotone. So we can interpret all of the rules as jointly defining a monotone predicate transformer.
By the Knaster-Tarski theorem, there is a least fixed point to the this lattice.
That fixed point gives you the set of well-typed terms, contexts, etc.