nLab
predicative topos

Context

Topos Theory

topos theory

Background

Toposes

Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory

Theorems

Foundations

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

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.

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 SetSet-topos (i.e. a topos with a geometric morphism to the category SetSet, see (Roberts 2015)), but every Grothendieck topos – a bounded SetSet-topos – is.

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

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

Revised on October 3, 2016 04:30:37 by David Roberts (202.138.10.51)