18
$\begingroup$

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?

$\endgroup$

2 Answers 2

14
$\begingroup$

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.

$\endgroup$
5
  • $\begingroup$ This makes sense to me, but it is a bit of a confusing convention then that categories with families, categories with attributes, and natural models are all given different names, if they are just different definitions of the same notion. It is a bit as if "categories with finite limits and power objects", "cartesian closed categories with subobject classifiers", and "locally cartesian closed Heyting pretoposes with coequalizers and power objects" were each given different names in common use, instead of all being called "elementary toposes". $\endgroup$ Mar 18 at 19:21
  • 2
    $\begingroup$ @SridharRamesh I agree! Unfortunately, as you probably know, there are plenty of other situations in mathematics where multiple names for the same concept are still in use for historical reasons. Sometimes a concept is reinvented more than once, and only later do people realize that two things with different names are actually the same. Other times people don't like the existing name(s) and introduce a new one, but not everyone agrees to switch (cf xkcd.com/927). $\endgroup$ Mar 18 at 23:07
  • 2
    $\begingroup$ One can also make an argument that if two definitions that turn out to be the same are nevertheless presented sufficiently differently and the proof of their sameness is nontrivial enough, it's worth maintaining two different names. If "X=Y" is a big theorem, then we may not want to make it sound trivial by using the same word to refer to X and Y. I don't know if I would argue that that's the case here, but some might. $\endgroup$ Mar 18 at 23:09
  • $\begingroup$ So I understand what the difference between (2) and (3) is, but I don't really see what the benefit of (2) is, since (3) seems strictly easier to define. Contexts are lists in the initial model, but why should I care if contexts are lists or not in other models? $\endgroup$
    – Max New
    Apr 28 at 22:30
  • $\begingroup$ @MaxNew A lot of people feel that way, and for fairly good reasons. But I think there are sometimes substantive reasons to use (2). For instance, if every context is built out of types, then operations on types can be lifted to operations on contexts. E.g. once you have identity types, you automatically also have identity contexts. $\endgroup$ Apr 28 at 23:02
4
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.