In a direct proof of the equivalence of categories between the covering maps $p:(\hat X, \hat x) \rightarrow (X,x)$ of a topological space $(X,x)$ for sufficiently beautiful $X$ and the $\pi_1(X,x)$-Sets, I found the following construction I do not understand:
To show the surjectivity of the fibre functor, we need to show that for each $\pi_1(X,x)$-Set $G$ there is a covering space $p:(\hat X, \hat x) \rightarrow (X,x)$ such that $G \cong p^{-1}(x)$. As we, by assumption, have the universal covering $\tilde X$ we construct the desired covering explicitly as
$\tilde X \times_{\pi_1(X,x)} G$,
which is then said to be a covering as it is a fibre bundle with a discrete fibre. However, I haven't found concise information about this construction/notation and Wikipedia's definition of a fibre bundle does not seem to match well. I think we assume $G$ to carry the discrete topology but what does the $\pi_1$ in the index imply?
$\tilde{X}\times_{\pi_1(X)}G$ is an example of the associated bundle construction:
Suppose you have a principle $H$-bundle $E\rightarrow B$ and a left action of $H$ on some other space $F$, then you can form the associated bundle $E\times_H F$ as described in wikipedia in the section "Fiber bundle associated to a principal bundle". This is a fiber bundle with fiber $F$.
To specify the situation to your case: Coverings are exactly fiber bundles with discrete fibers and the universal covering of a space $X$ is a principle $\pi_1(X)$-bundle via the operation by deck transformations. Since $G$ is a $\pi_1(X)$-set it comes with a left action of $\pi_1(X)$ and we can form the associated bundle $\tilde{X}\times_{\pi_1(X)}G$, which is a fiber bundle with fiber $G$ and since $G$ is discrete (By the way, since it will become the fibre of the resulting covering space, which is always discrete by definition.) it is a covering space.