nLab predicative topos

Idea

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).

Definition

There are various notions of predicative topos in the literature (see references below); here we discuss the notion advocated by Benno van den Berg.

Definition

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”.

Remark

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.

Properties

Theorem

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

Examples

Theorem

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.

References

The goal of formulating a notion of predicative topos was stated and pursued in a series of articles containing

• Ieke Moerdijk, Erik Palmgren, Wellfounded trees in categories (1999) (web)

• Ieke Moerdijk, Erik Palmgren, Type Theories, Toposes and Constructive Set Theory: Predicative Aspects of AST (2000) (web)

• Benno van den Berg, Ieke Moerdijk, Aspects of predicative algebraic set theory III: Sheaves. Proceedings of the London Mathematical Society., (2012) (arXiv:0912.1242)

The definition then appears in

• Benno van den Berg, Predicative toposes (arXiv:1207.0959)

Discussion of the category of sets as a $\Pi$-W-topos when formalized via h-sets in homotopy type theory is in

• Egbert Rijke, Bas Spitters, Sets in homotopy type theory (arXiv:1305.3835)

A non-example constructed via the internal logic of an unbounded $Set$-topos is given in

• David Roberts, The weak choice principle WISC may fail in the category of sets, Studia Logica Volume 103 (2015) Issue 5, pp 1005-1017, doi:10.1007/s11225-015-9603-6 arXiv:1311.3074