nLab ionad



Topos Theory

topos theory



Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory




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 Set XSet^X plays an role analogous to that of the lattice 𝟚 X\mathbb{2}^X (the power set of XX) in the theory of topological spaces. Intuitively, we are categorifying the subobject classifier 𝟚Set\mathbb{2}\in Set to the “categorified subobject classifier” SetCatSet\in Cat (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̪ˠeast 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’, ‘ЫН-адь’, [nd]). We could go on to decline it out of the nominative case, but now it's getting silly.


Recall that a topology on a set XX can be defined by giving its interior operator, an operation Int:𝟚 X𝟚 XInt\colon \mathbb{2}^X \to \mathbb{2}^X (where 𝟚\mathbb{2} is the poset of truth values) such that

  • AInt(A)A \supseteq Int(A),
  • Int(Int(A))Int(A)Int(Int(A)) \supseteq Int(A),
  • Int(X)=XInt(X) = X, and
  • Int(AB)=Int(A)Int(B)Int(A \cap B) = Int(A) \cap Int(B)

for all subsets A,BA, B of XX.

In more sophisticated language, IntInt is a finite meet-preserving comonad on the power set of XX.

Categorifying (mostly), we have this:


An ionad is a set XX together with a finite limit-preserving comonad Int XInt_X on the category Set XSet^X. An ionad is bounded if the comonad is accessible.

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).

Remark (Garner Remark 3.9)

Bounded ionads give rise to exactly the Grothendieck toposes with enough points as their topos of coalgebras. (See below)

Sets, groupoids, or categories?

It may seem odd to take XX to be a set rather than something else such as a groupoid or a category. An analogous definition can be given where XX 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:

  1. A set XX together with a finite-limit-preserving comonad on its powerset 𝟚 X\mathbb{2}^X.
  2. A set XX equipped with an equivalence relation (which we can regard as a preorder that happens to be symmetric) together with a finite-limit-preserving comonad on the hom-preorder 𝟚 X\mathbb{2}^X.
  3. A preorder XX together with a finite-limit-preserving comonad on 𝟚 X\mathbb{2}^X.

All three of these induce a topology on the underlying set of XX. But it is (1) that is exactly a topological space: (2) and (3) include the extra data of a (perhaps symmetric) preorder on XX 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):

  • A structure as in (2) above, but such that the given equivalence relation coincides with the relation “xx and yy are in all the same open sets” (which it automatically implies).
  • A structure as in (3) above, but such that the given preorder coincides with the specialization preorder.

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

  • A groupoid XX with a finite-limit-preserving comonad on Set XSet^X such that the induced functor from XX to the category of points of the resulting topos is pseudomonic.
  • A category XX with a finite-limit-preserving comonad on Set XSet^X such that the induced functor from XX to the category of points of the resulting topos is fully faithful.

(Asking that these functors also be surjective on objects would be a sobriety condition on an ionad.)

When categorifying further to “nn-ionads” and “\infty-ionads”, the possible options multiply further; but that is probably a topic for another page. For discussion of these questions, see the nForum thread.

Morphisms of ionads

Recall that, given two topological spaces XX and YY, a continuous map from XX to YY is a function f:XYf\colon X \to Y (on the underlying sets) such that

  • f *(Int(A))Int(f *(A))f^*(Int(A)) \subseteq Int(f^*(A))

for every subset AA of YY, where f *f^* takes the preimage.

Categorifying (and adding a coherence law), we have this:


Given ionads XX and YY, a continuous map from XX to YY consists of a function f:XYf\colon X \to Y (on the underlying sets of points) together with a natural transformation

Int f:f *Int YInt Xf *, Int_f\colon f^* \circ Int_Y \to Int_X \circ f^* ,

where f *:Set YSet Xf^*\colon Set^Y \to Set^X is Set fSet^f, such that Int fInt_f ‘respects the comonad structures’.

I need to figure out exactly what this last clause means.

Note that Int fInt_f is part of the structure here; it is not merely a property. (In other words, the forgetful functor from ionads to topological spaces is not faithful.)

There is an obvious notion of 2-morphism, which turns out to be trivial (but probably would not be if XX 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.

The topos of opens

As every topological space has a Heyting algebra (in fact a frame, or dually a locale) of open subsets, so every ionad has a topos (in fact a Grothendieck topos, if it is bounded) of opens.


Given an ionad XX, an open in XX is simply a coalgebra? of the comonad Int XInt_X.

The opens of XX form a topos Ω(X)\Omega(X), and we have a surjective geometric morphism from Set XSet^X to Ω(X)\Omega(X). In fact, an ionad may be defined as a set XX together with a surjective geometric morphism from Set XSet^X to some topos, much as a topological space may be defined as a set XX together with a surjective locale morphism from 𝟚 X\mathbb{2}^X to some locale. The topos Ω(X)\Omega(X) is essentially unique by surjectivity, and this also shows that Ω(X)\Omega(X) has enough points.

Just as Ω(X)\Omega(X) is a frame whenever XX is a topological space, so Ω(X)\Omega(X) should be a Grothendieck topos when XX 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 f:XYf\colon X \to Y and a commuting square

Ω(Y) Ω(X) 𝟚 Y f * 𝟚 X \array { \Omega(Y) & \to & \Omega(X) \\ \downarrow & & \downarrow \\ \mathbb{2}^Y & \overset{f^*}\to & \mathbb{2}^X }

Similarly, a continuous map between ionads may be given by a function f:XYf\colon X \to Y and a commuting square

Ω(Y) Ω(X) Set Y f * Set X \array { \Omega(Y) & \to & \Omega(X) \\ \downarrow & & \downarrow \\ Set^Y & \overset{f^*}\to & Set^X }

Without loss of generality, we may require this square to commute on the nose; this is related to the triviality of 22-morphisms in the category of ionads.

Note that the map Ω(Y)Ω(X)\Omega(Y) \to \Omega(X) must be the preimage half of a geometric morphism from Ω(X)\Omega(X) to Ω(Y)\Omega(Y); we may also define a continous map XX to YY to be such a geometric morphism together with a compatible map between the generating points of the toposes.

Bases of ionad structures


Ionads have been introduced and studied in

Some basic aspects of the theory are developed there, and applications to topology, logic and geometry are discussed.

Further aspects of the theory of ionads, with a focus on their logical importance were studied in

Last revised on May 24, 2023 at 21:23:35. See the history of this page for a list of all contributions to it.