Functor from orbit category to Top Given a topological group $G$, define the orbit category $\mathcal{O}(G)$ as the category whose objects are the $G$-sets $G / H$, and whose morphisms are the $G$-equivariant maps. Peter May's book has the following lemma on page 31:

Let $X$ be a $G$-space. Then passage to orbit spaces defines a functor $X / (-) : \mathcal{O}(G) \to \textbf{Top}$.

This functor sends $G / H$ to $X / H$, and sends a $G$-equivariant map $\alpha : G / H \to G / K$ given by $gH \mapsto g\gamma H$ (note that every $G$-equivariant map is of this form) to the continuous map $Hx \mapsto K\gamma^{-1}x$. May uses this functor in his construction of covering spaces of a space $B$ corresponding to subgroups of $\pi_1(B, b)$.
Why is this functor defined this way? I'm having trouble understanding why $\alpha$ is taken to $Hx \mapsto K\gamma^{-1}x$.
 A: As you note, every $G$-equivariant map $\alpha\colon G/H\rightarrow G/K$ has the form $gH\mapsto g\gamma K$ (though be cautious that $\gamma$ is only determined modulo $K$ and needs to satisfy $\gamma^{-1}H\gamma\subseteq K$ for this to be a $G$-equivariant map). This means we can consider the $G$-equivariant map $\tilde{\alpha}\colon G\rightarrow G$ given by $g\mapsto g\gamma$ (in fact, every $G$-equivariant map $G\rightarrow G$ has this form for a unique and arbitrary $\gamma$). Thus, we obtain a commutative diagram
$\require{AMScd}$
\begin{CD}
G @>\tilde{\alpha}>> G\\
@Vp_HVV @Vp_KVV\\
G/H @>\alpha>> G/K.
\end{CD}
Assume $F\colon\mathcal{O}(G)\rightarrow\textbf{Top}$ is a functor such that $F(G/H)=X/H$ on objects. This functor then transforms the diagram into a commutative diagram
\begin{CD}
X @>F\tilde{\alpha}>> X\\
@VFp_HVV @VFp_KVV\\
X/H @>F\alpha>> X/K.
\end{CD}
I propose we take $Fp_H\colon X\rightarrow X/H$ to be the natural projection $x\mapsto Hx$. Hopefully, that feels natural. Then, the vertical maps are quotient maps, so $F\alpha$ would already be uniquely determined by $F\tilde{\alpha}$ in case we have functoriality.
Now, $\tilde{\alpha}$ comes from the element $\gamma$ of $G$ acting on $G$ via right translation. We require a homeomorphism $F\tilde{\alpha}\colon X\rightarrow X$, so since we have the element $\gamma$ of $G$ lying around, it's not far-fetched to think we might simply want to let $F\tilde{\alpha}$ to be the map $x\mapsto\gamma.x$. However, that doesn't work. Why? The action of $G$ on itself via right translation is an action from the right, whereas the action of $G$ on $X$ is an action from the left. Even though the $G$-equivariant maps $G\rightarrow G$ are in $1-1$-correspondence with the elements of $G$, the composition of those maps does not correspond to the composition in $G$, but rather composition in the opposite order (the resulting group is sometimes called $G^{op}$). To witness, following the map $g\mapsto g\gamma$ corresponding to $\gamma$ by the map $g\mapsto g\eta$ corresponding to $\eta$ yields $g\mapsto g\gamma\eta$, corresponding to $\gamma\eta$ rather than  $\eta\gamma$. But, there is a simple way of identifying $G$ and $G^{op}$ (i.e. reversing the order of composition), namely by inversion, so if we let $F\tilde{\alpha}$ be $x\mapsto\gamma^{-1}.x$, this recovers functoriality for these types of maps.
Of course, it remains to check that this actually gives a well-defined functor on the entire category, but the point I'm trying to make is that a few hopefully more "natural" choices and considerations actually force us to define the functor the way it is defined. The ultimate justification as to why the functor is defined the way it is will be give once you learn its application, but I understand that tautological answers of the form "it is defined this way, because that's what's needed to make the following theorem work" are not always satisfying as someone is learning something for the first time, and don't necessarily motivate how the definition was come up with in the first place.
