# nLab predicative topos

topos theory

foundations

## Foundational axioms

foundational axiom

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