# Prove that a "tensor product" principal $G$-bundle coincides with a "pullback" via topos morphism

From Moerdijk, Classifying spaces and classifying topoi, page 22. Consider a right $G$-set $S$ with the discrete topology. Let $E$ be a principal $G$-bundle over the topological space $X$. One can construct another principal $G$-bundle $S\otimes_G E$ as the quotient of $S\times E$ by the equivalence relation $(s\cdot g,e)\sim(s, g\cdot e)$. Moreover, one can construct another right $G$-set substituting $E$ by the set $\tilde G$, which is $G$ with the right multiplication action (but which, being $G$, supports also left multiplication and so the relation is well defined). So consider an arbitrary topos morphism $f:Sh(X)\longrightarrow \mathcal BG$, where the domain is the topos of sheaves on $X$ and the codomain is the topos of right $G$-sets.

The aim is to prove that, for any $S$,

$$(S\otimes_G\tilde G)\otimes_G f^*(\tilde G)\cong f^*(S \otimes_G\tilde G);$$

from this it will follow that, since $S\otimes_G\tilde G\cong S$, then

$$S\otimes_G f^*(G)\cong f^*(S \otimes_G\tilde G)\cong f^*(S)$$

and so the functors $-\otimes_G f^*(G)$ and $f^*$ coincide.

Can someone give me a hint in order to prove the key isomorphism? I tried with universal properties, but I find some problems in dealing with maps from $G$-sets to sheaves, which are not very natural unless they are actually $f^*$...

It's easier to just prove directly that $f^{\ast}(-)$ coincides with $(-) \otimes_G f^{\ast}(G)$. The point is that both of these functors are cocontinuous in their argument, and right $G$-sets is (freely) generated under colimits by $G$. So to show that they agree it suffices to show that they agree at $G$. Plugging in $G$ gives $f^{\ast}(G)$ and $G \otimes_G f^{\ast}(G) \cong f^{\ast}(G)$ respectively.