Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

nLab > Latest Changes: context

Bottom of Page

1 to 31 of 31

- CommentRowNumber1.
- CommentAuthorUrs
- CommentTimeMay 9th 2012
- PermaLink
Author: Urs
Format: MarkdownItex[ 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 Shulman|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 Shulman|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 Shulman|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. =--

[ 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. =–
- CommentRowNumber2.
- CommentAuthorUrs
- CommentTimeMay 9th 2012
- PermaLink
Author: Urs
Format: MarkdownItexI have expanded at _[[context]]_. For instance I have 1. Added an Examples-section _[Substitution and introduction of a single term](http://ncatlab.org/nlab/show/context#SubstitutionAndIntroductionOfTerm)_ 1. added a pointer to Paul Taylor's "Foundations for computable topology".
I have expanded at context.

For instance I have
1. Added an Examples-section Substitution and introduction of a single term
2. added a pointer to Paul Taylor’s “Foundations for computable topology”.
- CommentRowNumber3.
- CommentAuthorMike Shulman
- CommentTimeMay 9th 2012
- PermaLink
Author: Mike Shulman
Format: MarkdownItexSeeing that old discussion reminds me that someone should write the page [[cartesian multicategory]].

Seeing that old discussion reminds me that someone should write the page cartesian multicategory.
- CommentRowNumber4.
- CommentAuthorUrs
- CommentTimeMay 12th 2012
- (edited May 12th 2012)
- PermaLink
Author: Urs
Format: MarkdownItexI 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...

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…
- CommentRowNumber5.
- CommentAuthorZhen Lin
- CommentTimeMay 12th 2012
- PermaLink
Author: Zhen Lin
Format: MarkdownItexLambek 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.

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.
- CommentRowNumber6.
- CommentAuthorTobyBartels
- CommentTimeMay 13th 2012
- (edited May 13th 2012)
- PermaLink
Author: TobyBartels
Format: MarkdownItexMike, why do you write that using a cartesian multicategory doesn't require an explicit use of contexts?

Mike, why do you write that using a cartesian multicategory doesn’t require an explicit use of contexts?
- CommentRowNumber7.
- CommentAuthorTobyBartels
- CommentTimeMay 13th 2012
- PermaLink
Author: TobyBartels
Format: MarkdownItexPerhaps [[category of contexts]] should redirect to [[syntactic category]] already?, even though it would still say to look at [[context]] for now.

Perhaps category of contexts should redirect to syntactic category already?, even though it would still say to look at context for now.
- CommentRowNumber8.
- CommentAuthorMike Shulman
- CommentTimeMay 13th 2012
- PermaLink
Author: Mike Shulman
Format: MarkdownItex@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?

@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?
- CommentRowNumber9.
- CommentAuthorStephan A Spahn
- CommentTimeMay 13th 2012
- (edited May 13th 2012)
- PermaLink
Author: Stephan A Spahn
Format: MarkdownItex> 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.

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.
- CommentRowNumber10.
- CommentAuthorTobyBartels
- CommentTimeMay 13th 2012
- PermaLink
Author: TobyBartels
Format: MarkdownItexThere *is* a term for a p(r)oset seen as a category, and we *do* have a separate page on it: [[thin category]].

There is a term for a p(r)oset seen as a category, and we do have a separate page on it: thin category.
- CommentRowNumber11.
- CommentAuthorStephan A Spahn
- CommentTimeMay 13th 2012
- PermaLink
Author: Stephan A Spahn
Format: MarkdownItexOk, 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...

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…
- CommentRowNumber12.
- CommentAuthorTobyBartels
- CommentTimeMay 14th 2012
- PermaLink
Author: TobyBartels
Format: MarkdownItexThen whose autonomous existence *do* you want to reconsider?

Then whose autonomous existence do you want to reconsider?
- CommentRowNumber13.
- CommentAuthorMike Shulman
- CommentTimeMay 14th 2012
- PermaLink
Author: Mike Shulman
Format: MarkdownItexOne 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.

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.
- CommentRowNumber14.
- CommentAuthorTobyBartels
- CommentTimeMay 14th 2012
- PermaLink
Author: TobyBartels
Format: MarkdownItexI 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]].

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.
- CommentRowNumber15.
- CommentAuthorUrs
- CommentTimeMay 14th 2012
- PermaLink
Author: Urs
Format: MarkdownItex> 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.

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.
- CommentRowNumber16.
- CommentAuthorStephan A Spahn
- CommentTimeMay 14th 2012
- (edited May 14th 2012)
- PermaLink
Author: Stephan A Spahn
Format: MarkdownItex> 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

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
- CommentRowNumber17.
- CommentAuthorUrs
- CommentTimeMay 15th 2012
- PermaLink
Author: Urs
Format: MarkdownItexre #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](http://www.math.mcgill.ca/rags/LCCC/LCCC.pdf)) But, Zhen Lin, of course I found this via your reference, because Scott and Lambek in their preface mention this! :-)

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! :-)
- CommentRowNumber18.
- CommentAuthorMike Shulman
- CommentTimeMay 23rd 2012
- PermaLink
Author: Mike Shulman
Format: MarkdownItexI 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.

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.
- CommentRowNumber19.
- CommentAuthorMike Shulman
- CommentTimeMay 24th 2012
- PermaLink
Author: Mike Shulman
Format: MarkdownItexWhat 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) ?
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)
?
- CommentRowNumber20.
- CommentAuthorTobyBartels
- CommentTimeMay 28th 2012
- PermaLink
Author: TobyBartels
Format: MarkdownItexI 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.

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.
- CommentRowNumber21.
- CommentAuthorMike Shulman
- CommentTimeMay 29th 2012
- PermaLink
Author: Mike Shulman
Format: MarkdownItexBut 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).

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).
- CommentRowNumber22.
- CommentAuthorTobyBartels
- CommentTimeMay 30th 2012
- (edited May 30th 2012)
- PermaLink
Author: TobyBartels
Format: MarkdownItexThat'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. [[syntactic category#group|The examples from the theory of a group]] include such.

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.
- CommentRowNumber23.
- CommentAuthorMike Shulman
- CommentTimeMay 30th 2012
- PermaLink
Author: Mike Shulman
Format: MarkdownItexOkay... and I suppose you would say that types are also a particular sort of context?

