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

Definition

A predicative topos is a ΠW-pretopos satisfying the axiom of multiple choice.

This is (van den Berg, def. 6.1).

Remark

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.

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

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