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.

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 ΠW\Pi W-pretopos, but it need not satisfy WISC.

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 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 March 5, 2017 03:54:48 by Mike Shulman (76.167.222.204)