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*.

added section about split contexts in type theories.

Anonymous

]]>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 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 like $Syn(T)$. If the name is accepted to involve syntactic then the notation should as well.

]]>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.

]]>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.

]]>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… and I suppose you would say that types are also a particular sort of context?

]]>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.

]]>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).

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.

]]>What would everyone think about trying to use systematically the notations

- $Syn$ rather than $Con$ for the syntactic category (since we are calling the page that rather than “category of contexts”), and
- $Lang$ rather than $Lan$ for the internal logic/language (since $Lan$ always makes me think of left Kan extensions)

?

]]>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.

]]>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

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! :-)

]]>Then whose autonomous existence

doyou 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

]]>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.

]]>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.

]]>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.

]]>Then whose autonomous existence *do* you want to reconsider?

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…

]]>There *is* a term for a p(r)oset seen as a category, and we *do* have a separate page on it: thin category.

I realize that we have a bit of a mess concerning the material behind the links

category of contextsandsyntactic 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.

]]>@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?

]]>