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?

]]>