What does it take to divide by $2$?

Solution 1:

There was a paper recently posted to arXiv about this question: Swan, On Dividing by Two in Constructive Mathematics.

It turns out that there are examples of toposes where you can't divide by two.

Solution 2:

(The following is not really an answer, or just a very partial one, but it's definitely relevant and too long for a comment.)

There is a theorem of Richard Friedberg ("The uniqueness of finite division for recursive equivalence types", Math. Z. 75 (1961), 3–7) which goes as follows (all of this is in classical logic):

For $A$ and $B$ subsets of $\mathbb{N}$, define $A \sim B$ when there exists a partial computable function $f:\mathbb{N}\rightharpoonup\mathbb{N}$ that is one-to-one on its domain and defined at least on all of $A$ such that $f(A) = B$. (One also says that $A$ and $B$ are computably equivalent or recursively equivalent, and it is indeed an equivalence relation, not to be confused with "computably/recursively isomorphic", see here.) Then [Friedberg's theorem states]: if $n$ is a positive integer then $(n\times A) \sim (n \times B)$ implies $A\sim B$ (here, $n\times A$ is the set of natural numbers coding pairs $(i,k)$ where $0\leq i<n$ and $k\in A$ for some standard coding of pairs of natural numbers by natural numbers).

To make this assertion closer to the question asked here, subsets of $\mathbb{N}$ can be considered as objects, indeed subobjects of $\mathcal{N}$, in the effective topos (an elementary topos with n.n.o. $\mathcal{N}$ such that all functions $\mathcal{N}\to\mathcal{N}$ are computable), in fact, these subobjects are exactly those classified by maps $\mathcal{N} \to \Omega_{\neg\neg}$ where $\Omega_{\neg\neg} = \nabla 2$ is the subobject of the truth values $p\in\Omega$ such that $\neg\neg p = p$; moreover, to say that two such objects are isomorphic, or internally isomorphic, in the effective topos, is equivalent to saying that $A$ and $B$ are computably isomorphic as above. So Friedberg's result can be reinterpreted by saying that if $A$ and $B$ are such objects of the effective topos and if $n\times A$ and $n\times B$ are isomorphic then $A$ and $B$ are.

I'm not sure how much this can be internalized (e.g., does the effective topos validate "if $A$ and $B$ are $\neg\neg$-stable sets of natural numbers and $n\times A$ is isomorphic to $n\times B$ then $A$ is isomorphic to $B$" for explicit $n$? and how about for $n$ quantified inside the topos?) or generalized (do we really need $\neg\neg$-stability?). But this may be worth looking into, and provides at least a positive kind-of-answer to the original question.