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.
Mike,
have you at all thought about doing “stable homotopy type theory” in analogy to your proposal for doing “directed homotopy type theory”?
So I am thinking of axiomatizing the internal homotopy-logic of the “tower -topos” and then internally characterizing in there the spectrum objects.
Just an idea. I haven’t thought about it in any detail. I just thought I’d check if you had. :-)
Hmm, no, I haven’t thought of that. That wouldn’t be quite the right topos; you need maps , not . But it’s an interesting idea!
Right, after posting this yesterday night I went to bed. And then in bed I thought “Aw, I should have typed instead of ” (as in Def 8.1 in Stable Infinity-Categories ). But then I didn’t want to get up again ;-)
Can we look for any old variety of homotopy type theory? What about one to correspond to categories with duals?
So far the strategy that we are talking about potentially works for structures that can be formulated as certain objects with certain properties in some topos.
Because the HoTT language takes place in an -topos.
The strategy with the directed homotopy type theory and the stable homotopy type theory was the following: in these cases either -categories or spectrum objects internal to an -topos can be characterized as special objects in a diagram -topos for some diagram category (in the first case , in the second ). Since is again an -topos, there is a chance that we can add axioms to the homotopy type theory language such as to characterize this, from the inside. And then we have to think about how to use these axioms to describe the actual objects that we want (internal -categories or internal spectra).
For categories with duals I suppose one would first go to the context of , characterize internal -categories there, and then see if we can characterize duals on these.
On the other hand, if we want to describe -categories with duals and adjoints, say because we want to describe topological quantum field theory in homotopy type theory, then it might be an idea to go via a description of such beasts that is not modeled on simplices, but that constructs these structures more directly. I kept wondering about that:
At (infinity,n)-category with adjoints is referenced an approach that realizes -categories with adjoints as -stacks on a certain category of iterated submersions of smooth manifolds with embeddings (and a bit more stuff).
Do we have a chance of saying that internally? Is it remarkable that -categories can be modeled as -stacks on (iterated submersions of) smooth manifolds, and that at the same time cohesion knows about smooth manifolds, in a way?
I don’t know. But I have been wondering about this.
Interesting. I wonder if that big conversation on fundamental n-categories with duals of stratified spaces can fit in somewhere.
Here’s a question: is the subcategory of spectra in an exponential ideal? If not, then it can’t be extended to a reflective subfibration, which would make it hard to express internally.
I wrote:
is the subcategory of spectra in an exponential ideal?
The answer to this must be “no”, because an exponential ideal in a cartesian closed category is itself cartesian closed, but the category of spectra is not cartesian closed.
1 to 8 of 8