= Solution
A <decidable object in a topos> has a decomposition $A\times A=\Delta_A\amalg D_A$, with $D_A$ representing inequality. In the <internal logic of a topos>, equality on $A$ is decidable. These categorical complements behave well under <pullback>.
For a <subobject> $B\hookrightarrow A$, pull back the displayed decomposition along $B\times B\hookrightarrow A\times A$. The diagonal pulls back to $\Delta_B$, while $D_A$ pulls back to its complement. Hence \b[every <subobject> of a decidable object is decidable]; the <subobject> itself need not be complemented in $A$.
For two decidable objects, the diagonals of $A$ and $B$ give four disjoint summands of $(A\times B)^2$, according as each coordinate pair is equal or unequal. The both-equal summand is $\Delta_{A\times B}$, and the other three give its complement. The <terminal object> is decidable, so induction gives \b[closure under finite products], including the empty product.
For a family $(A_i)_{i\in I}$ of decidable objects with an existing <coproduct> $A=\coprod_iA_i$, products distribute over this <coproduct>, giving
$$
A\times A\cong\coprod_{i,j\in I}(A_i\times A_j).
$$
The <coproduct> injections in a topos are disjoint. The diagonal consists of $\Delta_{A_i}$ in each $i=j$ summand, and has complement
$$
\boxed{\left(\coprod_iD_{A_i}\right)\amalg\left(\coprod_{i\ne j}A_i\times A_j\right).}
$$
Consequently \b[every existing <coproduct> of decidable objects is decidable], including the <initial object>. In a <Grothendieck topos> all small <coproducts> exist. No assertion that arbitrary products preserve decidability is used.
Back to article page
