Equivalence Between Category of Covering Spaces and Category of Sets with an Action By The Fundamental Groupoid Let $\Pi_1(X)$ be the fundamental groupoid of a locally path-connected topological space $X$ and define  $\Pi_1(X)-\mathbf{Sets}$ to be the category of sets equipped with an action by the fundamental groupoid. Let furthermore $\mathbf{Cov}(X)$ be the category of covering spaces over $X$. I want to show that we have the following equivalence of categories
$$\mathbf{Cov}(X)\simeq \Pi_1(X)-\mathbf{Sets}.$$
So far, I have constructed two functors
$$\Phi:\mathbf{Cov}(X)\to\Pi_1(X)-\mathbf{Sets}$$
and (I think and hope this is correct)
$$\Psi:\Pi_1(X)-\mathbf{Sets}\to\mathbf{Cov}(X).$$
I now want to show that they give me the equivalence between the categories. However, I find it quite difficult to show that we have natural isomorphisms $\Phi\Psi\Longrightarrow \mathbf{1}_{\Pi_1(X)-\mathbf{Sets}}$ and $\Psi\Phi\Longrightarrow \mathbf{1}_{\mathbf{Cov}_{/X}}$.
In the first section, I will briefly go through the construction of the functors $\Phi$ and $\Psi$. After that, I will explain my concerns about the equivalence.
This post will only concern one of the directions about the equivalence. Just to make the post more concentrated and not "too much". I will (maybe) post another question later, depending on if I don't manage to figure out the other direction by myself.

Construction of Functors
We begin with an explanation of the functor $\Phi$, then with $\Psi$.
The Construction of the Functor $\Phi$
In the category $\Pi_1(X)-\mathbf{Sets}$, an object is a functor $F:\Pi_1(X)\to\mathbf{Sets}$. So, we need to construct such a functor using a covering space.
Objects. Let $p:Y\to X$ be a covering space, we define a functor
$$F:\Pi_1(X)\to\mathbf{Sets}$$
as follows.
Objects of the fundamental groupoid are points of $X$, so we define
$$F(x)=p^{-1}(x),$$
where $x\in X$.
A morphism in $\Pi_1(X)$, between two points $x_0$ and $x_1$, is a path $\alpha:x_0\to x_1$ modulo homotopy equivalence. Given such a path, we construct a set-theoretical map $\alpha_*:p^{-1}(x_0)\to p^{-1}(x_1)$ (from a point $y_0\in p^{-1}(x_0)$ to a point $y_1\in p^{-1}(x_1)$) as follows:
We have a covering space $p:Y\to X$, which makes it possible to apply the path-lifting property. That is, we lift $\alpha:x_0\to x_1$ to a path $\widetilde{\alpha}:y_0\to y_1$, such that $\beta(0)=y_0$ and $p_*\widetilde{\alpha}=\alpha$. Letting $\widetilde{\alpha}(1)=y_1$, one can check that $p_*\widetilde{\alpha}(1)=p(y_1)=\alpha(1)=x_1$, which gives a well-defined map
$$\alpha_*:p^{-1}(x_0)\to p^{-1}(x_1),$$
which is the morphism in $\mathbf{Sets}$. So $F$ is, indeed, a functor.
Morphisms. A morphism in $\Pi_1(X)-\mathbf{Sets}$ between two functors $F,G:\Pi_1(X)\to\mathbf{Sets}$ is a natural transformation $\eta:F\Longrightarrow G$.
One can construct a natural transformation $\eta$ using a covering space homomorphism $\varphi:(Y_0,p_0)\to (Y_1,p_1)$, by letting $\eta_x:F(x)\to G(x)$ be defined by $\eta_{x}(y)=\varphi_{|p_0^{-1}(x)}(y)$. This gives us a commutative diagram
$\require{AMScd}$
\begin{CD}
p_0^{-1}(x_0) @>\eta_{x_0}>> p_1^{-1}(x_0)\\
@VVF(\alpha)V @VVG(\alpha)V\\
p_0^{-1}(x_1) @>\eta_{x_1}>> p_1^{-1}(x_1),
\end{CD}
with $\alpha:x_0\to x_1$ a homotopy path.
Hence, we know where to map objects through the functor $\Phi$.
The Construction of the Functor $\Psi$
Objects. Factor $X$ as follows
$$
X=\bigcup_i V_i,
$$
where $V_i$ has the subspace topology and such that $\Pi_1(V_i)=\pi_1(V_i,x_i)=0$ (with a basepoint $x_i$), which can be done since $X$ is locally path-connected.
An object in $\Pi_1(X)-\mathbf{Sets}$ is a functor $G$, say. The functor $G$ is constant at each $V_i$. That is, for $v_i\in V_i$, we have
$$
G(v_i)=S_i,
$$
where $S_i$ is some set, equipped with the discrete topology.
To build a covering space of $X$, let us define an equivalence relation $\sim_a$ on points in $\bigsqcup_i V_i$, we will do it through the collection of inclusions
$$
h_i:V_i\hookrightarrow X.
$$
We say that two points $x\in V_i$ and $y\in V_j$ are equivalent under $\sim_a$ if and only if
$$
h_i(x)=h_j(y).
$$
We then paste it together and express $X$ as the quotient space
$$
X=\bigsqcup_i V_i / \sim_a
$$
Furthermore, let $V_j\times S_j$ be the topological space, where $V_j$ has the subspace topology, $S_j$ the discrete topology and their product the product topology. We define another equivalence relation $\sim_b$ on the space
$$
\bigsqcup_i \Big [V_i\times S_i \Big ]
$$
as follows
$$
V_i\times S_i\ni(x,s)\sim_b (y,t)\in V_j\times S_j \iff \\
h_i(x)=h_j(y)\\
s\in G(v_i)\cong G(x)=G(y)\cong G(v_j)\ni t
$$
This gives us the space $\widetilde{X}$, which covers $X$
$$
\widetilde{X}=\bigsqcup_i \Big [V_i\times S_i \Big ]\Big /\sim_b.
$$
Morphisms. A morphism in $\Pi_1(X)-\mathbf{Sets}$, is a natural transformations $\mu:G_1\Longrightarrow G_2$ between $G_1,G_2:\Pi_1(X)-\mathbf{Sets}$. That is, given a point $x\in\Pi_1(X)$, we assign a morphism $\mu_x:G_1(x)\to G_2(x)$. And given a path $\gamma:x\to y$ in $X$, such that we have the following commutativity $\mu_y\circ G_1(\gamma)=G_2(\gamma)\circ\mu_x$.
We use that natural transformation to construct a covering space homomorphism.
Let $f: \bigsqcup_i\Big [ V_i\times G_1(V_i)\Big ] \to  \bigsqcup_i\Big [ V_i\times G_2(V_i)\Big ]$ be defined by $f(v,s)=(v,\mu_{x}(s))$, where $x\in V_j$ for some $j$. This gives us the commutativity of the diagram follows, and hence, we have a covering homomorphism
$$\require{AMScd}
\require{cancel}
\def\diaguparrow#1{\smash{\raise.6em\rlap{\ \ \scriptstyle #1}
   \lower.6em{\cancelto{}{\Space{2em}{1.7em}{0px}}}}}
