nLab generic proof

Generic proofs

Generic proofs


A generic proof in a category CC is a map (morphism) θ:ΘΛ\theta\colon \Theta\to\Lambda with all pullbacks such that, for every map f:YXf\colon Y\to X, there exists a (not necessarily unique) map ν:XΛ\nu\colon X\to \Lambda such that ff and the pulled back map ν *θ:Θ× ΛXX\nu^*\theta\;\colon\; \Theta \times_\Lambda X \to X each factor through each other, i.e. they are equivalent in the preorder reflection? of the slice category C/XC/X.

Y f Θ× ΛX ν *θ X ν Θ θ Λ \array { Y \\ \uparrow \downarrow & \searrow^f \\ \Theta \times_\Lambda X & \overset{\nu^*\theta}\longrightarrow & X \\ \downarrow & & \downarrow\mathrlap{\nu} \\ \Theta & \overset{\theta}\longrightarrow & \Lambda }

The main interest of generic proofs is in the following:


If CC has finite limits, then its ex/lex completion C ex/lexC_{ex/lex} is a topos if and only if CC has weak dependent product?s and a generic proof.

In particular, if CC is a locally cartesian closed category, then C ex/lexC_{ex/lex} is a topos if and only if CC has a generic proof.

A counterpart of generic proofs in type theory is Russell’s axiom of reducibility?.

Axioms of choice

If CC is a topos satisfying the axiom of choice, then its subobject classifier is a generic proof, since any f:YXf\colon Y\to X factors through, and (assuming AC) is factored through by, its image, a subobject of XX. In fact, for such a CC, C ex/lexC_{ex/lex} is equivalent to CC.

The statement “SetSet has a generic proof,” or equivalently “Set ex/lexSet_{ex/lex} 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 “Set ex/lexSet_{ex/lex} is well-powered.” Note that if XX is a set, then the subobject lattice of (the image of) XX in Set ex/lexSet_{ex/lex} is precisely the preorder reflection of C/XC/X; 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 C ex/lexC_{ex/lex} where C=Set C = Set^{\to} (the arrow category of SetSet): this is an example of an exact completion of a topos that is well-powered but not itself a topos (because CC lacks a generic proof). It also shows, taking DD to be the coproduct completion? of the walking arrow, that we can have D exD_{ex} (which is Set Set^\to here) a topos but (D ex) ex(D_{ex})_{ex} 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)

Last revised on February 22, 2013 at 21:56:38. See the history of this page for a list of all contributions to it.