What does it take to divide by $2$?

Theorem 1 [ZFC, classical logic]: If $A,B$ are sets such that $\textbf{2}\times A\cong \textbf{2}\times B$, then $A\cong B$.

That's because the axiom of choice allows for the definition of cardinality $|A|$ of any set $A$, and for $|A|\geq\aleph_0$ we have $|\textbf{2}\times A|=|A|$.

Theorem 2: Theorem 1 still holds in ZF with classical logic.

This is less trivial and explained in Section 5 of Division by Three - however, though the construction does not involve any choices, it does involve the law of excluded middle.

Question: Are there intuitionistic set theories in which one can prove $$\textbf{2}\times A\cong \textbf{2}\times B\quad\Rightarrow\quad A\cong B\quad\text{?}$$

For example, is this statement true in elementary topoi or can it be proved in some intuitionistic type theory?

In his comment below Kyle indicated that the statement is unprovable in some type theory - does somebody know the argument or a reference for that?

Edit See also the related question Does $A\times A\cong B\times B$ imply $A\cong B$? about 'square roots'

• JMoravitz: In intuitionistic logic, the contrapositive of a statement does not imply the statement itself; i.e. $\neg B \Rightarrow \neg A$ does not imply $A \Rightarrow B$. (It only implies $A \Rightarrow \neg\neg B$, which is intuitionistically a strictly weaker statement.) Also, I don't understand in which way the contrapositive is "trivially true"; note that $A$ and $B$ may be arbitrary (maybe infinite) sets. – Ingo Blechschmidt Nov 17 '14 at 9:37
• @HandeBruijn That depends a lot on the exact variety of constructive mathematics. In particular, intuitionistic set theories often make use of infinity in some way. – Mario Carneiro Jan 4 '15 at 11:24
• $\aleph_0$ certainly does exist in constructive mathematics, which although inspired in part by Brouwer is not very closely related to his exact form of intuitionism. The natural reading of the question is how to prove the result in a theory like IZF of CZF, both of which can handle transfinite ordinals just fine. – Carl Mummert Jan 5 '15 at 0:22
• @Hanno: if no answer is obtained here, I believe this question would fit on MathOverflow, where it would reach a different set of eyes. – Carl Mummert Jan 7 '15 at 16:21
• @ConorO'Brien: Yes that's fine and proves $\Leftarrow$, but the question asks whether one can also show $\Rightarrow$ from intuitionistic principles. – Hanno Jan 8 '15 at 21:17

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.

(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.