Does Tarski's squaring theorem imply Axiom of Choice in NFU? I'm trying to see which results from mainstream set theory (ZF) about Axiom of Choice can be proved in New Foundations with Urelements (U is added simply because otherwise Axiom of Choice doesn't hold). Currently I'm stuck proving Tarski's theorem, that the claim
"for every infinite set $A$, there exists a bijection between $A\times\{*\}$ and $A\times A$"
implies AC (in fact, Zermelo's wellordering theorem). All the proofs I've seen so far (see e.g. https://en.wikipedia.org/wiki/Tarski%27s_theorem_about_choice#Proof) seem to rely on the existence of Hartogs' ordinal for a given set $X$ (an ordinal so big that there is no injection from it to $X$), but that's obviously not going to work in a theory with universal set, since $V$ doesn't have a Hartogs' ordinal.
I am aware that all I need is one injection from $V$ to $Ord$ (set of all ordinals), but so far it has eluded me. I can't even build it recursively on rank since the universe is not well-founded ($V\in V$).
Does anyone have any ideas on how to proceed? Could it possibly be that the implication doesn't hold?
 A: The proof in $\sf NF$ is pretty much the same as in $\sf ZF$, but one needs to make some adjustments to assure stratification.
First note that if you can well order $\iota^2``V = \{ \iota^2 `x  \mid x \in V \}$, where $\iota^2 ` x  = \{\{x\}\}$, then you can easily well order $V$ via Stratified comprehension. To see that, let $R$ be a well ordering on $\iota^2 ``V$, then we can define a well ordering $R^*$ on $V$, as: $$ R^*= \{ \langle a,b \rangle \mid  \langle \iota^2 `a , \iota^2`b \rangle \in R   \} $$
Now in Forster's book: Set Theory with a Universal Set: Exploring an Untyped Universe, 2.2 Cardinal and ordinal arithmetic, Remark 2.2.2, Theorems 2.2.3, 2.2.4, pp: 46-48.
To quote [terminology modified], he concludes:

"that any aleph $ < |Ord| $ is $T^2$ of something, and that $ |Ord|$ itself is  not $T^2$ of anything. The notation '$\aleph(\alpha)$' denotes the least aleph not $\leq \alpha$,  Hartogs' aleph function. Thus $\sf |Ord| \not \leq |\iota^2 ``V|$, and $\sf |Ord| = \aleph (| \iota^2`` V  |)$"

Just to clarify, $|Ord|$ here which is usually denoted as $\Omega$, the order type of $Ord$, cannot be $T^2 \alpha$ for some $\alpha$ because by then $\alpha$ would be an ordinal not in $Ord$. Also $\Omega \not \leq |\iota^2 ``V|$ because if not so, then there will be an injection from $Ord$ to $\iota^2``V$, and a well ordering $R$ on the range of that injection that would be an element of $\Omega$, and so the order type of $R^{\iota^-2} = \{\langle a,b \rangle \mid \ \langle \iota^2 a, \iota^2 b \rangle \in R \}$ would an ordinal $\alpha$ such that $\Omega=T^2 \alpha$.
Now, simply you can use $Ord$ itself as the well ordered set to unite with $\iota^2 `` V$, and run Tarski's' argument, to prove the existence of a well ordering on $\iota^2 ``V$.
