Recall the notion of **groupoid** (Wikipedia, nLab). An important construction of groupoids is as "action groupoids" for group actions. Namely, let $X$ be a groupoid and $G$ a group, and suppose that $G$ acts on $X$ by groupoid automorphisms. Then we can form a new groupoid $X//G$, which has as objects the objects of $X$, but the morphisms include, in addition to the original morphisms of $X$, a morphism $x \overset g \to gx$ for each $g\in G$ and $x\in X$. The composition of morphisms is well-defined if the action is by groupoid automorphisms. (When $X$ is a set, then $X//G$ is equivalent to the skeletal groupoid whose objects are the elements of the "coarse" quotient $X/G$, and with ${\rm Aut}(\bar x) = {\rm Stab}_G(x)$.)

(Probably there is a fancier construction, in which the conditions on the word "group action" be relaxed to an "action" up to specified natural isomorphism, and then $G$ could act on $X$ by autoequivalences, rather than autoisomorphisms, but this generalization won't concern me.)

Let $1$ denote the one-point set, thought of as a groupoid with only identity morphisms. Then any group $G$ acts uniquely on $1$, and so we have the groupoid $1//G$. In general, although $X\times 1 \cong X$, we do not have $X \times (1//G) \cong X//G$ for arbitrary $G$-actions on $X$ unless the action is trivial. (Here $\times$ denotes the **groupoid product**, which is just what you think it is.) However, the construction provides natural bijections between the objects of $X//G$ and the objects of $X \times (1//G)$, and between the morphisms of $X//G$ and the morphisms of $X \times (1//G)$.

Question:Is there some sort of "semidirect" or "crossed" product of groupoids, which presumably depends on extra data, so that we do have $X//G \cong X \rtimes (1//G)$? By which I mean, what is the correct notion of "action" of a groupoid $Y$ on a groupoid $X$ and what is the corresponding correct notion of $X \rtimes Y$?

I see that the page semidirect product in nLab defines $X \rtimes G$ as something closely related to $X//G$. But clearly this ought to be called $X\rtimes (1//G)$, but then I do not know what the right definition for $X\rtimes Y$ is, hence the question. And really I'd like to know about a "double crossed product" $X\bowtie Y$.

My motivation for this question is from my answer to Do rational numbers admit a categorification which respects the following “duality”?.