I wonder how much of localic homotopy theory could be done in cohesive homotopy type theory with the shape modality represented by localization at the locale of real numbers?

]]>Moerdijk-Wraith might be what I was thinking of.

]]>You might want to check

- Erik Palmgren ,
*From intuitionistic to point-free topology: some remarks on the foundation of homotopy theory*, (2006). (pdf)

and the references therein.

Another interesting paper in the direction of toposes is

- Moerdijk-Wraith,
*Connected locally connected toposes are path-connected*, Transactions AMS**295**(1986) pp.849-859. (pdf)

Although this hardly qualifies as “low brow”.

]]>The closest I can recall having seen is, I think, a definition of a fundamental group of a topos using real-interval paths, and a comparison to the “topos-theoretic” fundamental group. But I can’t remember what paper that was in.

It might also be worth looking (again, perhaps) at Moerdijk’s “classifying spaces and classifying topoi”.

]]>Mike, that’s of course the right general abstract point of view. For a change, I was wondering about a low-brow approach. Say one were to do the analogue of a standard first course in topology, starting from scratch and culminating in some elementary basics of homotopy theory such as fundamental group and covering spaces, but now all based on locales instead of topological spaces. I am wondering if this has been considered somewhere.

]]>Indeed! Perhaps I misunderstood, I thought you were suggesting that viewing homotopy theory as about $\infty$-groupoids gives us a ‘localic homotopy theory’.

]]>Saying that homotopy theory is about $\infty$-groupoids doesn’t preclude us from studying how other objects like spaces, locales, topoi, and their algebraic versions give rise to $\infty$-groupoids! In particular, that’s what cohesive $\infty$-toposes are all about (but neither are they they only way to study it).

]]>Mike: I don’t feel that this is really the same thing with regard to obtaining a ’constructive homotopy theory’, or indeed a self-standing localic homotopy theory (divorced of the constructive aspect).

1) If this was the whole story, it should generalise to other space-like settings. And it does *not* generalise to motivic homotopy theory. Here we invert the affine line, so end up with something with contractible shape, but the most significant aspect of the homotopy theory, where the Tate twists enter, is completely missed if we stop there. There is clearly something more than purely the contractibility of $\mathbb{R}$ at play. It is true that we do not have an $(\infty,1)$-topos in the motivic setting after inverting the affine line, but I do not think that that accounts for it.

2) Even if one takes this perspective, the topological representation can be useful for homotopy theory (there are still many things in chromatic homotopy theory that need significant geometric input, as far as I know), and without a constructive approach to homotopy theory of topological spaces we do not have that available (constructively).

3) That homotopy theory is about $\infty$-groupoids is also not on firm foundations, even non-constructively; to assume it is basically to bypass the hardest aspects of constructive homotopy theory. One aspect is the missing homotopy hypothesis, but we also lack the bridge between topological spaces and homotopy types in the first place. This does not mean of course that we cannot ignore these issues and explore notions of $\infty$-groupoid that match our intuition, as everyone is doing. But we should remember that we have not magically addressed the original question.

4) Homotopy is also used as a tool in geometric topology (for instance) even in its most fundamental notions (isotopy). Here $\infty$-groupoids are certainly not an appropriate language; geometric topology corresponds to much higher categorical phenomena. That is to say: to use homotopy theory as a tool is different from studying homotopy types alone, and the former uses the topological representation.

]]>From the modern point of view that homotopy theory is about $\infty$-groupoids, with topological spaces simply representing their fundamental $\infty$-groupoid, we can say that every topos — even every $(\infty,1)$-topos — has a shape that is in good cases represented by an $\infty$-groupoid, and locales are simply localic toposes. The role of the real numbers is just that they happen to have a contractible shape, so that any “homotopy equivalence” defined using them must necessarily give rise to an equivalence of shapes. Parametrized homotopy theory and equivariant homotopy theory are also particular cases of the $(\infty,1)$-categorical perspective.

]]>Or even translate it into English along with the rest of mathematics: big topos.

]]>*gros topos*, with a single “s”. it matters :-)

One possibility is to use classifying toposes to construct the geometric realization, as in Peter Johnstone’s - a topological topos. Simplicial sets classify strict linear orders, so one needs (at least) classical logic to construct the geometric realization into the gross topos over locales. For the gross topos over locales see e.g. continuous truth. As I observed here, this idea can be made to work for Grothendieck’s simplest test category/ the cubical sets with diagonals. They classify strictly bi-pointed sets and the unit interval in the gross topos over locales, is bi-pointed.

I am not sure whether that answers your question.

]]>Homotopy theory in any constructive topological setting (localic, type-theoretic) is highly under-developed, I would say. I’ve often thought about it myself, but I’m put off by two things: I think a really good foundations for (constructive) topology remains to be found; and developing the algebraic topology of finite topological spaces might be more interesting.

A crucial result to aim at is the one that makes the bridge to simplical/cubical/whatever sets possible, Milnor’s theorem. Here the compactness of the unit interval is certainly needed, and things are quite delicate.

]]>I am starting *localic homotopy theory*, with some pointers.

back in “The point of pointless topology” Peter Johnstone suggested that localic homotopy theory ought to be developed:

So far, relatively little work has been done on specific applications of locale theory in contexts like these; so it is perhaps appropriate to conclude this article by mentioning some areas which (in the writer’s opinion, at least) seem ripe for study in this way. One is homotopy theory: the work of Joyal, Fourman and Hyland [15] shows that in a constructive context it may be necessary to regard the real Une as a (nonspatial) locale, at least if we wish to retain the Heine-Borel theorem that its closed bounded subsets are compact. So there is scope for developing the basic ideas of homotopy theory for locales, starting from the localic notion of the unit interval; when interpreted in the two contexts mentioned above, it should yield results in the “Ex-homotopy theory” and “equivariant homotopy theory” that have been studied in recent years by James [27, 28]

Has anything been done in this direction?

]]>