Everything is a presheaf

You could take the classical point of view that everything is a set, but that isn't very rewarding beyond a few nesting levels. You could go from studying sets to studying sets of sets, but in general there isn't any point in going deeper then that. We need some kind of organizing principle that goes deeper then that.

Is a function now to be represented as a set of set systems of the form {{0},{0,1}}? Perhaps a function is a morphism $f : A \to B$ of sets? In fact neither approach is really satisfying. To cut a long story short, a function $f : A \to B$ should be represented as a presheaf of the topos $Sets^{\to}$. Only then can we start to reason about functions logically.

Taken to its logical conclusion, topos theory will eliminate the unneccessary division between the functional and logic programming paradigms. Functions are just another object of a topos like any other presheaf, and now we can reason about them logically. In particular, the topos $Sets^{\to}$ enables us to construct the dual lattices of subalgebras and congruences of functions. The manner that we do so is no different then for any other presheaf.

• Sets: objects of the topos $Sets$
• Functions: objects of the topos $Sets^{\to}$

With the issue of the foundation of functions finally resolved by topos theory, we can now construct a whole wide range of algebraic structures using sets and functions. We have foundations for more then just sets and set systems. Any algebraic structure from a commutative magma to a lie algebra can be constructed from fundamental presheaves like sets and functions.

Then there is the issue of the categories themselves. All the nicest structures that we can reason about logically are presheaves, and it would seem categories are not that. To expose category theory to logical reasoning we can first construct the presheaf topos of quivers $Quiv$ and the functor $f: Cat \to Quiv$ taking any category to its underlying quiver. Then we are part way to reasoning about categories logically.

The only missing ingredients are composition and identities. In fact we can represent these as functions of the topos $Sets^{\to}$. Any functor induces morphisms of its composition and identity functions in $Sets^{\to}$ which describe the preservation of composition and identities. Then we can reason logically about categories using the presheaf topos $Quiv \times Sets^{\to} \times Sets^{\to}$.

All the data of a category is encoded in its corresponding presheaf. All this can be defined abstractly, so it doesn't matter how you encode categories. When you want to pick out a presheaf from them you simply use one of the presheaf valued functors like $f: Cat \to Quiv$. What matters is you have the option of reasoning about them logically using presheaf theory, so they are integrated into the overall topos theory.

So we have a pretty reasonably thorough system of reasoning about algebraic structures using presheaves not to mention objects that are already sheaves. Sheaves appear quite often in applications in algebraic and differential geometry. This same framework can be extended to deal with anything from structure sheaves, to schemes, or algebraic spaces. All is possible if you understand the simple fact that everything is a presheaf.