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.
in another entry I want to be able to point to context extension, so I created a brief entry
Slight expansion.
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.
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))$.
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.)
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?
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.)
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.
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
to
and to
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?
I’ve never heard any type theorist refer to an arbitrary context morphism as an “extension”.
1 to 10 of 10