Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Discussion 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).
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeSep 22nd 2012

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

    • CommentRowNumber2.
    • CommentAuthorTobyBartels
    • CommentTimeSep 23rd 2012

    Slight expansion.

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeSep 23rd 2012

    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.

    • CommentRowNumber4.
    • CommentAuthorTobyBartels
    • CommentTimeSep 23rd 2012

    The display map is a projection map from a product only if the type TT of the new variable is a type in the empty context. But in general, TT 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/ΓDisp/\Gamma, the subcategory of the slice category Ctxt/Γ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:T)(x\colon T); then Γ×Γ\Gamma \times \Gamma is (x:T,y:T)(x\colon T, y\colon T). Then Γ\Gamma itself is (isomorphic to) the extended context (x:T,y:T,p:Id(x,y))(x\colon T, y\colon T, p\colon Id(x,y)).

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeSep 23rd 2012
    • (edited Sep 23rd 2012)

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

    • CommentRowNumber6.
    • CommentAuthorTobyBartels
    • CommentTimeSep 23rd 2012

    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?

    • CommentRowNumber7.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 2nd 2016

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

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeMar 2nd 2016

    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.

    • CommentRowNumber9.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 4th 2016

    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

    • Γ=x 0:A 0,x 1:A 1(x 0),x 2:A 2(x 0,x 1),x n:A n(x 0,,x n1)\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

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

    and to

    • Γ,x k=a(x 1,,x n):A k(x 0,,x k1)\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, Γ(a(x 1,,x n)/x k)\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?

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeMar 4th 2016

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