ct.category theory - Are all coproducts of 1 in a topos distinct ?

At least if you're talking about finite coproducts, then the answer is yes. If $nle m$, then we have a canonical inclusion $sum_{i=1}^n 1 hookrightarrow sum_{j=1}^m 1$, which is in fact a complemented subobject with complement $sum_{k=1}^{m-n} 1$. If this inclusion is an isomorphism, then its complement is initial, and hence (assuming the topos is nontrivial) $n=m$. Now if we have an arbitrary isomorphism $sum_{i=1}^n 1 cong sum_{j=1}^m 1$, then composing with the above inclusion we get a monic $sum_{i=1}^m 1 hookrightarrow sum_{j=1}^m 1$. However, one can show by induction that any finite coproduct of copies of $1$ in a topos is Dedekind-finite, i.e. any monic from it to itself is an isomorphism. (See D5.2.9 in "Sketches of an Elephant" vol 2.) Thus, the standard inclusion is also an isomorphism, so again $n=m$.

• Next co.combinatorics - Is there a natural family of languages whose generating functions are holonomic (i.e. D-finite)?
• Previous the sun - Solar / lunar positions in ECEF using SOFA C libraries