If $A,B$ are sets such that $\textbf{2}\times A\cong \textbf{2}\times B$, then $A\cong B$.Theorem 1[ZFC, classical logic]: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 1 still holds in ZF with classical logic.Theorem 2:This is less trivial and explained in Section 5 of Division by Three – however, though the construction does not involve any choices, it

doesinvolve the law of excluded middle.

Are thereQuestion:intuitionisticset 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?

EditSee also the related question Does $A\times A\cong B\times B$ imply $A\cong B$? about ‘square roots’

**Answer**

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.

**Attribution***Source : Link , Question Author : Hanno , Answer Author : aws*