Exercise with adjunctions The category of the $M$-sets, that I'll denote $\mathbf{Set}^M$, has a symmetric cartesian structure. I already proved that if the functor $F:=-\times X$ has a right adjoint, it must be the functor $G:=\mathbf{Set}^M(M\times X,-)$; this is an $M$-set equipped with the following action: for $h\in \mathbf{Set}^M(M\times X,-)$, $m'\cdot h(m,x)=h(mm',x)$. I also know that the unity of the adjunction is, for an $M$-set $Y$, the $M$-morphism $\eta_Y$ such that $\eta_Y(y):(m,x)\mapsto (my,x)$.
My problem is that I can't prove the this is actually an adjunction. Firstly, if I have a $M$-morphism $Y\to \mathbf{Set}^M(M\times X,Z)$, how can I obtain a morphism $Y\times X\to Z$? I don't understand if there is an agile way to prove that $F\dashv G$, because proving directly the universal property of the unit seems quite complex. Any suggestion?
 A: My suggestion is to prove that there is a bijection on hom-sets $ \mathbf{Set}^M(Y \times X, Z) \simeq \mathbf{Set}^M(Y,\mathbf{Set}^M(M\times X,Z)).$ For $h: Y \times X \to Z$ define $\bar{h}: Y \to \mathbf{Set}^M(M\times X,Z)$ by $y \mapsto [(m,x) \mapsto h(my,x)].$ First, this is a map into $\mathbf{Set}^M(M\times X,Z)$ because $m'(m,x) = (m'm,m'x) \mapsto h(m'my,m'x) = m' \cdot h(my,x)$ by the equivariance of $h$. Second, $\bar{h}$ is $M$-equivariant: $m'y \mapsto [(m,x) \mapsto (mm'y,x)] = m'\cdot [(m,x) \mapsto h(my,x)].$
Conversely, for any $\bar{f}: Y \to \mathbf{Set}^M(M\times X,Z)$ define $f: Y \times X \to Z$ as $(x,y) \mapsto \bar{f}(y)(e,x).$ This is $M$-equivariant: $(mx, my) \mapsto \bar{f}(my)(e,mx) = \bar{f}(y)(m \cdot e,mx) = m \cdot (\bar{f}(y)(e,x)),$ where the first equality is the equivariance of $\bar{f}$ plus the action on morphisms that you've provided, and the second is the equivariance of $\bar{f}(y)$.
You can ensure that these maps are inverses of each other.
It may be hard to construct all the maps in the right way, with all the possible variations in which things can be multiplied. What I personally find helpful is understanding the construction of mapping objects in a sheaf category, which comes from essentially the same argument. (Sheaves are functors $D^{op} \to \mathbf{Set}$, and $\mathbf{Set}^M$ is functors from one-object category $\mathbf{BM}.$) Somehow having only one object makes it confusing because all arrows can be composed with each other from both sides. In the general case it is clearer, e.g. the form of the right adjoint you've described is immediate, and inserting $e$ in $\bar{f}(y)$ in the passage from $Y \to GZ$ to $FY \to Z$ comes from Yoneda lemma, where a natural transformation $yA \to X$ is determined by its action on $\operatorname{id}_A$: in our case $A$ is the object of $\mathbf{BM}$ and $\operatorname{id}_A$ is $e \in M.$
