What collections of sets are appropriate for the "HoTT: Logic of spaces" and are they models?

60 Views Asked by At

There is very nice article https://arxiv.org/abs/1703.03007 "Homotopy type theory: the logic of space" which provides mapping among 1) Types of Homotopy Type Theory; 2) objects and morphisms of some specific categories; 3) spaces.

My question is about collection of spaces into which the HoTT types/objects are mapped.

What do we know about such collections? Are there some features how can we recognize that some collection of spaces is the collection for some HoTT theory (apart from the recognition as suggested by the definition)? E.g. may we take some collection of spaces and read the topological invariants and then from this set of invariants can recognize this collection as some kind of model for HoTT theory (with some particular topological invariants?). It may be possible that such collection is model of HoTT indeed, but, of course, as with every model, inferring expression of theory in this one model is not sufficient for assering that this expression is true in the theory generally, one should be able to do this in all such collections of spaces.

And what about taking one space and generting all the remaining spaces in the collection? What are the appropriate operations and from which spaces this generation can be done (for some theory) and for which cannot?

Maybe this is HoTT model theory (if there is any) in the spaces?

Sorry for many questions in one question, but these subquestions are just hints for the general question: what do we know about collection of spaces as a model of HoTT and are there some mathematical branches / authors / important articles that are elaborating on the properties of such collections of spaces?

1

There are 1 best solutions below

0
On

It is a deep theorem (ultimately due to Shulman, but with important contributions along the way from many others such as Awodey, Cisinski, Voevodsky, etc.) that every (grothendieck) $(\infty,1)$-topos is a model of HoTT (in fact the truth is very slightly more subtle, see the references here for more details). Life is too short to write "$(\infty,1)$" all the time, so for this post I'll just write "topos" instead. This is fairly common amongst other authors as well, so be careful when reading the literature!

The primordial example is the topos of spaces. That is, the topos whose objects are topological spaces (up to homotopy), and interpreting HoTT in this topos lets us prove things about classical homotopy theory. Of course, there are many more options at our disposal. For instance, to any group $G$ we can build a topos whose objects are "spaces equipped with a $G$ action", and when we interpret HoTT in this topos, we get a homotopy theory that automatically respects $G$-symmetries. Similarly to any space $X$ we can build a topos $\mathsf{Sh}(X)$ of "sheaves of spaces over $X$". Interpreting HoTT in this topos gives statements about bundles of homotopy types over $X$, etc.

In the "classical" theory of $1$-topoi, we get a category (the topos) whose objects "look like sets" in the sense that we can manipulate them like ordinary sets, prove things about them as though they were sets, etc. This is a powerful tool for proving facts about complicated objects (like sheaves) that hides a lot of the complexity of those objects. Now, in the theory of $(\infty,1)$-topoi, we get an "$\infty$-category" whose objects "look like spaces" in an analogous way. The incredible thing is that these spaces can also be manipulated "like sets" (as long as you're somewhat careful) which is precisely the machinery of HoTT! So now we have a tool for proving incredibly complicated statements (about sheaves of homotopy types, say) by using the fairly simple language of type theory.

You ask how we can recognize when a collection of spaces is a model of HoTT, and the answer is given by the Giraud-Rezk-Lurie theorem which gives necessary and sufficient conditions for an $\infty$-category to actually be a topos. Be warned, though! The subject of $\infty$-topoi (and even of $\infty$-categories) can be unforgiving to newcomers, and there's a lot of background knowledge that is expected of you. The upshot, of course, is that it's some of the coolest math being done today, and the community is extremely accepting and inviting (something that unfortunately cannot be said of every branch of math...). There's lots of people who will be happy to help you along the journey, should you choose to pursue it!


I hope this helps ^_^