A generic proof in a category is a map (morphism) with all pullbacks such that, for every map , there exists a (not necessarily unique) map such that and the pulled back map each factor through each other, i.e. they are equivalent in the preorder reflection? of the slice category .
The main interest of generic proofs is in the following:
In particular, if is a locally cartesian closed category, then is a topos if and only if has a generic proof.
If is a topos satisfying the axiom of choice, then its subobject classifier is a generic proof, since any factors through, and (assuming AC) is factored through by, its image, a subobject of . In fact, for such a , is equivalent to .
The statement ” has a generic proof,” or equivalently ” is a topos,” is weaker than the full axiom of choice. Indeed, Menni 2007 shows that the exact completion of a Boolean Grothendieck topos with enough points is also a topos.
An even weaker statement is ” is well-powered.” Note that if is a set, then the subobject lattice of (the image of) in is precisely the preorder reflection of ; thus this second statement says in particular that all such preorder reflections are essentially small. This can be regarded as saying that although full AC may not hold, it is only violated in a “small way” at each set. It is sufficient, for instance, to show that the category of anafunctors between two small categories is essentially small.
An instructive example is where (the arrow category of ): this is an example of an exact completion of a topos that is well-powered but not itself a topos (because lacks a generic proof). It also shows, taking to be the coproduct completion? of the walking arrow, that we can have (which is here) a topos but not a topos. Details may be found in Menni’s 2003 paper, section 5.3.
Matías Menni, “Exact completions and toposes”, Ph.D. Thesis, U. Edinburgh 2000. (web)
Matías Menni, A characterization of the left exact categories whose exact completions are toposes, J. Pure Appl. Algebra 177 (2003) 287-301. (pdf)
Matías Menni, Cocomplete toposes whose exact completions are toposes, J. Pure Appl. Alg. 210 (2007), 511–520. (pdf)