What does it take to divide by $2$?

Question

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'

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

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