As a Grothendieck topos is a categorified locale, so an ionad is a categorified topological space. While the opens are primary in toposes and locales, the points are primary in ionads and topological spaces.
Toby: I expect that you know this, David, but for the record: it's still the subobject classifier constructively, but that may not be . I have written this as ‘’ to try to keep it simple but unbiased.
David Roberts: Sure. I wonder then what the analogue of the constructive is when we pass to as a 2-topos. Would it be a constructive version of ? Thoughts?
Toby: As a constructive mathematician, I would just say that it is ; I simply would not accept that is a boolean topos. In the case of the poset of truth values, which I am calling here, the classical mathematician has an even simpler description of that poset, which you have called . But in the case of , even the classical mathematician has no simpler way to describe it, so constructivists should already be happy with Garner's definition of ionads. (A strongly finitist mathematician, however, could describe up to equivalence very explicitly as a locally finite category whose set of objects is , which the finitist would regard as still a large category, and other mathematicians would not be satisfied with that description.)
The word ‘ionad’ is Irish for a location, place, or site; ‘Ionad’ often translates ‘Centre’ in titles of institutions. It is pronounced /ˈɪnəd/ (roughly ‘INN-ad’ or ‘UNN-ad’, not ‘i-NAD’ or ‘yonad’; ‘ЫН-ад’ in a North Slavic language), or more precisely [ˈɨ̞n̪ˠəd̪ˠ] (at least in Munster), following Wikipedia. The plural (which you can use if you like to use ‘topoi’ too) is ‘ionaid’ (/ˈɪnəɟ/, ‘INN-adge’ or ‘UNN-adge’, ‘ЫН-адь’, [ˈɨ̞n̪ˠədʲ]). We could go on to decline it out of the nominative case, but now it's getting silly.
Finn Lawler: I would pronounce this more like ‘UNN-ad’ (I don’t know enough about IPA to make that more precise). The Irish dialect I was exposed to (there being no Dublin or Leinster dialect) is the standard one taught in schools, which is an amalgam of all three, but principally that of Connacht, I think.
The nominative plural is ‘ionaid’, which I would pronounce something like ‘UNN-idge’. Here the ‘d’ is palatized.
Toby: I'm just using my knowledge of phonology to follow the information on Wikipedia's articles, so take it with a grain of salt. However, I can imagine someone hearing [ˈɨ̞n̪ˠəd̪ˠ] as ‘UNN-ad’, so I happily add it to the text. I don't suppose you can get a good recording? (Also, thanks for the plural, which I should have looked up for myself.)
for all subsets of .
Categorifying (mostly), we have this:
It seems to me that a full categorification would allow to be a groupoid. —Toby
Mike Shulman: Actually, if you want to allow groupoids, I don’t think there’s any reason not to allow arbitrary categories. Richard and I had a discussion about this question, and at one point I think he was on the side you present, but we’ve both since come around to this version. Notice that any ionad induces a category structure on its set of points, since each point is in particular a geometric morphism from to . I think this induced “category of points” should be regarded as a categorification of the specialization order induced on the points of a topological space. In particular, it comes for free as part of the structure; you don’t have to specify it in advance.
You can specify either of them in advance; you can start with being a category in the definition of ionad, or you can define a generalized sort of topological space as a poset equipped with a lex comonad on its poset of downsets. In either case it amounts to specifying an ordinary ionad/space, together with a distinguished category/poset mapping bijectively-on-objects to its induced category/poset of points. In both cases, any continuous map necessarily preserves the induced category/order, but if you start with a distinguished category/order of points, your continuous maps have to preserve that too. These notions might be interesting, but the comparison makes me fairly sure that ionads starting with a set are already the natural “fully categorified” categorification of topological space.
Toby: I didn't want to allow just any category, to be analogous to not allowing just any p(r)oset as points of a topological space. But I'll think about what happens when the points are allowed to form a groupoid.
Mike Shulman: I think the same argument applies to groupoids. As I said, any ionad induces a category structure on its set of points, and if you start with a groupoid you’re just picking a distinguished groupoid on that set of points which maps bijectively-on-objects to the induced category.
It’s like the difference between a Segal space and a complete Segal space. Segal spaces may be interesting, but it’s the complete ones that model -categories. And also the difference between an ordinary multicategory and an “enhanced” multicategory in the sense of Baez-Dolan-Cheng. The weird notions that come with an extra groupoid structure on the objects may be technically useful, but usually the more fundamental notion is the one where the groupoid of objects is induced from the category of objects.
Although Garner does not require an ionad to be bounded, the nicest results hold for them, and all of his applications involve only bounded ionads. In fact, Garner writes, ‘Indeed, the existence of unbounded ionads is a problem that seems to be independent of the axioms of Zermelo-Fraenkel set theory.’ (Section 3.8).
for every subset of , where takes the preimage.
Categorifying (and adding a coherence law), we have this:
where is , such that ‘respects the comonad structures’.
I need to figure out exactly what this last clause means.
There is an obvious notion of 2-morphism, which turns out to be trivial (but probably would not be if were allowed to be a groupoid). However, the category of ionads is presumably (like Top) still a locally prosetal 2-category under the specialisation order.
Given an ionad , an open in is simply a coalgebra of the comonad .
The opens of form a topos , and we have a surjective geometric morphism from to . In fact, an ionad may be defined as a set together with a surjective geometric morphism from to some topos, much as a topological space may be defined as a set together with a surjective locale morphism from to some locale. The topos is essentially unique by surjectivity, and this also shows that has enough points?.
Just as is a frame whenever is a topological space, so should be a Grothendieck topos when is an ionad. In fact, this holds only for bounded ionads; an ionad may be defined to be bounded if and only if its topos of opens is cocomplete (or equivalently a Grothendieck topos).
A continous map between topological spaces may be given by a function and a commuting square
Similarly, a continuous map between ionads may be given by a function and a commuting square
Without loss of generality, we may require this square to commute on the nose; this is related to the triviality of -morphisms in the category of ionads.
Note that the map must be the preimage half of a geometric morphism from to ; we may also define a continous map to to be such a geometric morphism together with a compatible map between the generating points of the toposes.
Ionads have been introduced and studied in