I'm starting reading something about $G$-homology and as one of the first example I encountered the Borel $G$-homology defined as $$ H^G_*(X):= H_*(EG\times_G X)$$ where $H_*$ is any homology theory, (let us stick with singular homology theory for now).
As one of the first properties one want to prove is that if $X$ is a free $G$-space, then $$H_*^G(X)\xrightarrow{\cong} H_*(X/G)$$
Now on these notes just after Def. $2.2$, the author want to prove this, but it seems to me that he is assuming that the $G$-action on $EG$ is globally transitive, (i.e. $BG=\ast$) which it's not true in general.
On this book by Lück and Kreck , in example $20.8$ they suggest (in a slightly more general setting) to apply the induction structure, which in our easy case would be associated to the trivial morphism $\pi\colon G\to \{1\}$ and would become $$\phi\colon EG\times_G X \to E\{1\}\times_{\{1\}}\{1\}\times_{\pi} X$$ $$ (e,x)\mapsto (E\pi(e),1,x)$$ and then using the easy fact that $E\{1\}\simeq \ast$ we would have $$\phi \colon EG\times_G X \to X/G$$
They claim that since $G$ acts freely on $X$, the map induces an isomorphism in homology. Now I'm aware that sometimes this is taken as an axiom for equivariant homology theories, but I need a proof in my easy case.
UPDATE Maybe I found a way to correct the reasoning done in the notes, So it is sufficient to prove that $$\phi\colon EG\times_G X \to X/G$$ is an homotopy equivalence. Let us consider the contraction of $EG$ to a point, which exists by def. of $EG$. So we have an equivalence $EG\times_G X\xrightarrow{\simeq} * \times_G X$ and the latter should be the same as $X/G$. What is unclear to me is where the free action on $X$ comes into play here.
You have to be careful with your argument about extending a homotopy of $EG$ to $X\times_G EG$, why should you be able to do that? In the non-free case stuff can happen... Just to imagine, consider $gx=x$, $ge\neq e$ and the image of a path $e \to ge$ in $EG$.
What you can always do is write down a map $X\times_G EG \to X/G$ by collapsing $EG$ to a point. This is an often use method to compute equivariant homology e.g. by considering spectral sequences. Also you will see that equivariant homology is a lot about analyzing the fix points of the action, something which only exists for non-free actions. However if $X$ is $G$-free, then the fiber computes to $EG$, which gives you a weak equivalence if your $X$ was paracompact to start with.