@Jonathan Sterling; January 15, 2020

Practitioners of theoretical computer science tend to view the topos mainly as a mathematical universe “inside which” one works. The first encounter with the topos is typically motivated by presheaves, which are functors $\mathscr{C}^{\mathrm{op}}\to\mathbf{Set}$; common examples include $\mathscr{C} = \omega$ for guarded recursion or step-indexing, $\mathscr{C} = \mathbf{FinSet}^{\mathrm{op}}$ for variable binding, etc. The lesson that many workers in computer science have learned is that the pitifully bureaucratic yawping involved in stating and substantiating the laws for families of thingies that vary nicely in some other thingy can be eliminated with prejudice by simply working internally to a category of (pre)sheaves. We have saved many trees in Pittsburgh this way during the past couple years.

This was my own first rendezvous with the world of topoi — at the time, I was frustrated with the complexity of manually combining the already quite complex model of dependent type theory in partial equivalence relations (due to Stuart Allen) with variation in contexts of “clock names”, each of which is glued onto a copy of $\omega$, for the purpose of reducing coinduction to guarded recursion. My answer to this regrettable quagmire was to first develop the logic of clock-indexed guarded recursion in an abstract setting (a certain category of presheaves), and then develop the partial equivalence relation model internally to this logic:

<aside> 📖 S., Harper (2018). Guarded Computational Type Theory. LICS.

</aside>

This admittedly practical perspective on topoi, that they are a tool to wipe out repetitive “reasoning” by factoring out naturality and continuity conditions, is unfortunately reductive enough that those of us who stop there will miss out. I want to point out some other aspects of topos theory coming from geometry and algebra that yet have important implications for computer science and programming languages, which I think are not so well-understood except among topos theorists — a very small group of people whom we are sadly losing more quickly than we can replace them, a cadre from a more elegant age in which a nod and a wink from “Sammy” Eilenberg could secure a tenured position. I hope to give some motivation to this geometrical perspective from the point of view of a computer scientist, touching on my recent manuscript with Bob Harper on logical relations and the phase distinction vis-à-vis ML modules.

<aside> 📖 S., Harper **(2020). Logical Relations as Types: Proof-Relevant Parametricity for Program Modules. Unpublished manuscript.

</aside>

The exposition here owes a lot to that of Anel and Joyal; while Anel and Joyal emphasize the connections between topos theory, geometry, and commutative algebra, we make the connection to computer science and programming languages.

<aside> 📖 Anel, Joyal (2019). Topo-logie. New Spaces in Mathematics and Physics — Formal and Conceptual Reflections.

</aside>

Grothendieck topos theory as general topology

Sheaves on a topological space

We have to go back to the beginning. A topological space is a pair $(X,\mathcal{O}_X)$ of a set of “points” $X$ and a frame of open subsets $\mathcal{O}_X\subseteq \mathcal{P}(X)$: that $\mathcal{O}_X$ is a frame means that it is closed under finite intersection and arbitrary unions, and that finite intersections distribute across unions (which is in this case automatic). It is very common in mathematics to metonymically write $X$ for the pair $(X,\mathcal{O}_X)$, which we will feel free to do.

An open cover of an open $U\in\mathcal{O}_X$ is a family of open subsets $V_i\subseteq U$ such that $U\subseteq\bigcup_i V_i$; we will write $V\twoheadrightarrow U$ to denote an open cover.

The utility of sheaves is to attach algebraic data to the space $X$ in a way that is compatible with restriction to open subspaces and with gluing together data defined on an open cover. Formally this is achieved by associating to each open $U \in \mathcal{O}_X$ a set $E(U)$, and to each open subset $V\subseteq U$ a restriction map $E(U)\to E(V)$, such that the following gluing principle holds: if $\bigcup_i V_i$ covers $U$, then mutually compatible elements of $E(V_i)$ may be extended to a unique total element of $E(U)$. One can show that this definition is equivalent to stating that $E$ is a presheaf on the posetal category $\mathcal{O}_X$ that satisfies an additional “gluing” axiom to ensure that it treats open covers like covers.

Effective epimorphisms / generalized covers

We can understand the purpose of this gluing axiom from a broader perspective. First of all, an open cover $V\twoheadrightarrow U$ has certain properties that can be re-phrased in generality for any category in which certain limits and colimits make sense, where the notion is rebranded as effective epimorphism, often just called “covers”. A cover in a category $\mathscr{C}$ is a morphism $f : d\twoheadrightarrow c$ whose kernel pair exists such that $f$ that is the coequalizer of its kernel pair; glossed into plain English:

<aside> 💡 A morphism $f:d\to c$ is an effective epimorphism when $c$ is the quotient of $d$ by the relation that identifies any two elements that $f$ treats the same.

</aside>

It’s worth checking for yourself that open covers are effective epimorphisms in $\mathcal{O}_X$.

Now, here is what is happening with the sheaf condition. The Yoneda embedding $h_\bullet : \mathcal{O}_X\hookrightarrow \mathrm{Pr}(\mathcal{O}X)$ sends every open $U$ to the representable functor $\mathrm{Hom}{\mathcal{O}_X}(-,U)$; unfortunately, however, the morphism $h_V\to h_U$ induced by an cover $V\twoheadrightarrow U$ is almost never a cover in $\mathrm{Pr}(\mathcal{O}_X)$. But it can be seen that a presheaf $E : \mathrm{Pr}(\mathcal{O}_X)$ is a sheaf if and only if it treats all (pullbacks of) such $h_V\to h_U$ as if they were effective epimorphisms. Hence the function of the sheaf condition is to ensure that the Yoneda embedding exhibit the sheaves as a true generalization of the opens that respects the geometry of $X$.

Sheaves are generalized (proof-relevant) opens