Referring to the last part of this answer https://mathoverflow.net/a/225403/170683, I would like to understand how in the case of a Galois cover $f\colon X\to Y=X/G$ with Galois group $G$ (I guess that means $\operatorname{Aut}_Y(X)=G$), we have a canonical equivalence $\operatorname{Sh}(X/G)\simeq \operatorname{Sh}(X)^{hG}$ between the category of sheaves on $X/G$ and the category of homotopy fixed points $\operatorname{Sh}(X)^{hG}$, which for me (and also for the user who gave the answer above) is defined in various equivalent ways, such as the category having objects pairs $(A,\sigma)$ for $A$ in $\operatorname{Sh}(X)$ and $\sigma=\{\sigma_g\colon A\to g^*A\}_{g\in G}$ a family of isomorphism satisfying the cocycle condition $\sigma_{gh}=h^*\sigma_g\sigma_h$, and morphisms the obvious equivariant ones.
Now, the reasoning in the answer seems to be that using the descent for the morphism $f$ we are able to establish an equivalence (via the comonadicity of the adjunction $f^*\dashv f_*$) of the categories $\operatorname{Sh}(X/G)\simeq f^*f_*$-$\operatorname{coalg}_{\operatorname{Sh}(X)}$, and that I know. But now how explicitly we find the homotopy fixed point structure starting from the coalgebra (and viceversa) in order to have $\operatorname{Sh}(X/G)\simeq f^*f_*$-$\operatorname{coalg}_{\operatorname{Sh}(X)}\simeq \operatorname{Sh}(X)^{hG}$?
My attempt is the following. Given a coalgebra $a\colon A\to f^*f_*A$ and $g\in G$, which we said is an isomorphism $g\colon X\to X$ such that $fg=f$, we get a morphism $\sigma_g$ as the composite
$$A \overset{a}{\longrightarrow} f^*f_*A=(fg)^*f_*A=g^*f^*f_*A\overset{g^*\varepsilon_A}{\longrightarrow} g^*A.$$
Unfortunately, I'm not sure this is an isomorphism satisfying the cocycle condition. A reasonable inverse should be $g^*\sigma_{g^{-1}}$.
For sure is needed the coalgebra conditions for $a$ saying that $\varepsilon_A\circ a=\mathrm{id}$ and $f^*f_*a\circ a=(f^*\eta f_*)_A\circ a$. Also, I have no clue for how to define the algebra structure starting from the data of an homotopy fixed point.
Do you think this is true and the approach is correct? Any help is appreciated. Thanks in advance.
