# 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’