For which "permutation groups" is the sign homomorphism well-defined constructively? Let $X$ be a finite set. I now have a favorite construction of the sign homomorphism $Sym(X) \to C_2$. But perhaps it shouldn't be my favorite construction.
After discussion with the experts, I've learned that Poonen's construction only works constructively if $X$ is assumed to be cardinal-finite in the following sense. I refer to the nlab page for finite object:
Definition: Let $X$ be an object of a topos. Say that $X$ is a finite cardinal if it is a proper initial segment of $\mathbb N$, and cardinal-finite if it is equipped with a bijection to a finite cardinal. (This is the definition under "external version" on the nlab page.)
The reason is that Poonen's construction involves picking out the index-2 subgroup $G < C_2^{\binom{X}{2}}$ defined by $G = \{(x_e)_{e \in \binom{X}{2}} \mid \sum_e x_e = 0\}$. Here $\binom{X}{2}$ is the set of 2-element subsets of $X$. The point is that in order to sum over $\binom{X}{2}$, it needs to be a cardinal-finite set, which in turn basically means that $X$ itself should be cardinal-finite.
Here is an example suggesting that this may not be the optimal generality, pointed out to me by Andrew Swan. Let $G$ be a discrete group, and let $\mathcal E$ be the topos of $G$-sets. Then a cardinal-finite object $X$ in $\mathcal E$ is a finite set equipped with the trivial $G$-action. In this case, $Sym(X)$ is the usual symmetric group on $X$, again equipped with the trivial $G$-action. And indeed, the sign permutation $Sym(X) \to C_2$ is well-defined ($C_2$ is the usual group, with trivial $G$-action). But more generally, if $X$ is any finite set with (possibly nontrivial) $G$-action, then although the $G$-action on $Sym(X)$ is generally nontrivial, via $(g \cdot f)(x) = g \cdot (f(g^{-1} \cdot x))$, it's plain from this formula that each $g \in G$ acts via an even permutation on $Sym(X)$, so that the sign permutation $Sym(X) \to C_2$ is still well-defined! Such an object $X$ is locally cardinal-finite in the following sense:
Definition: Let $X$ be an object of a topos. Say that $X$ is locally cardinal-finite if it becomes cardinal-finite after pullback to some well-supported slice topos. (This is Definition 2.1 on the nlab page above).
This suggests that answer to the following might be yes, even though I don't know a proof:
Question 1: Let $X$ be a locally cardinal-finite object of a topos $\mathcal E$. Then does the internal group object $Sym(X) \in Grp(\mathcal E)$ admit a nontrivial "sign" homomorphism $Sym(X) \to C_2$ in $Grp(\mathcal E)$?
I believe the definition of local cardinal-finiteness is equivalent to saying in the internal logic of $\mathcal E$ that there merely exists a bijection from $X$ to a finite cardinal. So I think the following version of the question is more-or-less equivalent:
Question 2: Work in a constructive metatheory. Let $X$ be a set for which there exists a bijection from $X$ to a finite cardinal. Then does there exist a nontrivial "sign" homomorphism $Sym(X) \to C_2$?
Question 3: Perhaps I haven't identified the right class of "finite" objects to work with for the sign to exist constructively. Is there some other constructive notion of "finiteness" more general than cardinal-finiteness for which the "sign" homomorphism is well-defined?
 A: The answer to question 2 as phrased is trivially yes: since there exists such a bijection, choose one, and use it to define a sign homomorphism.  But I assume what you meant to ask is, if there exists a bijection from $X$ to a finite cardinal, can we construct a specified sign homomorphism?  (In the language of type theory, we're switching from a propositionally truncated $\exists$ to an untruncated $\Sigma$.  It's harder to formulate this exactly in first-order logic.)  This is what's equivalent to question 1 (the way you phrased question 2 originally would be equivalent to asking whether there is such a sign homomorphism in some well-supported slice).
However, the answer to these questions is also yes, because the sign homomorphism for finite cardinals is unique, and unique objects can always be specified.  In the language of type theory, the "type of sign homomorphisms" is always a proposition, so we can eliminate into it out of a propositionally truncated type like "there exists a bijection to a finite cardinal" without needing to truncate it first.
(The standard proof of uniqueness of the sign homomorphism should go through constructively.  For instance, since ${\rm Sym}(X)$ is generated by transpositions, and any two transpositions are conjugate, any such homomorphism is determined by a single value, hence there can be at most one nontrivial such.)
