Discover the Fascinating World of Topos Theory with Mark Hopkins 📚

A Taste of Topos Theory - Mark Hopkins

There are many ways to approach the mathematical field of topos theory.
One view is that the concept of "topos" allows us to extract an interface
from set theory, that we can apply to other domains that also fit the definition of a topos.

The interface turns out to be a lambda calculus, and one with a lot of nice
features: it has sums and products, it's dependently typed, it has refinement types with intersection and union i.e. we can form subtypes by applying a predicate, and frequently it comes with other goodies like modalities.
By happy coincidence some of the most common constructions in discrete maths and computer science - graphs, automata - are topoi, or at least quasitopoi.

We'll explore what this all means with an example or two.