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.