I’m in the process of changing jobs. As a result of that, I’ve actually got some time between leaving the old, and starting the new. So I’ve been trying to look into Topoi. Topoi are, basically, an alternative formulation of mathematical logic. In most common presentations of logic, set theory is used as the underlying mathematical basis – set theory and a mathematical logic built alongside it provide a complete foundational structure for mathematics.
Topoi is a different approach. Instead of starting with set theory and a logic with set theoretic semantics, Topoi starts with categories. (I’ve done a bunch of writing about categories before: see the archives for my category theory posts.)
Reading about Topoi is rough going. The references I’ve found so far are seriously rough going. So instead of diving right in, I’m going to take a couple of steps back, to some of the foundational material that I think helps make it easier to see where the category theory is coming from. (As a general statement, I find that category theory is fascinating, but it’s so abstract that you really need to do some work to ground it in a way that makes sense. Even then, it’s not easy to grasp, but it’s worth the effort!)
A lot of category theoretic concepts originated in algebraic topology. Topoi follows that – one of its foundational concepts is related to the topological idea of a sheaf. So we’re going to start by looking at what a sheaf is.