This is similar to What does it take to divide by $2$? about $(A\sqcup A\cong B\sqcup B)\Rightarrow A\cong B$ which is valid in $\textsf{ZFC}$ by using cardinalities and also in $\textsf{ZF}$ by some combinatorial argument, but where it remained unclear whether constructive arguments suffice.
This questions concerns products instead of disjoint union, so:
Question: Does $\textsf{ZF}$ prove the implication $(A\times A\cong B\times B)\Rightarrow A\cong B$?
If yes: is anything known in case of intuitionistic set/type theories?
This is a generalization of tetori's nice answer, which in fact shows that this assumption implies the axiom of choice.
Proof. We calculate: $$(a+b)^2=a^2+b^2+2\cdot a\cdot b=a^2+b^2+a\cdot b=a+b+a\cdot b=a\cdot b$$ The second equality comes from the fact that $a\leq a+a=2\cdot a\leq a^2=a$, the last one follows from the same reasoning. $\qquad\square$
Proof. $(2^a)^2=2^{a+a}=2^a.\qquad\square$
(The proof appears in Jech, The Axiom of Choice, Lemma 11.6; and there are generalizations of this lemma out there.)
Proof. We will show that if $\kappa$ is an aleph number, then $2^\kappa$ is an aleph number. This implies the axiom of choice, by a theorem of Rubin and Rubin from 1963.
Let $\lambda=\aleph(2^\kappa)$, the least aleph cardinal such that $\lambda\nleq 2^\kappa$. Then $2^\kappa$ and $\lambda$ satisfy the hypothesis of Lemma I, and therefore $(2^\kappa+\lambda)^2=2^\kappa\cdot\lambda=(2^\kappa)^2\cdot\lambda^2=(2^\kappa\cdot\lambda)^2$. By the uniqueness of the square root, $2^\kappa+\lambda=2^\kappa\cdot\lambda$, and by Tarski's lemma $2^\kappa$ and $\lambda$ are comparable.
Finally $\lambda\nleq2^\kappa$, therefore $2^\kappa<\lambda$, so $2^\kappa$ is an aleph number. $\qquad\square$
(I will remark here that the final proof uses $\sf ZF$ in a substantial way. In $\sf ZFA$, where atoms are allowed, having $2^\kappa$ as an aleph does not imply the axiom of choice.)