\begin{CD}
&& \bigsqcup_i\Big [ V_i\times G_2(V_i)\Big ]\\
& \diaguparrow{f} @VVp_2V \\
\bigsqcup_i\Big [ V_i\times G_1(V_i)\Big ] @>>p_1> \bigsqcup_i\Big [ V_i\Big ]
\end{CD}$$
which induces a covering space homomorphism from $\widetilde{X}$ onto $X$.

Equivalence of Categories
I now want to show that the categories are equivalent
$$\mathbf{Cov}(X)\simeq \Pi_1(X)-\mathbf{Sets}.$$
This means that we have to construct natural isomorphisms of functors
$$
\Psi\circ \Phi\cong \operatorname{Id}_{\mathbf{Cov}(X)}\qquad \text{and}\qquad \Phi\circ\Psi\cong \operatorname{Id}_{\Pi_1(X)-\mathbf{Sets}}
$$
Constructing a Natural Isomorphism $\eta:\Psi\circ\Phi\Longrightarrow \operatorname{Id}_{\mathbf{Cov}(X)}$
What we need is to construct an isomorphism $\eta_{(Y,p)}:\Psi\circ\Phi(Y,p)\to \mathbf{1}_{\mathbf{Cov}(X)}(Y,p)$, for every covering space $(Y,p)$ of $X$, such that the following diagram commutes
$\require{AMScd}$
\begin{CD}
\Psi\circ\Phi(Y_0,p_0) @>\eta_{(Y_0,p_0)}>> \operatorname{Id}_{\mathbf{Cov}(X)}(Y_0,p_0)\\
@VV\Psi\circ\Phi(\varphi)V @VV\operatorname{Id}_{\mathbf{Cov}(X)}(\varphi)V\\
\Psi\circ\Phi(Y_1,p_1) @>\eta_{(Y_1,p_1)}>> \operatorname{Id}_{\mathbf{Cov}(X)}(Y_1,p_1)
\end{CD}
The above diagram reduces to
$\require{AMScd}$
\begin{CD}
\Psi\circ\Phi(Y_0,p_0) @>\eta_{(Y_0,p_0)}>> (Y_0,p_0)\\
@VV\Psi\circ\Phi(\varphi)V @VV\varphi V\\
\Psi\circ\Phi(Y_1,p_1) @>\eta_{(Y_1,p_1)}>> (Y_1,p_1)
\end{CD}
Question 1. Maybe this is obvious, but how should I define $\eta_{(Y,p)}$ to make it both an isomorphism and such that the diagram commutes?
Question 2. It is difficult for me to understand what $\Psi\circ\Phi(Y,p)$ and $\Psi\circ\Phi(\varphi)$ looks like. Applying $\Phi$ to $(Y,p)$ gives a functor $F:\Pi_1(X)-\mathbf{Sets}$, such that $F(x)=p^{-1}(x)$ and which maps paths according to rule we gave earlier.
Given the functor $F$, what does $\Psi(F)$ look like? Do I need to understand it in order to prove the commutativity of the diagram and/or construct $\eta_{(Y_0,p_0)}$?
Likewise, given a covering space homomorphism $\varphi:(Y_0,p_0)\to (Y_1,p_1)$, what does $\Psi\circ\Phi(\varphi)$ give me? First, I map $\varphi$ to a natural equivalence $\mu:F_0\Longrightarrow F_1$ such that we have morphisms $\mu_x:F_0(x)\to F_1(x)$ and a diagram which commutes
$\require{AMScd}$
\begin{CD}
p_0^{-1}(x_0) @>\mu_{x_0}>> p_1^{-1}(x_0)\\
@VVF_0(\alpha)V @VVF_1(\alpha)V\\
p_0^{-1}(x_1) @>\mu_{x_1}>> p_1^{-1}(x_1),
\end{CD}
where does $\Psi$ map this natural transformation?
This is probably easy. But there are a lot of abstract things going on at the same time, which makes me lose myself.
Best wishes,
Joel
 A: In simple terms, both a covering map $p$ (by looking at preimages) and a $\Pi_1(X)$-set are assigning discrete sets to the points of $X$, in a path compatible way.
