In mathematics, an elementary topos (plural toposes or topoi) is a category which has properties making it resemble the category of sets. Elementary toposes can be used as models of intuitionistic higher-order logic.
An elementary topos (hereafter just topos) can be pictured as an alternate mathematical universe. It is a category which is sufficiently like the category of sets (the “standard mathematical universe”) that common mathematical constructions can be carried in it, such as subsets, function spaces, etc.
More precisely, a topos supports intuitionistic higher-order logic as an internal language. As such, toposes are widely used as models of constructive mathematics.
As originally defined by Lawvere and Tierney, an elementary topos is a category such that:
The requirement that be finitely cocomplete was later observed to be redundant, as it follows from the rest. (However, the general construction of finite colimits is relatively complicated; in most examples, one can find a more concrete description, which simplifies the translation of statements from the internal language.)
An even more minimalistic definition is possible: an elementary topos is a finitely complete category with power objects. (This essentially replaces the requirements to have exponentials and a subobject classifier with just the special case of exponentials .)
Many other properties follow, such as being regular and moreover exact.
A logical functor is a functor between topoi that preserves finite limits and power objects. Logical functors preserve the structures that topoi have. In particular, they preserve finite colimits, subobject classifiers, and exponential objects.
Having a subobject classifier is a strong requirement, which rules out most categories of algebraic structures such as groups, rings, etc.
Every Grothendieck topos (a category equivalent to the category of sheaves on a site) is an elementary topos. Important special cases include:
The category of finite sets is an elementary topos (however, it lacks a natural numbers object), and similarly for finite -sets.
The effective topos is an important example of an elementary topos with natural numbers object. It is not a Grothendieck topos. It can be viewed as a universe of computable mathematics. This example is generalized by realizability toposes.
A source of examples is the fundamental theorem of topos theory, which states that for every elementary topos and every object , the slice category is an elementary topos.