An object $X$ of a category $C$ is said to be *projective* if the hom-functor $C(X,-)$ preserves epimorphisms (or, in general, some restricted class of epimorphisms such as the regular or effective ones). The axiom of choice is equivalent to the assertion that all objects of **Set** are projective. In general, a "projective set" $X$ is one such that we can make $X$-indexed families of choices.

In section D4.5 of *Sketches of an Elephant*, an object $X$ of a topos $C$ is said to be *internally projective* if the right adjoint $\Pi_X : C/X \to C$ preserves epimorphisms, and $C$ is said to satisfy the *internal axiom of choice* if all objects are internally projective. The latter definition is found in many other places; I haven't seen the former elsewhere, but I don't know its actual origin.

My question is, if $X$ is internally projective in this sense in $C$, is $X\times Y$ internally projective in $C/Y$ for another object $Y$? This seems to be a necessary condition for the definition to be sufficiently "internal", but I haven't been able to prove it yet.

A similar question is, if $C$ satisfies the internal axiom of choice, does the functor $\Pi_f : C/X \to C/Y$ preserve epimorphisms for any morphism $f:X\to Y$?

willbe stable under pullback/slicing, just like ordinary statements in the internal logic. So a statement which is not so stable cannot be expresed "internally" in such a way. $\endgroup$ – Mike Shulman Aug 23 '13 at 15:095more comments