Not signed in

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

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeSep 22nd 2012
   • PermaLink
   Author: Urs
   Format: MarkdownItexin another entry I want to be able to point to _[[context extension]]_, so I created a brief entry

   in another entry I want to be able to point to context extension, so I created a brief entry

2. • CommentRowNumber2.
   • CommentAuthorTobyBartels
   • CommentTimeSep 23rd 2012
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexSlight expansion.

   Slight expansion.

3. • CommentRowNumber3.
   • CommentAuthorUrs
   • CommentTimeSep 23rd 2012
   • PermaLink
   Author: Urs
   Format: MarkdownItexThanks. One question: I am not sure how to read the last paragraph on display maps. What it says there seems to come down to saying that display maps are precisely only the projection maps. But that's only one choice of class of display maps, and not actually an interesting one. Or maybe I am misreading that paragraph.

   Thanks.

   One question: I am not sure how to read the last paragraph on display maps. What it says there seems to come down to saying that display maps are precisely only the projection maps. But that’s only one choice of class of display maps, and not actually an interesting one. Or maybe I am misreading that paragraph.

4. • CommentRowNumber4.
   • CommentAuthorTobyBartels
   • CommentTimeSep 23rd 2012
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexThe display map is a projection map from a product only if the type $T$ of the new variable is a type in the empty context. But in general, $T$ could be any type in the unextended context $\Gamma$. So really we are only claiming that every display map to $\Gamma$ is a product projection in the slice category over $\Gamma$, but of course every map to $\Gamma$ is that. (And a display map to $\Gamma$ is *precisely* a product projection in $Disp/\Gamma$, the subcategory of the slice category $Ctxt/\Gamma$ generated by the display maps; which is trivial.) Or from the other direction: If we have appropriate identity types, then every map is a display map, and in particular the diagonal $\Gamma \to \Gamma \times \Gamma$ is one, so how is this given by a context extension? For simplicity, suppose that $\Gamma$ is just one free variable, so of the form $(x\colon T)$; then $\Gamma \times \Gamma$ is $(x\colon T, y\colon T)$. Then $\Gamma$ itself is (isomorphic to) the extended context $(x\colon T, y\colon T, p\colon Id(x,y))$.

   The display map is a projection map from a product only if the type $T$ of the new variable is a type in the empty context. But in general, $T$ could be any type in the unextended context $\Gamma$. So really we are only claiming that every display map to $\Gamma$ is a product projection in the slice category over $\Gamma$, but of course every map to $\Gamma$ is that. (And a display map to $\Gamma$ is precisely a product projection in $Disp/\Gamma$, the subcategory of the slice category $Ctxt/\Gamma$ generated by the display maps; which is trivial.)

   Or from the other direction: If we have appropriate identity types, then every map is a display map, and in particular the diagonal $\Gamma \to \Gamma \times \Gamma$ is one, so how is this given by a context extension? For simplicity, suppose that $\Gamma$ is just one free variable, so of the form $(x\colon T)$; then $\Gamma \times \Gamma$ is $(x\colon T, y\colon T)$. Then $\Gamma$ itself is (isomorphic to) the extended context $(x\colon T, y\colon T, p\colon Id(x,y))$.

5. • CommentRowNumber5.
   • CommentAuthorUrs
   • CommentTimeSep 23rd 2012
   • (edited Sep 23rd 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexThanks, Toby. I appreciate the details. But I still don't quite follow. So as you say in your first paragraph, if "product" means "product in the slice" then every every morphism to $\Gamma$ is a product projection. But let's step back a bit: by the discussion at [[display map]] in full generality the class of diplays maps is a _choice_. It could be every map. It could be something very restriutive. Depends on the ambient setup and on which type theory is supposed to be interpreted. Could you maybe just spell out for me in a few more words what that last paragraph in the entry is saying? I am likely just being dense here. But I am sure if you just expand a little I'll get it. (Also, you'll see that I gave the entry subsections and reorganized slightly. See what you think.)

   Thanks, Toby. I appreciate the details. But I still don’t quite follow.

   So as you say in your first paragraph, if “product” means “product in the slice” then every every morphism to $\Gamma$ is a product projection.

   But let’s step back a bit: by the discussion at display map in full generality the class of diplays maps is a choice. It could be every map. It could be something very restriutive. Depends on the ambient setup and on which type theory is supposed to be interpreted.

   Could you maybe just spell out for me in a few more words what that last paragraph in the entry is saying? I am likely just being dense here. But I am sure if you just expand a little I’ll get it.

   (Also, you’ll see that I gave the entry subsections and reorganized slightly. See what you think.)