For a given cover $(Y,p)$, we first construct the functor that assigns each point of $x\in X$ the fibre of $Y$ above it $\Phi(Y,p)$, then we construct a covering $(Z,q):=\Psi\circ\Phi\,(Y,p)$ such that its fibres are $q^{-1}(x)\cong\Phi(Y,p)\,(x)=p^{-1}(x)$.
Note that, by construction of $\Psi$, for every $x$ an index $i$ can be chosen such that $x\in V_i$ and we should also fix a path $w_x^i:v_i\leadsto x$ in $V_i$, so that
$$s\in G(v_i)\cong G(x)=G(y)\cong G(v_j)\ni t$$
should really mean $x=y$ and $G(w_x^i)\,(s)=G(w_x^j)\,(t)$, so that when we will lift the path $w_x^i$, point $s$ over $v_i$ goes to the same place where point $t$ over $v_j$.
(Since $V_i$ was chosen to be simply connected, this construction is independent of the actual choices $w_x^i$.)
Now, let $(x,s)\in Z$ be a point, then $s$ actually implicitly refers to an index $i$ such that $x\in V_i$ and $s\in \Phi(Y,p)\,(v_i)$, but $\Phi(Y,p)\,(v_i)=p^{-1}(v_i)$, so you receive the correspondent of $(x,s)$ by travelling $s\in p^{-1}(v_i)$ along $w_x^i$.
This correspondence is indeed bijective, for its inverse, travel a point $y\in p^{-1}(x)$ along $(w_x^i)^{-1}$ for some $i$ to obtain an element of $p^{-1}(v_i)$.
There are still lot of details to check, e.g. that these maps are well defined, continuous and natural.
I hope it helps. Good luck!
A: To prove the equivalence of the categories, it suffices to take one of the above functors (e.g. $\Phi:\text{Cov}(X)→\Pi1(X)−Sets$) and show that it is:

*

*Full

*Faithful

*Essentially Surjective
In other words, you don't need to explicitly construct the inverse functor and the natural isomorphisms. Hope this helps shorten the proof.
