I've been trying to understand the notion of syntactic category for a type theory/logic. This entry in the ncatlab is the closest I've found to a clear explanation. It seems like a fairly good article, but it is not yet entirely clear to me, as it doesn't seem fully precise (whereas others resources seem more formal but rely on a lot of extra technical baggage).
I'd like a precise statement of (1) what exactly do we need to assume from a "type theory" in order to define its syntactic category, and (2) how exactly is the category constructed from the formal system, what are the morphisms precisely.
To illustrate why the ncatlab article doesnt clarify this for me fully:
Presumably this construction works for a very large class of formal deduction systems, rather than specifically for "type theories". This makes the adjunction between theories and categories somewhat ambiguous to me. What exactly do we include in the category of "theories" in this context?
Is a morphism an arbitrary sequence of typing judgments $\Delta \vdash t:T$, or is it a derivation of such a statement in the given type theory's formal deduction system? The article seems to say both at different points.
There is a comment in the article itself stating that it is incomplete.