Skip to main content
2 of 2
typo
David Spivak
  • 8.7k
  • 1
  • 28
  • 64

A different way to describe the same answer that Zhen and Todd arrived at is to work in the internal logic of $E$. That way we may pretend that $f_*$ is the global sections functor $\mathrm{Hom}(1,-) : D \to \mathrm{Set}$, as long as we treat $\mathrm{Set}$ constructively. Then we have the components of a putative natural transformation

$$ \mathrm{Hom}(1,P A) \to P(\mathrm{Hom}(1,A)) $$

which, under the universal property of power objects $ \mathrm{Hom}(1,P A) \cong \mathrm{Sub}(A)$, sends a subobject $S\rightarrowtail A$ in $D$ to the set of all global sections $1 \to A$ which factor through it. The naturality square for $p:A\to B$ requires that if we take the direct image subobject $p_!(S)$, then a global section of $B$ factors through $p_!(S)$ just when it lifts to some global section of $A$ factoring through $S$. It's easy to see that this is the same as asking that $1\in D$ be projective, which is equivalent to saying that the global sections functor $f_* = \mathrm{Hom}(1,-)$ preserves epimorphisms.

Mike Shulman
  • 66.8k
  • 7
  • 162
  • 368