What are the motivations for different variants of categorical models of dependent type?

Question

I am new to the categorical semantics for dependent type theories, so it is surprising for me to see nLab introduces so many variants of categorical models, including comprehension categories, display map categories, category with attributes, category with families, natural models and contextual categories.

I wonder what are the motivations for these different models? For example, IMHO, I think category with families is one of them that is quite close to the syntax and developed quite early, I am curious what are the disadvantages of CwF that lead to the development of other notions?

Answer 1

I would divide these models into three general groups.

1. Structures that are more "categorical", arising naturally from categories "in nature" without the need for strictification theorems. In particular, in these models substitution/pullback is only functorial up to isomorphism. These include display map categories and comprehension categories. The variations among this group arise in part from how much of the rest of the structure of type theory one wants to retain, e.g. whether a dependent type is treated as a separate notion, or is identified with its projection map, and whether that projection map is equipped with a structure or just a property.

2. Structures that faithfully represent the entire syntax of type theory, with strict substitution, and including the fact that contexts are inductively generated as lists of types. These are contextual categories, a.k.a. C-systems; there's really only one notion here, although it can be named and defined in different-looking ways.

3. Structures that faithfully represent the syntax of type theory, with strict substitution, but with a separate class of things called "contexts" that aren't necessarily inductively generated as lists of types. These are categories with families, categories with attributes, and natural models, which are also really just equivalent ways to define the same thing, so I would say there's really only one notion here too.

Arguably the difference between the last two points is just a difference in the type theory they correspond to: in case (3) the type theory has a judgment $\Gamma \,\mathsf{ctx}$ with rules like $$\frac{\Gamma\,\mathsf{ctx} \qquad \Gamma \vdash A\,\mathsf{type}}{\Gamma,x:A \,\mathsf{ctx}}$$ while in case (2) there is no such judgment, and an ordinary rule like $$\frac{\Gamma\vdash a:A \qquad \Gamma \vdash b:B}{\Gamma \vdash (a,b):A\times B}$$ is actually regarded as a schema of rules parametrized by an external natural number length of context: $$\frac{\cdot\vdash a:A \qquad \cdot \vdash b:B}{\cdot \vdash (a,b):A\times B} \qquad \frac{x:X\vdash a:A \qquad x:X \vdash b:B}{x:X \vdash (a,b):A\times B} \qquad \frac{x:X,y:Y\vdash a:A \qquad x:X,y:Y \vdash b:B}{x:X,y:Y \vdash (a,b):A\times B} \qquad\cdots$$ However, even when using type theories without a context-judgment, structures of type (3) occupy an intermediate stage between those of type (1) and type (2). Namely, the way to make (1) into (2) is to first apply a strictification theorem to make it into (3), and then apply the "contextual coreflection" to make it into (2). In particular, any type theory without a context judgment can be interpreted in a (3) structure via this contextual coreflection.

Answer 2

I think they are here to show a particular thing of interest, because they're all very similar. There is always a category for contexts whose pullbacks correspond to substitutions, there's always a functor that tells you the types under a certain context, etc., the only difference is that they are described in different perspectives. For example, in CwA you have display maps anyway, and if you start the definition with display maps you get a display map category. If you make some sets isomorphic to global sections of display maps you get a category with families.

In some context, as models of type theories, these constructions are all equivalent modulo technical details, because they are just different ways to describe the same thing. If your model lacks a property needed by the type theory, you'll have to add it, if your model has extra properties not needed by the type theory, it is better to ignore them because they may have consequences (for example, if you prove a theorem about your type theory using a cat model, it may not be true in your type theory but you proved it using the extra properties. You don't want that to happen). So essentially they're equivalent in this sense.

The difference arise when you actually want to do something with the categorical structures themselves, and you can imagine that some definitions are convenient in some sense but not others, etc., so we tend to use the most convenient ones.