You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Xuanrui Qi (Jun 25 2021 at 19:26):AFAIK, there are two main approaches of defining categorical semantics for a type theory:
I have seen both styles for STLC, but for MLTT and more complex cases (particularly presheaf semantics of dependent TT), it seems that almost everybody uses the context-based approach. The question is, why do people do this?
I personally prefer the first style as it is more direct. I understand that the context-based style and nameless syntax fix problems like closedness and substitution, but I wonder if those are deal-breakers. For me, the more direct style is much easier to understand and to present.
If anyone has a "direct" presentation of the presheaf semantics of MLTT/intuitionistic type theory, please let me know! Almost everything I have seen are based on contexts and substitutions.
Xuanrui Qi (Jun 25 2021 at 20:09):Hm, I guess the presheaf semantics part of my question makes little sense, but the rest of the question seems to be valid.
Jon Awbrey (Jun 26 2021 at 00:36):How does this relate to ordinary Propositions As Types (Curry–Howard)?
Xuanrui Qi (Jun 26 2021 at 05:21):I don't know much about the categorical semantics of predicate logic, but I guess you get something like propositions as objects? I guess they're related in this way.
Matteo Capucci (he/him) (Jun 26 2021 at 11:04):Xuanrui Qi said:
AFAIK, there are two main approaches of defining categorical semantics for a type theory:
- interpret types as objects, and sequents x : A |- M(x) : B (or more generally, typing judgments) as morphisms (the naive approach of lambdas as morphisms can be considered a subcase);
- contexts as objects, and context maps/substitutions as morphisms.
I have seen both styles for STLC, but for MLTT and more complex cases (particularly presheaf semantics of dependent TT), it seems that almost everybody uses the context-based approach. The question is, why do people do this?
I personally prefer the first style as it is more direct. I understand that the context-based style and nameless syntax fix problems like closedness and substitution, but I wonder if those are deal-breakers. For me, the more direct style is much easier to understand and to present.
If anyone has a "direct" presentation of the presheaf semantics of MLTT/intuitionistic type theory, please let me know! Almost everything I have seen are based on contexts and substitutions.
These two are usually combined: the second kind (called the 'syntactic category') is the base of a fibration whose fibers are of the first kind
Matteo Capucci (he/him) (Jun 26 2021 at 11:05):The two things get combined by constructions like the tripos-to-topos construction, which build a category whose internal logic is the one expressed by the fibration
Mike Shulman (Jun 26 2021 at 15:09):I don't think it has anything to do with fibrations. You can use either style in either the base or the fibers of a fibration.
Mike Shulman (Jun 26 2021 at 15:19):I also don't think it has anything to do with namelessness of syntax. You could use either style with any kind of variables (named, de Bruijn, locally nameless, ...).
Mike Shulman (Jun 26 2021 at 15:21):The problem with your first style is that it doesn't correspond very well to syntax. In syntax we have contexts, so the more direct way of interpreting syntax into a category is to have the contexts correspond to something in the category. What your first style essentially does is to implicitly take the product of all the types in a context to make them into one type. So the contexts are still really being interpreted as objects, it's just that there's an extra level of indirection.
Mike Shulman (Jun 26 2021 at 15:22):There's a third style, which I prefer over either one, which is to take semantics as occurring in a multicategory. Then you can interpret types as objects and still have something to send the contexts to without implicitly taking products: the list of types in a context corresponds to the list of objects in the domain of a morphism in a multicategory.
Mike Shulman (Jun 26 2021 at 15:23):This also has the advantage that the rules of type theory for connectives often correspond more directly to the universal properties of the corresponding objects in a multicategory.
Mike Shulman (Jun 26 2021 at 15:24):The issue with dependent type theory is that contexts are much more complicated, with a lot more structure, because some types in the context can depend on earlier types in the context. So it's hard to get away without interpreting them as something in the semantics.
Mike Shulman (Jun 26 2021 at 15:28):The most common way to interpret dependent type theory is in a categorical structure that has two kinds of "objects", one that's used to represent contexts and one that's used to represet types. Since types can be dependent on contexts, the type-objects occur in a fibration over the category of context-objects. This is a "category with families" or "comprehension category" (and lots of other names). So this is really more of a mix of your two styles. (In fact, even for simple type theory the contexts-as-objects approach is arguably mixing the styles as well, because the types also get interpreted as objects, and it doesn't necessarily need to be the same class of objects; it could be a category with families in which the type-objects are constant over the context-objects.)
Mike Shulman (Jun 26 2021 at 15:30):There is also a more "multicategorical" approach to the semantics of dependent type theory in which "contexts" are not just a separate class of objects, but really are "lists of types" just as they are in syntax. But it's more complicated because of dependency: you can't first specify a collection of type-objects and then just say the contexts are lists of them, since the type-objects may depend on some context, i.e. list of prior type-objects. So the "contexts" still have to occur as "things" in the semantics, but the rules specify that each of them is built up in a unique way as a list of types. This is called a "contextual category".
Fawzi Hreiki (Jun 26 2021 at 15:34):Say you're taking the multicategorical approach to algebraic or predicate theories. How do you define the notion of a model then? Because usually a model is a structure preserving functor from the syntactic category to the background category (e.g. Sets).
Fawzi Hreiki (Jun 26 2021 at 15:34):Do you need to pass to the free finite-product category on the multicategory?
Mike Shulman (Jun 26 2021 at 15:36):A model is a structure-preserving functor from the syntactic multicategory to the background multicategory.
Mike Shulman (Jun 26 2021 at 15:37):If your semantic category like Set is a monoidal category, you pass to its underlying multicategory.
Xuanrui Qi (Jun 27 2021 at 18:58):Hm, I have a follow-up question about contexts. Can't we just "work only with closed types and terms", as the naive types-as-objects approach would suggest? What would be the problem with this approach?
Mike Shulman (Jun 27 2021 at 21:09):Well, types are defined inductively, and the induction passes through open ones in the process of constructing closed ones. So you can't expect to define something like an interpretation function recursively over only closed types, since closed types aren't inductively defined all by themselves. It's possible you could play some tricky games to get around this, but I expect probably any resulting simplification would be outweighed by the extra complication of the trickery.
Mike Shulman (Jun 27 2021 at 21:10):I really think it's better to do things one step at a time: first construct a semantics that closely matches the behavior of syntax, like a multicategory or a category-with-families, then show how the "natural" categorical semantics can be massaged into the form of syntax-like semantics.