Topos Theory

topos theory



Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory


Regular and Exact categories

κ-ary regular and exact categories



Category Theory




A pretopos is a category which is both exact and extensive. (See familial regularity and exactness for why extensivity and exactness deserve to be considered together.) This implies that it is a coherent category.

Frequently one is especially interested in pretoposes having additional properties, such as:

  • A Heyting pretopos is a pretopos which is also a Heyting category; a Boolean pretopos is a pretopos which is also a Boolean category. These are suitable as frameworks for finitist predicative mathematics, respectively with intuitionistic or classical logic.

  • A Π-pretopos is a pretopos which is also a locally cartesian closed category. (A Π\Pi-pretopos is automatically a Heyting pretopos.) These are suitable as frameworks for finitist constructive mathematics which is ‘weakly predicative’.

  • A WW-pretopos is a pretopos which has (locally) W-types (initial algebras for polynomial endofunctors), most famously a natural numbers object. (Here, we take any exponentiable morphism to define a polynomial endofunctor. This paragraph is original to this page and not in the literature; it may not be the best definition.) Heyting WW-pretoposes and Boolean WW-pretoposes are suitable as frameworks for non-finitist but strongly predicative mathematics (with intuitionistic and classical logic, respectively).

  • A ΠW-pretopos is a topos that is both a Π\Pi-pretopos and a WW-pretopos. (Now every morphism defines a polynomial endofunctor, since every morphism is exponentiable.) These are suitable as frameworks for weakly predicative constructive mathematics that is not finitist.

  • A predicative topos is a ΠW-pretopos that satisfies the axiom of multiple choice. (This now differs from a WW-topos below mainly in still lacking power objects, hence still a context for weakly predicative constructive mathematics.)

  • A topos is a pretopos that has power objects. A topos is automatically a Π\Pi-pretopos; conversely, a Π\Pi-pretopos is a topos iff it has a subobject classifier, and a Boolean Π\Pi-pretopos is always a topos. Toposes and Boolean toposes are suitable as frameworks for finitist (but otherwise impredicative) mathematics, with intuitionistic and classical logic respectively.

  • A WW-topos is of course a topos that is a WW-pretopos; it is sufficient that the topos have a natural numbers object (see van den Berg & Moerdijk), so this is often called a topos with NNO. These are suitable as frameworks for (non-predicative, non-finitist) constructive mathematics, while Boolean WW-toposes are suitable as a framework for classical mathematics without the axiom of choice.

  • A topos with choice is a topos that satisfies the axiom of choice (that every epimorphism is split). Every topos with choice is automatically boolean, so WW-toposes with choice are suitable as a framework for full classical mathematics. (In fact, a well-pointed WW-topos with choice is precisely a model of ETCS.)

Infinitary pretoposes

An infinitary pretopos is an infinitary coherent category which is both infinitary extensive and exact. Giraud's theorem says that infinitary pretoposes with small generating sets are the same as Grothendieck toposes, and in particular are toposes (although this last result is not valid in predicative mathematics).


Internal logic and mathematics in pretopoi

Like any coherent (or Heyting) category, a (Heyting) pretopos has an internal logic. Extensivity and exactness make a Heyting pretopos a very set-like category. One can say imprecisely that it has “all the good first-order properties of a topos”, meaning not that it has those properties that can be expressed in elementary terms (which is false) but that it has those properties that (unlike exponential and power objects) correspond to first-order reasoning in ordinary mathematics. Therefore, pretoposes (especially Heyting, Π\Pi, and/or WW ones) are related to predicative constructive mathematics in a way similar to how toposes are related to non-predicative constructive mathematics.


A pretopos is necessarily balanced, but while it has coproducts and coequalizers of equivalence relations, it need not have all finite colimits. However, if it has countable pullback-stable unions of subobjects, then any internal binary relation generates an equivalence relation and therefore has a quotient, so we can construct arbitrary coequalizers and thus arbitrary finite colimits. And we can perform an “internal” version of this argument in a Π\Pi-pretopos with a NNO, such as a Π\Pi-WW-pretopos.

The precanonical topology

A pretopos, being a coherent category, admits a subcanonical Grothendieck topology called the coherent topology. In a pretopos, this topology is generated by finite jointly epimorphic families. Since the canonical topology on a Grothendieck topos consists of all jointly epimorphic families, the coherent topology on a pretopos is sometimes called the precanonical topology.

The codomain fibration of a pretopos is always a stack for its precanonical topology. Being a pretopos is stronger than necessary for this condition to hold in a coherent category, however; see coherent category for the necessary and sufficient conditions.


Revised on July 13, 2017 10:02:34 by Urs Schreiber (