nLab
predicative topos

Contents

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

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

Revised on August 11, 2013 17:09:12 by Urs Schreiber (89.204.135.38)