example. topos [tt-004R]
example. topos [tt-004R]
Topos theory unifies, in an extraordinary way, important aspects of geometry and logic.
Grothendieck topos was first introduced by Grothendieck to generalize topological space [kostecki2011introduction, 7.2]:
every space gives rise to a topos (namely, the category of sheaves on it).
Topological properties of the space can be reinterpreted in a useful way as categorical properties of its associated topos.
Elementary topos was introduced by Lawvere and Tierney, to generalize Set. A topos can be regarded as a 'universe of sets' [leinster2016basic, 6.3.20]. \(\mathbf {Set}\) is the most basic example of a topos, and every topos shares enough features with Set that [⧉]
anything you really really needed to do in the category of sets can be done in any topos.
Every presheaf category, is a topos. [leinster2016basic, 6.3.27]
A topos can allow the interpretation of a higher-order logic. In particular, objects can be seen as collections of elements of a given type, subobjects are viewed as propositions. Products and coproducts are interpreted as conjunction and disjunction respectively. For an introduction, see [pitts2001categorical].