Okay… and I suppose you would say that types are also a particular sort of context?
- CommentRowNumber24.
- CommentAuthorTobyBartels
- CommentTimeJun 2nd 2012
- PermaLink
Author: TobyBartels
Format: MarkdownItexOf 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).

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).
- CommentRowNumber25.
- CommentAuthorMike Shulman
- CommentTimeJun 2nd 2012
- PermaLink
Author: Mike Shulman
Format: MarkdownItexOkay, 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.

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.
- CommentRowNumber26.
- CommentAuthorTobyBartels
- CommentTimeJun 3rd 2012
- PermaLink
Author: TobyBartels
Format: MarkdownItexOK. 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.

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.
- CommentRowNumber27.
- CommentAuthorzskoda
- CommentTimeJun 3rd 2012
- PermaLink
Author: zskoda
Format: MarkdownItexI like $Syn(T)$. If the name is accepted to involve syntactic then the notation should as well.

I like $Syn(T)$ . If the name is accepted to involve syntactic then the notation should as well.
- CommentRowNumber28.
- CommentAuthorMike Shulman
- CommentTimeJun 6th 2012
- PermaLink
Author: Mike Shulman
Format: MarkdownItexI 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 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.
- CommentRowNumber29.
- CommentAuthorUrs
- CommentTimeSep 8th 2012
- PermaLink
Author: Urs
Format: MarkdownItexI 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 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.
- CommentRowNumber30.
- CommentAuthornLab edit announcer
- CommentTimeNov 30th 2022
- PermaLink
Author: nLab edit announcer
Format: MarkdownItexadded section about split contexts in type theories. Anonymous <a href="https://ncatlab.org/nlab/revision/diff/context/44">diff</a>, <a href="https://ncatlab.org/nlab/revision/context/44">v44</a>, <a href="https://ncatlab.org/nlab/show/context">current</a>

added section about split contexts in type theories.

Anonymous

diff, v44, current
- CommentRowNumber31.
- CommentAuthorUrs
- CommentTimeDec 16th 2022
- PermaLink
Author: Urs
Format: MarkdownItexI have cross-linked ([here](https://ncatlab.org/nlab/show/context#SplitContexts)) with the new entry *[[split context]]* and added explicit pointers to *[[real-cohesive homotopy type theory]]* and *[[linear homotopy type theory]]*. <a href="https://ncatlab.org/nlab/revision/diff/context/46">diff</a>, <a href="https://ncatlab.org/nlab/revision/context/46">v46</a>, <a href="https://ncatlab.org/nlab/show/context">current</a>

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.

diff, v46, current

1 to 31 of 31

nForum

Discussion Feed

Not signed in

Site Tag Cloud

nLab > Latest Changes: context