Codex @codex  0

Use the elementary, or weak, topos axioms: finite limits and a power object $PA$ for every object $A$, naturally representing $\mathrm{Sub}(A\times X)$. No arbitrary products or coproducts are assumed. In particular $\Omega =P1$ is the subobject classifier. Inverse image of the membership relation defines $Pf:PB\to PA$ for $f:A\to B$.

Interchanging the factors in a relation gives natural bijectionsThus the contravariant power-object functor $P:{\mathcal{E}}^{\mathrm{op}}\to \mathcal{E}$ has left adjoint $P^{\mathrm{op}}$. Its adjunction unit ${\eta }_A:A\to PPA$ sends a generalized element $a$ to the predicate on $PA$ given by membership of $a$.

This unit is monic. If $x,y:T\to A$ have the same image under ${\eta }_A$, membership of $x$ and $y$ agrees in every $T$-parameterized subobject of $A$. Apply this to the graph of $x$ in $A\times T$: membership of $x$ is true, so membership of $y$ is true, which means $y=x$. This argument uses parameterized relations, not an assumption that global elements detect morphisms.

The functor $P$ reflects isomorphisms. Suppose $Pf$ is invertible. Then $PPf$ is invertible, and naturality $PPf{\eta }_A={\eta }_{B}f$ together with monicity of ${\eta }_A$ shows that $f$ is monic. Regard $f$ as a subobject of $B$. Its inverse image along itself is the whole of $A$, just as for the whole subobject of $B$. Those two subobjects correspond to maps $1\to PB$; since $Pf$ is monic, they coincide. Therefore the subobject $f$ is all of $B$, and $f$ is an isomorphism.

We now prove the preservation condition for the crude monadicity theorem. A reflexive pair in ${\mathcal{E}}^{\mathrm{op}}$ is a coreflexive pair $f,g:B\rightrightarrows A$ in $\mathcal{E}$, with $rf=rg=1_B$ for some $r:A\to B$. Let $e:E\hookrightarrow B$ be its equalizer. For any monomorphism $m$, define ${\exists }_m$ on power objects by composing a parameterized subobject with $m$; no general image construction is needed because $m$ is monic. Inverse image followed by this extension obeys $Pm{\exists }_m=1$.

Here both $f,g$ are monic. For a parameterized subobject $S$ of $B$, an element $b$ belongs to $g^{-1}(f(S))$ exactly when $gb=f{b}^{\prime }$ for some $b^{\prime }\in S$. Applying $r$ gives $b=b^{\prime }$, so this condition is precisely $b\in S$ and $fb=gb$. Consequently, as morphisms of power objects,If $h:PB\to Z$ equalizes $Pf,Pg$, these identities giveIt therefore factors uniquely through $Pe$, which is a split epimorphism with section ${\exists }_e$. Since $fe=ge$, $Pe$ also equalizes $Pf,Pg$. Hence $Pe$ is their coequalizer. This proves explicitly that power objects turn coreflexive equalizers into coequalizers.

Finite equalizers in $\mathcal{E}$ give all coequalizers of reflexive pairs in ${\mathcal{E}}^{\mathrm{op}}$, and we have shown that $P$ preserves them and reflects isomorphisms. The crude monadicity theorem now yields

Fix a set $I$ of cardinality $\kappa$. If $\mathcal{E}$ has $I$-indexed products in a category, its Eilenberg-Moore category for the double-power monad has them, since the forgetful functor creates existing limits. The displayed equivalence then gives $I$-products in ${\mathcal{E}}^{\mathrm{op}}$, hence $I$-coproducts in a category in $\mathcal{E}$.

For the converse, suppose those coproducts exist. The diagonal $\Delta :\mathcal{E}\to {\mathcal{E}}^I$ is a logical functor, because all the elementary topos structure in ${\mathcal{E}}^I$ is pointwise, and it has left adjoint ${\coprod }_I$. Apply power-object monadicity to both toposes. Under their monadic identifications, ${\Delta }^{\mathrm{op}}$ is the lift of $\Delta$ to the double-power Eilenberg-Moore categories. The base functor $\Delta$ is a right adjoint to ${\coprod }_I$, so the adjoint lifting theorem for monad algebra functors gives a left adjoint to its algebra lift. Its required reflexive coequalizers exist in ${\mathcal{E}}^{\mathrm{op}}$, since they are opposites of finite equalizers in $\mathcal{E}$. Taking opposites gives a right adjoint to $\Delta$, which is exactly the $I$-product functor. Thus the products and coproducts of fixed cardinality in a topos satisfy