Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
[ forwarding old discussion that used to be at context ]
The following discussion was initiated by a previous version of the above entry which referred to “cartesian multicategories” rather than finitely complete categories.
+–{: .query} Mike: What is a cartesian multicategory, and how do I interpret the theory of groups in one? I can guess what it would mean for a multicategory to have finite products. But if I interpret the multiplication as a morphism $G\times G\to G$, then I’m not using the multicategory structure, so we might as well just be in a category with finite products. And if I interpret the multiplication as a multimap $(G;G)\to G$, then I don’t know how to interpret the axiom of inverses, since there is no ’diagonal’ $G\to (G;G)$ or ’projection’ $G\to ()$.
Toby: I'm not sure why I generalised to cartesian multicategories, but it is a nontrivial generalisation. (Perhaps I was planning to show, as an example, how the category of contexts of the canonical language of a multicategory becomes a monoidal category or something, but that doesn't seem very useful. Maybe I was just doing unnecessary generality, but of course it's not the absolutely most general situation either.)
Anyway … you make a multicategory cartesian much as you might make a monoidal category cartesian by equipping it with appropriate diagonal and projection maps. The problem is that, while $G \to G \otimes G$ and $G \to 1$ make sense in a monoidal category, they don't make sense in a multicategory. But you fix this by filtering through Yoneda.
So a cartesian multicategory is a multicategory equipped with, for each object $G$ and object $X$, a function $\check{G}^*_X\colon hom(G;X) \leftarrow hom(G,G;X)$ and a function $\hat{G}^*_X\colon hom(G;X) \leftarrow hom(;X)$. (H'm, my commas and semicolons are the opposite of yours; no matter.) Then these are subject to various coherence requirements that should be obvious.
Mike: Okay, I see. Though I’m guessing you wanted those natural transformations to go the other way. Are there any naturally occurring examples of cartesian multicategories that are not cartesian monoidal categories? Even if there are, I’m inclined to regard the concept as esoteric enough that it would be clearer to just say “category with finite products” in this introductory article.
Toby: Ah, the curse of contravariance! Going over the whole introduction again, I think that I understand why I mentioned multicategories, which is that a context like $a\colon G, b\colon G$ is more naturally interpreted as a list $(G, G)$ of objects than as a single object $G \times G$. But if we were really to go in that direction, then we'd also want the context $a\colon G, b\colon G, (a b)^2 = a^2 b^2$ to be interpreted as a list in its own right rather than an actual subobject of $G \times G$, and that's going a bit far … farther than I understand clearly, in any case. So in fact I let the category be finitely complete so that we could form that subobject (referred to only via the link to internal logic, of course).
Mike: True. Is a one-object cartesian multicategory the same as a Lawvere theory, aka an operad relative to the theory of categories with finite products? If so, then perhaps the relevant place to work is a multicategory relative to the theory of lex categories? Can that be generalized to stronger logics?
Toby: Yes, that seems to be right, that Lawvere theories are equivalent to one-object cartesian multicategories (cartesian multimonoids? cartesian operads?). So this should work.
Of course, one thing that contexts do is to form an honest category even if you start with a multicategory. So here we're trying to go backwards and see what bare-bones starting point could lead to the same category of contexts of the equational theory of a group. =–
I have expanded at context.
For instance I have
Added an Examples-section Substitution and introduction of a single term
added a pointer to Paul Taylor’s “Foundations for computable topology”.
Seeing that old discussion reminds me that someone should write the page cartesian multicategory.
I realize that we have a bit of a mess concerning the material behind the links category of contexts and syntactic category.
These should be “the same”, right? Maybe somehow the matieral wants to be re-organized.
P.S. This arises in my little subquest of isolating a coherent statement of the alleged adjunction between “type theories” and “categories”. I am thinking maybe we should create a page titled the adjunction between type theories and categories. I just wish I knew where to point to and say: “It is stated on page x of book Y.” I guess Paul Taylor’s book contains part of the answer…
Lambek and Scott [Introduction to higher order categorical logic] give an adjunction between type theories and toposes with “canonical subobjects”: Part II, Theorem 15.4. There’s also an equivalence between simply typed lambda-calculi and cartesian closed categories with weak NNOs: Part I, Theorem 11.3.
Mike, why do you write that using a cartesian multicategory doesn’t require an explicit use of contexts?
Perhaps category of contexts should redirect to syntactic category already?, even though it would still say to look at context for now.
@Toby #6: What I was thinking is that in a (non-dependent) type theory, you can build a syntactic cartesian multicategory whose objects are types, rather than a syntactic category whose objects are contexts. The type theory itself still has contexts, but they don’t need to be incarnated as objects in the category theory. Is that right?
I realize that we have a bit of a mess concerning the material behind the links category of contexts and syntactic category.
For me the question arises what additional information we are provided by the names ”syntactic category” or ”category of context” - for a category theorist these are just type theories.
Saying these notions are the same amounts to propose that there is just one reasonable way to assign to a type theory (in italics) in the logician’s notation a type theory (a category).
To me ”category of contexts” (where the objects are contexts) sounds more specific than ”syntactic category” where one could expect the objects to be some other class of syntactic constructs from the related type theory (for example types). Hence for the examples I heard of ”category of contexts” would be the more precise term since it is more descriptive. However such periphrasis where we distinguish between ”something” and ”something seen as a category” is not done in the case of e.g. ”poset”.
In no case - I think - we should keep two entries where the one is just a terminological variation of the other.
There is a term for a p(r)oset seen as a category, and we do have a separate page on it: thin category.
Ok, in this case it is explained in the articles what the differences between these notions are. Maybe we can achieve such clarity in the other case, too! I wrote this since I often heard people talk about posets meaning thin categories so I thought it is convention to do so. In this regard the example of posets / thin categories was not that fortunate.
However it was not the entry type theory whose autonomous existence I indicated to reconsider…
Then whose autonomous existence do you want to reconsider?
One advantage of the term “syntactic category” over “category of contexts” is that it encompasses other versions of the construction where the objects are not contexts. For instance, there is the syntactic cartesian multicategory mentioned above, whose objects are types. In a non-dependent type theory with product types, or a dependent type theory with dependent sum types (in both cases assuming judgmental $\eta$-conversion), we can build an equivalent syntactic category whose objects are types, rather than contexts. In a type theory where propositions are not identified with particular types (such as the presentation of regular/coherent/geometric theories in the Elephant), the objects of the syntactic category are generally taken to be propositions-in-context. In a logic lacking conjunction, they ought instead to be finite lists of propositions in context. But these are all clearly variations on a single theme, so it is nice to have a single name for them all.
Regardless, most of the current content of the page context would really be more appropriate at a page called either “category of contexts” or “syntactic category”, whichever we settle on.
I vote for syntactic category. The page context should mostly just explain what a context is. It can also explain an interpretation of one context in another, thereby defining the category of contexts, but then it would link to syntactic category.
Lambek and Scott [Introduction to higher order categorical logic] give an adjunction between type theories and toposes with “canonical subobjects”: Part II, Theorem 15.4.
Thanks!! Finally a reference.
I need to be taking care of something else until tomorrow evening. But then I will try to come back to this. Thanks again.
Then whose autonomous existence do you want to reconsider?
As I said above, every entry where my proposal ”In no case - I think - we should keep two entries where the one is just a terminological variation of the other.” applies. But in light of what Mike said above this does not apply here.
I vote for syntactic category
Me, too. Because of the reasons Toby mentions and since this term is suggested by the complementary notion of semantic category (display category), practical foundations section 8.3.
One advantage of the term “syntactic category” over “category of contexts” is that it encompasses other versions of the construction where the objects are not contexts. For instance…
It would be nice to list those examples there
re #5 and #15:
Ah, and not to forget (I knew this and then DID forget about it): of course Seely proves the equivalence of categories
$MLDependentTypeTheories \simeq LocallyCartesianClosedCategories$in Locally cartesian closed categories and type theory (pdf)
But, Zhen Lin, of course I found this via your reference, because Scott and Lambek in their preface mention this! :-)
I have moved the discussion of syntactic categories from context to syntactic category. Should update more links and stuff, but I have to run right now.
What would everyone think about trying to use systematically the notations
?
I like $Lang$. The nice thing about $Con$ is that we usually name a category after its objects, and the objects of the syntactic category are contexts.
But one of the arguments for saying “syntactic category” rather than “category of contexts” is that the objects of the syntactic category are not always contexts (see #13 above).
That’s a fair point. But when people say ‘proposition in context’, they’re using a restrictive interpretation of ‘context’ in which a context consists solely of a list of free variables and associated types. If you add a list of propositional hypotheses to such, then the result is still a context: a list of assumptions to be made when making an assertion. The examples from the theory of a group include such.
Okay… and I suppose you would say that types are also a particular sort of context?
Of course a type is a special case of a context (a context with one free variable and no propositional hypotheses), but if you’re talking about using a multicategory whose objects are types, then this is a multicategory of types rather than a category of contexts, since a context in general is a list of such objects. So the objects of a syntactic multicategory are types, while the objects of a syntactic category are contexts. On the other hand, if you’re talking about the strong theories in which every context is equivalent to a context with one free variable and no propositional hypotheses, then types and contexts are essentially the same thing, so then we do have a syntactic category whose objects are types, which one can equally well view as contexts.
In either case, the category of contexts as syntactic category is the basic notion; a category of types or a multicategory of types are variations on this theme (and ones that can only be used for certain kinds of theories).
Okay, I guess you have a point, and I’m tired of this discussion. (-: $Con(T)$ it is, at least in the cases when its objects are contexts. In the other cases we can write $Typ(T)$ or something.
OK. But if, after all of this tiring discussion, you still want to call it $Syn(T)$ (for whatever reason), I won’t change it (or argue that it should be changed, etc). That’s because you’re the one currently working on it, and it’s a perfectly reasonable name. I just gave my opinion.
I like $Syn(T)$. If the name is accepted to involve syntactic then the notation should as well.
I do see the point that for better or for worse, we generally name categories after their objects, and in the vast majority of cases the objects of the syntactic category are contexts.
I would like to be able to point lay-people to context for an explanation of how to think of contexts and their interpretation in type theory and in particular in homotopy type theory. I found the entry to be in a very preliminary state. So I have edited a bit, brought a tiny bit of structure into it and added some further pointers. But I don’t really have time to do more now.
I have cross-linked (here) with the new entry split context and added explicit pointers to real-cohesive homotopy type theory and linear homotopy type theory.
1 to 31 of 31