Let $F(X)$ be the free group on a set $X$. Classically, we can prove the statement:
$F(X) \cong F(Y)$ if and only if $|X|=|Y|$.
The proofs (that I have seen) consist of turning the group isomorphism into an isomorphism of free abelian groups, then an isomorphism of vector spaces by modding out by some $p$. Where we can deduce that isomorphic vector spaces have bijective basis sets.
The last part of this proof uses AC. I came across Kleppmann - Generating sets of free groups and the axiom of choice, which proves that ZF + boolean prime ideal theorem can prove this, therefore it is weaker than AC.
I am interested in knowing how true this statement is constructively. I.e. are uses of excluded middle and choice (or rather statements weaker than choice) necessary to prove it?