From Emily Riehl, Category theory in context:
Exercise 1.5.vii. Let $\mathbf{\mathsf G}$ be a connected groupoid and let $G$ be the group of automorphisms at any of its objects. The inclusion $\mathbf{\mathsf B} G \hookrightarrow \mathbf{\mathsf G}$ defines an equivalence of categories. Construct an inverse equivalence $\mathbf{\mathsf G} \hookrightarrow \mathbf{\mathsf B} G$.
Remark: $\mathbf{\mathsf B} G$ denotes the category associated to the group $G$.
The only possible object assignment is $c \mapsto \epsilon$ for every object $c$ in $\mathrm{\mathsf G}$.
Using the axiom of choice I can get a family of isomorphisms $\alpha_c \colon \epsilon \rightarrow c$, and then define the arrow assignment $x \mapsto \alpha_d^{-1} \circ x \circ \alpha_c$ for every morphism $x \colon c \rightarrow d$ in $\mathbf{\mathsf G}$.
This defines an inverse equivalence.
But is it possible to find an inverse equivalence without using AC?
Best Answer
Just to sum up the findings in the comments, we have
All of this is over ZF. It can be done in slightly weaker systems, but whatever.
As @Max notes, we have
Proof.
Assume that $\mathbf{\mathsf B}G \hookrightarrow \mathbf{\mathsf G}$ is an equivalence for every connected groupoid $\mathbf{\mathsf G}$. Let $(X_i)_{i \in I}$ be a collection of nonempty sets all with the same cardinality. Consider the groupoid $\mathbf{\mathsf G}$ whose objects are $(X_i)_{i \in I}$ and let $\hom(X_i, X_j)$ be the set of bijections from $X_i$ to $X_j$.
If $I$ is empty, there's a trivial choice function $I \to \bigcup_{i \in I} X_i$ (namely the identity, since both these sets are the empty set). So from here on, assume $I$ is nonempty. $\mathbf{\mathsf G}$ is then connected since it is inhabited and any two objects are connected by a morphism. So by hypothesis, the inclusion $\mathbf{\mathsf B}G \hookrightarrow \mathbf{\mathsf G}$ is an equivalence, so in particular, we have a natural (in $X \in \mathbf{\mathsf G}$) isomorphism $\alpha_X : X_{i_0} \to X$, where $X_{i_0}$ is the image of $\epsilon$ in the inclusion $\mathbf{\mathsf B}G \hookrightarrow \mathbf{\mathsf G}$. Then since $X_{i_0}$ is nonempty, there exists $x_0 \in X_{i_0}$. $i \mapsto \alpha_{X_i}(x_0)$ is then our desired choice function.
Conversely, suppose that for every collection of nonempty sets $(X_i)_{i \in I}$, such that $X_i \simeq X_j$ for all $i, j \in I$, there is a choice function $I \to \bigcup_{i \in I} X_i$. Following your approach, we can define a functor $\mathbf{\mathbf{\mathsf G} \to \mathsf B}G$ whose value at any object is $\epsilon$. As noted, the morphisms are trickier. We can fix an object $X_0 \in \mathbf{\mathsf G}$ (since $\mathbf{\mathsf G}$ is connected, it's inhabited). Then each set $\hom(X_0, X)$ is inhabited (by assumption of connectedness) and they are all bijective with each other: $\hom(X_0, X) \simeq \hom(X_0, Y)$ via postcomposition with a bijection $X \to Y$. So by hypothesis, we have a choice function $\alpha_X \in \hom(X_0, X)$.
We can use $\alpha$ to define our functor on morphisms in $\mathbf{\mathsf G}$. As you said, choosing $f \mapsto \alpha_Y^{-1} \circ f \circ \alpha_X$ works. Functorality follows easily. The fact that this is our inverse equivalence is a little harder, but not too difficult.
It turns out that the weaker form of choice used above is equivalent to the full axiom of choice. The reference for this is Rudin and Rudin's Equivalents of the Axiom of Choice, II. Specifically, AC 7 is (essentially) our version of AC.
Proof.
Assuming the axiom of choice, proving the statement is trivial, so we'll focus on the other direction. Assume that for every collection of nonempty sets $(X_i)_{i \in I}$, such that $X_i \simeq X_j$ for all $i, j \in I$, there is a choice function $I \to \bigcup_{i \in I} X_i$.
The case $I = \emptyset$ is easy (as usual the identity function works as a choice function), so take $I$ to be nonempty.
Consider the set $Y := (\bigcup_{i \in I} X_i)^\omega$, that is, the set of functions from the natural numbers to the union of the $X_i$. We want to prove that this is bijective with $Y \times X_i$. For one direction, we have an injection $Y \to Y \times X_i$ which pairs up $y \in Y$ with a fixed element of $X_i$ (which exists since $X_i$ is non-empty). For the other direction, consider the map $Y \times X_i \to Y$ which takes $(f, x)$ to the function $g(0) = x$, $g(n + 1) = f(n)$. This is injective since we can recover the original function (via $g(n + 1)$) and the point $x$ (via $g(0)$). So by the Cantor-Schoeder-Berstein theorem, $Y \times X_i$ is bijective with $Y$. Hence, for $i, j \in I$ $Y \times X_i$ is bijective with $Y \times X_j$. Each of these sets is nonempty since we can take the constant function at some element of $\bigcup_{i \in I} X_i$ (which is nonempty because $I$ is nonempty and each $X_i$ is nonempty). So, we can apply our statement and get a choice function for $(Y \times X_i)_{i \in I}$. Composing with the projection $Y \times X_i \to X_i$, we get a choice function for $(X_i)_{i \in I}$.
Many experts are of the opinion that without the axiom of choice, a more appropriate notion of functor is an anafunctor. An anafunctor is essentially allowed to map objects "up to isomorphism". For example, to have an inverse anafunctor equivalence, we'd only need an essentially surjective, fully faithful functor between the categories, which is the "right" notion of equivalence of categories.