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.
There is now an extremely stubby stub at stack semantics.
Thanks! When I get around to revising that paper this fall, I’ll try to write some about it on the nLab too.
Don’t forget to explain in the entry why its called stack semantics.
I am wondering if we cannot give a better Idea-section in the entry stack semantics. The current idea section sounds very complicated and mysterious to the uninitiated, and it emphasizes the problem to be solved over the nature of the actual solution that is the page’s actual topic. If you see what I mean. (?)
Let me know if I am wrong about the following: my impression is that the simple conceptual idea behind “stack semantics” is clearest if we think not about toposes but about -toposes: then that simple idea is
Use the object-classifier groupoid object and in fact refine it to the object classifier category object.
Right?
For completeness and in case it is not clear what I mean:
the (-small) object classifier is the thing that classifies the core of the self-indexing/codomain fibration
The starting point of the “stack semantics” thing is – unless I am missing something – essentially the idea that we pass to something that classifies in fact all of .
That thing should be a category object in the -topos .
And that should — shouldn’t it? – start out looking like this:
first, the object classifier we may suggestively write as a “complete Segal groupoid object” as
which by univalence I can write more suggestively as
and looking at this makes us want to (doesn’t it?) say that the “stack semantics classifier” or whatever we call it, is a complete Segal category object that starts out looking as
where the object of morphisms is the function type regarded as a -dependent type.
Ahm, not sure, would be just grateful about some chat about this.
Thanks for bringing this up. I’ll try to write something coherent about how I think about stack semantics now (which isn’t exactly how I thought about it at first), either here or at the entry.
Just an idle thought, only partly related:
if we define a simplicial object in low degree type theoretically by proceeding as
then when interpreted in a type-theoretic model category this comes out as a Reedy fibrant+cofibrant (truncated) simplicial diagram: the fibrancy condition on the matching morphisms is the very interpretation of the above dependent types.
Of course this is still not a full simplicial diagram, because it stops when I stop typing the above lines. But at least the coherence is taken care of to the given degree. For instance the correct maps between two such objects will have the evident naive formulation.
Just a thought.
this comes out as a Reedy fibrant+cofibrant (truncated) simplicial diagram
Yes, that’s the basic idea of my paper on univalence for inverse diagrams. But you can only get semi-simplicial objects this way, as far as I can tell; the degeneracies are a problem.
I see. So now it’s out that I hadn’t read your article carefully. :-/ Actually I did, but got distrated somewhere in the middle.
But I see it now.
Hi Mike,
another idle thought:
in lowest degree choosing the degeneracy map means equipping with the structure of an algebra over the endofunctor whose initial algebra is the identity type .
This sounds vaguely suggestive of something. But I am not sure of what ;-) Maybe somehow the addition of degenracies to a semisimplicial Reedy fibrant diagram can usefully be related to higher inductive types of sorts?
Here is one more thought (all of this just elementary toying around, I am well aware, but I feel like chatting about it anyway):
The recursion principle for identity types is closely related to the complete-Segal condition.
Sorry for the boldface, but when this occured to me I found it charming.
This will be trivially evident for you, but let me just spell it out anyway, also in case some bystander is listening and wondering about it:
So the recursion principle for identity types says that if the category-object-to be
has an identity-assigning map , then this factors through the path object of by a compatible morphism
But this is precisely the morphism that the complete-Segal condition will be a condition on: namely it will say that this morphism exhibits the homotopy-full inclusion of elements in that are equivalences.
Yeah, hm, this is just a variant of the univalence story. Hm…
Hm, right. Isn’t that true:
univalence is equivalently the first degree component in the complete-Segal condition on “the homotopy stack semantics” (the classifier of the codomain fibration). ?!
Yes, I think that’s right; univalence means that when you build the internal full subcategory corresponding to the universal dependent type , its nerve is a complete Segal object.
That is nice. I don’t think I’ve seen it stated in that way before…
Okay, I completely replaced the stub at stack semantics with a different idea section and a long description of how I see stack-semantics relating to object classifier and universes. What do you think?
Thanks, yes, I like that.
Just to be sure: when you say “stack semantics” you are primarily referring to universe enlargement, and only secondarily to the issue of having a groupoidal or a categorical universe. Is that right?
Might it make sense to say this right in the first sentence? Something like “Stack semantics is an extension of the internal logic […] essentially corresponding to a universe enlargement.” ?
No, I use “stack semantics” to refer to both at once.
Okay, I see. This could maybe be clearer in the entry. Because where it currently says
[…] should be regarded as a category, or at worst as a groupoid […]
I got away with thinking that the difference is just meant to be a matter of taste.
How about if we put that right into the very first sentence and expand what is currently there to something like this:
The stack semantics is an extension of the internal logic a category (or higher category) C by extending an internal universe to an external universe category object, which allows us to talk about, and quantify over, objects of C. (Such quantification is sometimes called “unbounded” quantification.)
?
By the way, what motivated my questions here is that I wanted to understand what terminology you would prefer for the internal but categorical case, that where we refine the internal universe “Segal-complete groupoid object” (hence equivalently just an object) to an internal category object.
Wait, I think I misunderstood your “or”. When you said
the issue of having a groupoidal or a categorical universe
I thought you meant the issue of having (1) a groupoidal or categorical universe versus the alternative option (2) of having a set-like universe. I meant that stack semantics means that the universe is groupoidal or categorical, i.e. not set-like.
But I guess you were asking whether stack semantics means that the universe is groupoidal, or whether it means that it is categorical? It doesn’t really matter; I tried to explain that in the entry. Because the non-invertible morphisms are modeled in the internal language using exponential objects, it doesn’t matter whether the “universe” is a groupoid or a category. You get exactly the same Kripke-Joyal style semantics, which is the original meaning of “stack semantics”.
But I guess you were asking whether stack semantics means that the universe is groupoidal, or whether it means that it is categorical?
Yes! Mainly I am trying to figure out if when I want to express “consider the internal category object corresponding to the small self-indexing” it would be consistent with your use of terminology to say “consider the stack semantics”.
But I gather the answer to that is “No”, since, as you say, the choice of either universe groupoid or universe category does not affect the logic / semantics.
Okay, good. If you still have a second: can we find a proposal for a good technical term for the internal category object that should start out as
?
How about “the canonical internal base topos”? Or just “the internal base topos”?
Correct, that is not how I would use “stack semantics”.
I guess “the internal full subcategory on the object classifier” is too long? I’m not immediately enamored of “base topos” because we’re only talking inside of a single topos here, there is no base vs. other.
How about the “internal self-indexing”?
Fix broken link. Some programmatic change had turned what may have been an en-dash in the link to Mitchell-Bénabou language to a question mark.
1 to 21 of 21