Life in Johnstone's Topological Topos 1 -- Fundamentals | Chris Grossack's Blog
I’ve been thinking a lot about the internal logic of topoi again, and I want to have more examples of topoi that I understand well enough to externalize some statements. There’s more to life than just a localic $\mathsf{Sh}(B)$, and since I’m starting to feel like I understand that example pretty well, it’s time to push myself to understand other important examples too!
In particular, it would be nice to throw some gros topoi into the mix, and where better to start than Johnstone’s topological topos? This topos is fairly small (which makes explicit computation easy) and is very well studied (which makes finding references and examples merely annoying instead of totally impossible). Eventually I’ll want to learn about the effective topos1 (and other realizability topoi more generally), various smooth topoi, etc. but let’s take them on one-at-a-time!
Well, if we’re working in $\mathsf{Set}$, then a space is a set $X$ equipped with some ~bonus structure~. This structure can take a lot of forms, but one ubiquitous example is that of a topology $\tau \subseteq \mathcal{P}(X)$.
/cdn.vox-cdn.com/uploads/chorus_asset/file/23951575/VRG_Illo_STK192_L_Normand_LinaKhan_Neutral.jpg)
