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.

David Roberts: The idea strikes me that we are passing from the subobject classifier 2={0<1}2 = \{0 \lt 1\} in SetSet (assuming classical Booleaness) to the categorified subobject classifier SetSet in CatCat.

Toby: I expect that you know this, David, but for the record: it's still the subobject classifier constructively, but that may not be 22. I have written this as ‘𝟚\mathbb{2}’ to try to keep it simple but unbiased.

David Roberts: Sure. I wonder then what the analogue of the constructive 𝟚\mathbb{2} is when we pass to CatCat as a 2-topos. Would it be a constructive version of SetSet? Thoughts?

Toby: As a constructive mathematician, I would just say that it is SetSet; I simply would not accept that SetSet is a boolean topos. In the case of the poset of truth values, which I am calling 𝟚\mathbb{2} here, the classical mathematician has an even simpler description of that poset, which you have called 22. But in the case of SetSet, 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 SetSet up to equivalence very explicitly as a locally finite category whose set of objects is \mathbb{N}, 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.)


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.

It seems to me that a full categorification would allow XX 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 SetSet to Ω(X)\Omega(X). 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 XX 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 (,n)(\infty,n)-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).

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.

Revised on April 8, 2014 17:17:11 by David Roberts (