ACT @ The Functorial Topos

Idea

A topos is a category which packages a good deal of interesting structure. Its central feature is the so-called subobject classifier, which enables a lot of interesting internal properties.

Topoi have also the unique feature of being natural objects to study and describe in two very different areas of math: geometry and logic.

The first is where topoi first raised, through the work of Grothendieck on the foundation of algebraic geometry. He envisioned a very general concept of ‘space’, namely a category of sheaves on any site.

The second recognized the role of topoi only some years later, through the work of Lawvere and Tierney, among the others. They actually enlarged the notion of topos to that of elementary topos. This latter notion is more natural from a logical standpoint, since it’s defined in terms of the logical properties a topos is expected to have. Girard characterized those elementary topoi having a presentation as sheaves on a site. These correspond to the ‘original’ concept of topoi, and are thus called Grothendieck topoi.

The archetypal topos is $Set$. For the geometer, this is the topos of sheaves on a single, atomic point. For the logician, this is ?

(…)

Internal mathematics

A revolutionary aspect of topos theory is to present mathematics as taking place not in a fixed, God-given universe but in a variable and rich multiverse.

In fact, topoi have internal languages rich enough to express most of mathematics. This means mathematical theories are no longer constrained to talk and do stuff in a world of sets, but can talk and do stuff in much more interesting worlds.

(…)