What are the different approaches to formalizing type theory in the usual model-theoretic context?

Question

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?

Answer 1

Your understanding is a little backwards: first- and second-order logic are special cases of type theories, it's just that they are usually untyped, i.e. they have a single type, which is usually called a sort or a universe of discourse. The notion of a "model of type-theory" applies to first- and second-order logic: models of first-order logic are Heyting categories, while models of second-order logic are toposes.

How does this align with usual model theory? A first-order theory is a first-order logic supplemented with some signature and axioms. The model of a first-order theory (in the type-theoretic sense) is then a Heyting category supplemented with a sound (with respect to the axioms) interpretation of the signature inside the Heyting category. In particular, when you restrict your type-theoretic models so that the ambient category is the category of sets, you recover the notion of a model from classical model theory.

Why are models of type theories categories? It is because we can think of type theories/first- and second-order logic as presentations of categories by generators (the logical and non-logical signature of the type /first-/second-order theory) and relations (the inference rules/logical and non-logical axioms). That is to say, the data that goes into specifying type/first-/second-order theory is the same data that specifies categories, so categories are simply type theories, but seen from a different point of view. (One caveat to that: I think type theories in computer science are slightly more general and perhaps somewhat ahead of the categorical/model-theoretic picture).

Note that model theory itself is only coherent with, but not dependent on the type theory (i.e. on the inference rules of the logic). Rather, model theory begins by deciding to interpret propositions as characteristic morphisms to some object of truth values, and how the latter sits in the ambient category in which you're doing the model theory determines the type theory you're interpreting (e.g. this is how continuous logic and its funky inference rules arise from continuous model theory where we decide models to be metric spaces rather than sets and truth-values to be non-negative reals).

Answer 2

This question is actually a little difficult because what the best answer is is still a subject of ongoing research and debate.

First of all, dependent type theory is definitely not a first order theory so it needs a different kind of "model" to the usual notion from first order logic model theory. Now the problem is not that there is no good notion of model for type theory, but that there are several, and they have different pros and cons and it isn't clear which is the best way or if we have even discovered the best way yet.

All of these notions are based on the basic idea that there should be a category where contexts in type theory are interpreted as objects in the category, and each object comes equipped with a notion of type and term that are used to interpret types and terms in dependent type theory. The oldest kind of model is know as contextual category, from Cartmell, Generalised algebraic theories and contextual categories. These have the advantage of being very close to the syntax of type theory, but have a somewhat technical definition and so can be difficult to work with. At the other extreme are locally cartesian categories. These have a relatively easy definition using well studied ideas from category theory, but with two main disadvantages. Firstly, just to interpret type theory into a locally cartesian closed category is highly non trivial (see Hofmann, On the Interpretation of Type Theory in Locally Cartesian Closed Categories). Secondly, in a general locally cartesian closed category there is only really one way to interpret identity types, and using this interpretation one always gets a model of extensional type theory. This second point makes locally cartesian closed categories not so useful for HoTT, where it is important that the identity types are not extensional. In between contextual categories and locally cartesian closed categories there are several definitions including categories with families, categories with attributes and comprehension categories, that try to find a balance.

See the nlab page on Categorical Models of Dependent Types for more information.

A question of ongoing research is what kind of model should play the role of locally cartesian closed category for intensional dependent type theory. There is general consensus that this should be done using ideas from homotopical algebra such as weak factorisation system, and then interpreting identity type using the ideas in Awodey and Warren, Homotopy theoretic models of identity types. For instance, there is a general "coherence theorem" in Lumsdaine and Warren, The local universes model: an overlooked coherence construction for dependent type theories, that shows how to interpret intensional type theory in a number of categories. These include locally cartesian closed categories that also come equipped with a kind of structure from homotopical algebra known as right proper model structure.