basic constructions:
strong axioms
further
In traditional mathematics and set theory, the category Set of all sets is the archetypical topos. However, in predicative mathematics with its notion of sets, these do not form a topos since they do not satisfy the powerset axiom. In constructive mathematics, we may be weakly predicative and almost form a topos; the resulting weaker structure which Bishop sets (for example) form is a predicative topos (van den Berg).
There are various notions of predicative topos in the literature (see references below); here we discuss the notion advocated by Benno van den Berg.
A predicative topos is a ΠW-pretopos satisfying WISC.
This is (van den Berg, def. 6.1), who however calls what we call WISC the “axiom of multiple choice”, and the usual axiom of multiple choice the “strong axiom of multiple choice”.
In other words, the axiom of multiple choice appears in different strengths in the literature; see at WISC. Accordingly there is the notion of strong/weak predicative topos if it satisfies the strong/weak version of this axiom; van den Berg’s notion of predicative topos is the weak version.
Note that an impredicative elementary topos is not necessarily a predicative topos in this sense. A topos is always a $\Pi$-pretopos, and if it has an NNO then it is a $\Pi W$-pretopos, but it need not satisfy WISC (Roberts 2015).
A different approach to a notion of predicative topos is to assert, rather than a weak choice principle, the existence of some categorical version of higher inductive types. But this would also exclude some elementary toposes.
A category of internal sheaves over an internal site in a predicative topos is again a predicative topos.
This is (van den Berg, theorem 7.5), using vdBerg-Moerdijk, theorem 4.21
The category of Bishop sets in Martin-Löf dependent type theory is a [strong predicative topos.]
This is (van den Berg, theorem 6.2), based on (Moerdijk-Palmgren 99, section 7) and (Moerdijk-Palmgren 00, section 10).
Not every topos is a predicative topos, or even every $Set$-topos (i.e. a topos with a geometric morphism to the category $Set$, see (Roberts 2015)), but every Grothendieck topos – a bounded $Set$-topos – is.
The goal of formulating a notion of predicative topos was stated and pursued in a series of articles containing
The definition then appears in
Discussion of the category of sets as a $\Pi$-W-topos when formalized via h-sets in homotopy type theory is in
A non-example constructed via the internal logic of an unbounded $Set$-topos is given in
Last revised on March 4, 2019 at 07:12:14. See the history of this page for a list of all contributions to it.