How to express in categorical language that in some toposes not all complex numbers have square roots I'm trying to improve my ability to translate constructive logic into the category theoretical language of topos theory. So far, my understanding of constructive logic has been rather naive. I know that rigorous foundations can be found in HoTT (but not in its book form) and topos theory, but I don't know how to actually use these.
It's known that there exist toposes, like $\operatorname{Sh}(\mathbb C)$, in which the sentence:
$$\forall z \in \mathbb C. \exists w \in \mathbb C. w^2 = z$$
is false, where $\mathbb C$ is defined to be the product of the Dedekind reals with themselves. I suspect this is equivalent to saying that the natural projection from ordered pairs of complex numbers to unordered pairs is not surjective. In other words, I suspect that this is equivalent to saying that the natural projection $p:\mathbb C^2 \to \mathbb C^2/\pi$ is not surjective (where $\pi : \mathbb C^2 \to \mathbb C^2$ is the morphism which swaps the two components of its input). This would be strange, because $p$ is supposedly a coequaliser (between $\pi$ and $\operatorname{id}_{\mathbb C^2})$, and a coequalising morphism is always an epimorphism, which should also be a surjection (internal to the topos). How would I express this correctly in categorical language?
The motivation for my interpretation in terms of unordered pairs is that the square roots of a complex number form an unordered pair (conceptually speaking). I suspect that the issue surrounding existence of square roots lies in choosing an element from this unordered pair. But maybe I'm barking up the wrong tree.
 A: No the problem isn't quite choosing an element from an unordered pair, even if I agree with you that it somehow feel like it is. The map you are talking about is indeed always an epimorphism.
One way to answer your question is to say that the map $z \mapsto z^2 : \mathbb{C} \to \mathbb{C}$  is not (always) an epimorphism.
Indeed if you look at example you suggest $\operatorname{Sh}(\mathbb{C})$, then $\mathbb{C}$ is the sheaf of continuous complex valued functions and the fonction $z \mapsto z^2$ takes such a function and squares it.
Now one can show that around the point $ 0 \in \mathbb{C}$ the (germ of the) section $z \mapsto z$ cannot be written as the square of the germ of a continus function.
I remember there is a way (or rather several equivalent ways) to define a modified version of $\mathbb{C}^n / S_n$ so that this sheaf is equivalent to the sheaf of unit polynomials of degree $n$ which formalizes the intuition you are talking about in your question, but I can't quite remember how it works. So I prefer not to say too much, but I'm sure someone else can comment or give a reference about this.
E.g. one way this works is that the map from $\mathbb{C}^n \to \mathbb{C}^n$ that sends $n$ complex numbers $(x_1, \dotsc, x_n)$ to the (coefficients of the) unit polynomial $(t-x_1) \dotsb (t-x_n)$ seen as a map of locales, induces an isomorphism of locales $\mathbb{C}^n/S_n \simeq \mathbb{C}^n$. But there are less localic way to say this that might be closer to what you have in mind.
Edit: another approach that I now remember (and I remember reading about it somewhere, maybe someone can say where!). If you endow the set $\mathbb{C}^n/S_n$ with the quotient distance then you can't prove constructively that it is a complete metric space. Here the problem is about chosing an element from an unordered pair, but more precisely with doing it for a whole set of unordered pairs at once, so it require some form of choice. So, because of this, you can consider its metric completion $\overline{\mathbb{C}^n/S_n}$ (in the sense of Cauchy filters) and we can show constructively that the map described above induces a homeomorphism $\overline{\mathbb{C}^n/S_n} \simeq \mathbb{C}^n$. This allows us to show that the axiom of countable choice is enough to show that every complex polynomial admits a root, as countable choice is all you need to prove that $\mathbb{C}^n/S_n$ is complete (though there might be a more direct proof of this).
