Could not include topos theory - contents
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).
This is (van den Berg, def. 6.1).
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.
The goal of formulating a notion of predicative topos was stated and pursued in a series of articles containing
The definition then appears in