A generic proof in a category is a map such that for every map , there exists a (not necessarily unique) map such that and 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:
If has finite limits, then its ex/lex completion is a topos if and only if has weak dependent product?s and a generic proof.
In particular, if is a locally cartesian closed category, then is a topos if and only if has a generic proof.
A counterpart of generic proofs in type theory is Russell’s axiom of reducibility?.
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,” seems, at least a priori, to be weaker than the full axiom of choice.
A (seemingly) 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.