#constructivemath I **think** I've got a good proof that "every nonempty set has a group structure" -> #axiomofchoice , but I'd like to run it by the community. in particular, I'm not using the Hartogs number anywhere, and I'm not finding my proof in my brief Google search, so I'd like a sanity check on this.

well, let's look at a family of nonempty sets \( \{A_i\}_{i \in I} \), WTS \( \prod_I A_i \) is nonempty. each of the \( A_i \)'s has a group structure, heck, let's name it \( A'_i \) perhaps, and look at the product group \( \prod_I A'_i \) (here's the step where I feel slightly queasy, but since group products are fine constructively (or at least in Agda), I think it's ok...). but now, \( \prod_I A'_i \) has as its underlying set \( \prod_I A_i \), and by our group structure (and slight abuse of notation) this set is pointed by the identity element \( (e_i)_{i \in I} \in \prod_I A_i \) and we're done (?)