Homotopy cardinality of weak quotients Let $G$ be a group (regarded as a one-object groupoid) acting on a groupoid $X$ (i.e.: a functor $F: G \to \mathsf{Groupoids}$ sending the unique object of $G$ to $X$). Denote with $X//G$ the “weak quotient” of such an action, i.e. the Grothendieck construction of the functor $F$.
It seems to be well-known that the homotopy cardinality of the weak quotient $X//G$ is given by the formula
$$
|X//G| = \frac{|X|}{o(G)}\text{,}
$$
where $|X|$ is the homotopy cardinality of $X$ and $o(G)$ is the order of $G$ (of course this makes sense only when $|X|$ and $o(G)$ are finite). However, I wasn't able to find any recorded proof of this fact (maybe it's very simple and I can't see it). Can someone sketch a proof or give some reference where I can find one?
 A: If $p : E \to X$ is an $n$-sheeted covering of groupoids, then $|E| = n\cdot |X|$; apply this result to the case of the fibration of elements $p : X/\!\!/G \to G$, just reminding that that this map isn't a covering map unless the action of $G$ is free.
However, you can replace $p$ by a covering map $\tilde p$ that is sort of a fibrant replacement for $p$, in the category ${\bf Gpd}/X$; now $|G|=1/o(G)$ and $\tilde p$ has $|X|$ sheets!
A: I think the key point is that we know the cardinality of a semi direct product, which is the group theoretic background of the homotopy quotient. For instance, suppose $X$ is skeletal, so that isomorphic objects are equal, and that the action is transitive. Then all objects of $X$ have the same automorphism group $H$. By the usual orbit-stabilizer theorem, the stabilizer $K$ of some $x\in X$ has cardinality $|G|/|\mathrm{ob} X|$. Then $X//G$ has one isomorphism class of object, whose automorphism group $H\rtimes K$. The homotopy cardinality of $X$ is $|G|/(|K||H|)$ and of $X//G$ is $1/(|H||K|)$, as desired.
