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.
Richard Garner developed the theory of ionads, in which the topos plays an role analogous to that of the lattice (the power set of ) in the theory of topological spaces. Intuitively, we are categorifying the subobject classifier to the “categorified subobject classifier” (which classifies discrete opfibrations.
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.
for all subsets of .
Categorifying (mostly), we have this:
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).
It may seem odd to take to be a set rather than something else such as a groupoid or a category. An analogous definition can be given where is a groupoid or a category, of course, but the reason for taking it to be a set is that it makes the analogy to classical topological spaces closer. Consider the following three notions:
All three of these induce a topology on the underlying set of . But it is (1) that is exactly a topological space: (2) and (3) include the extra data of a (perhaps symmetric) preorder on that maps bijectively-on-objects into the specialization preorder of that topology.
However, as in other cases such as Segal categories/complete Segal spaces and generalized multicategories, another way to “get rid of extra data” is to force it to duplicate data that’s already present (a “completeness” condition). Thus we could consider instead (still in the uncategorified case):
These would give equivalent definitions to (1), but may be better-behaved in some ways. In homotopy type theory without sets cover, they would no longer be equivalent, but the groupoidal/preorder versions might be better. For ionads the corresponding definitions would be
(Asking that these functors also be surjective on objects would be a sobriety condition on an ionad.)
When categorifying further to “-ionads” and “-ionads”, the possible options multiply further; but that is probably a topic for another page. For discussion of these questions, see the nForum thread.
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