The axiom of choice and connected groupoids Recall the two definitions of equivalence of categories:
Definition 1. An equivalence of categories is a quadruplet $(F, G, \alpha, \beta)$, where $F : \mathbb{C} \to \mathbb{D}$ and $G : \mathbb{D} \to \mathbb{C}$ are functors and $\alpha : G F \Rightarrow \textrm{id}_\mathbb{C}$ and $\beta : F G \Rightarrow \textrm{id}_\mathbb{D}$ are natural isomorphisms.
Definition 2. A weak equivalence of categories is a fully faithful functor $F : \mathbb{C} \to \mathbb{D}$ that is also essentially surjective on objects, i.e. for each object $d$ in $\mathbb{D}$ there exists an object $c$ in $\mathbb{C}$ and an isomorphism $d \to F c$ in $\mathbb{D}$.

Assuming the axiom of choice, one can show that a weak equivalence $F : \mathbb{C} \to \mathbb{D}$ extends to an equivalence of categories $(F, G, \alpha, \beta)$. On the other hand, it is clear that this principle is equivalent to the axiom of choice: indeed, if we have some family of non-empty sets $( X_i : i \in I )$, we may form the category $\mathbb{C}$ whose object set is $\coprod_{i \in I} X_i$, such that there exists a unique arrow between two objects if and only if they come from the same set $X_i$; taking $\mathbb{D}$ to be the discrete category on the indexing set $I$, we have an evident projection functor $F : \mathbb{C} \to \mathbb{D}$, and by construction it is a weak equivalence; on the other hand, any functor $G : \mathbb{D} \to \mathbb{C}$ fitting into an equivalence $(F, G, \alpha, \beta)$ must yield a family $( x_i : i \in I )$ where $x_i = G i \in X_i$. Notice also that the categories $\mathbb{C}$ and $\mathbb{D}$ constructed here are groupoids (indeed, for that matter, setoids).
Question. Suppose $\mathbb{C}$ is a connected groupoid, i.e. between any two objects there exists at least one (iso)morphism between them. Then, if $\mathbb{D}$ is the full subcategory of $\mathbb{C}$ spanned by any single object, then the inclusion $G : \mathbb{D} \hookrightarrow \mathbb{C}$ is automatically a weak equivalence. Do I need the axiom of choice to extend $G$ to an equivalence of categories?
 A: The following are equivalent over ZF.
AC6. The Cartesian product of a set of non-empty sets is non-empty.
AC7. The Cartesian product of a set of non-empty sets of the same cardinality is non-empty.
GWE. Every weak equivalence from a group to a small connected groupoid is an equivalence of categories.
The numbering of AC6 and AC7 is taken from Rubin's "Equivalents of the Axiom of Choice", where they are shown to be equivalent. That AC6 implies GWE is a special case of the proposition that under the axiom of choice, every weak equivalence of categories is an equivalence.
It remains to show that GWE implies AC7. Let $X_i$ be a family of non-empty sets of the same cardinality $X$. Let $\mathbb{D}$ be the permutation group of $X$ considered as a category with one object. Let $\mathbb{C}$ the the groupoid whose objects are indexed by $I$ and whose morphisms $i\to j$ correspond to bijections $X_i\to X_j$. Pick $i\in I$ and let $G$ send $X$ to $X_i$ according to some bijection of $X$ to $X_i$; this is a weak equivalence $\mathbb{D}\to\mathbb{C}$. By GWE there is an equivalence $(F,G,\alpha,\beta)$.
I'll argue that $F$ must be given by bijections $f_j:X_j\to X$. This part is a bit sketchy. Let $\pi$ be a transposition of $X_j$, that is, a permutation that exchanges two elements. There is a bijection $g:X_i\to X_j$, so $g^{-1}\pi g$ is a transposition, so $F(g^{-1}\pi g)$ is a transposition, so $F(\pi)=F(g)F(g^{-1}\pi g)F(g):X\to X$ is a transposition. An isomorphism $S_{X_i}\to S_X$ that sends transpositions to transpositions must be induced by a bijection of the underlying sets (I think).
Since $X$ is non-empty there exists $x\in X$. For each $j\in I$ let $y_j$ be the the unique element $y_j\in X_j$ such that $f_j(y_j)=x$. Then $y\in\prod_j X_j$. So $\prod_j X_j$ is non-empty as required.