6. • CommentRowNumber6.
   • CommentAuthorTobyBartels
   • CommentTimeSep 23rd 2012
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexThe organisation is nice. I don't understand what you want in the final paragraph. Is it that the words are unclear? Or that it still seems to imply something wrong?

   The organisation is nice.

   I don’t understand what you want in the final paragraph. Is it that the words are unclear? Or that it still seems to imply something wrong?

7. • CommentRowNumber7.
   • CommentAuthorDavid_Corfield
   • CommentTimeMar 2nd 2016
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexI guess whatever that was being discussed in #5 and #6 never got resolved. Anything to add over three years later? Also can we not resolve this uncertainty: >(This might not actually be true in all type theories, or maybe it should be taken as the definition of ‘display morphism’; I'm not sure.)

   I guess whatever that was being discussed in #5 and #6 never got resolved. Anything to add over three years later?

   Also can we not resolve this uncertainty:

   (This might not actually be true in all type theories, or maybe it should be taken as the definition of ‘display morphism’; I’m not sure.)

8. • CommentRowNumber8.
   • CommentAuthorMike Shulman
   • CommentTimeMar 2nd 2016
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI think the confusion is that Toby was thinking and writing syntactically, while Urs was thinking semantically. The paragraph in question says "in the category of contexts", so it is not talking about the general concept of "display map" but rather about the particular display maps with which the category of contexts of a type theory is canonically equipped. Regarding the parenthetical, I would be inclined to take that as the definition of "display map" (meaning, the definition of the *canonical* class of display maps in the category of contexts). Although there is some ambiguity as to whether a "context extension" here means only an extension by *one* variable or possibly an extension by many variables at once.

   I think the confusion is that Toby was thinking and writing syntactically, while Urs was thinking semantically. The paragraph in question says “in the category of contexts”, so it is not talking about the general concept of “display map” but rather about the particular display maps with which the category of contexts of a type theory is canonically equipped.

   Regarding the parenthetical, I would be inclined to take that as the definition of “display map” (meaning, the definition of the canonical class of display maps in the category of contexts). Although there is some ambiguity as to whether a “context extension” here means only an extension by one variable or possibly an extension by many variables at once.

9. • CommentRowNumber9.
   • CommentAuthorDavid_Corfield
   • CommentTimeMar 4th 2016
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexRanta uses 'context extension' in the general sense of an interpretation, a morphism in the category of contexts (see [[syntactic category]]), sec 7.1 of Type-Theoretic Grammar. You can see the motivation for this from his observation that interpretation includes two basic cases, namely the change from * $\Gamma \;=\; x_0:A_0,\; x_1:A_1(x_0),\; x_2:A_2(x_0,x_1),\;\dots x_n:A_n(x_0,\dots,x_{n-1})$ to * $\Gamma, x: A(x_0,\dots,x_{n})$ and to * $\Gamma, x_k = a(x_1, \dots,x_n): A_k(x_0,\dots,x_{k-1})$. It might seem strange to call the latter an extension, as he notes, since the new context is shorter, $\Gamma(a(x_1, \dots,x_n)/x_k)$, but it is an extension of our knowledge. Apparently, Martin-Löf had said this in lectures on choice sequences in 1990-91. So Is that standard to restrict context extension to the first of these?

   Ranta uses ’context extension’ in the general sense of an interpretation, a morphism in the category of contexts (see syntactic category), sec 7.1 of Type-Theoretic Grammar. You can see the motivation for this from his observation that interpretation includes two basic cases, namely the change from

   • $\Gamma \;=\; x_0:A_0,\; x_1:A_1(x_0),\; x_2:A_2(x_0,x_1),\;\dots x_n:A_n(x_0,\dots,x_{n-1})$

   to

   • $\Gamma, x: A(x_0,\dots,x_{n})$

   and to

   • $\Gamma, x_k = a(x_1, \dots,x_n): A_k(x_0,\dots,x_{k-1})$.

   It might seem strange to call the latter an extension, as he notes, since the new context is shorter, $\Gamma(a(x_1, \dots,x_n)/x_k)$, but it is an extension of our knowledge.

   Apparently, Martin-Löf had said this in lectures on choice sequences in 1990-91.

   So Is that standard to restrict context extension to the first of these?

10. • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeMar 4th 2016
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexI've never heard any type theorist refer to an arbitrary context morphism as an "extension".

    I’ve never heard any type theorist refer to an arbitrary context morphism as an “extension”.