Equivalence of Definitions of Principal $G$-bundle I've finally gotten around to learning about principal $G$-bundles.
In the literature, I've encountered (more than) four different definitions.  Since I'm still a beginner, it's unclear to me whether these definitions are equivalent or not.  I would appreciate any clarification.
All maps and group actions are assumed continuous.

Definition 1: A principal $G$-bundle is a fiber bundle $F \to P \xrightarrow{\pi} X$ together with a right action of $G$ on $P$ such that:
(1) $G$ acts freely and transitively on fibers.
(2A) $G$ preserves fibers.



Definition 2: A principal $G$-bundle is a fiber bundle $F \to P \xrightarrow{\pi} X$ together with a left action of $G$ on $F$ (note $F$ here) such that:
(1) $G$ acts freely and transitively on $F$.
(2B) There exists a trivializing cover with $G$-valued transition maps.



Definition 3: A principal $G$-bundle is a fiber bundle $F \to P \xrightarrow{\pi} X$ together with a right action of $G$ on $P$ such that:
(1') $G$ acts freely on $P$ and $X = P/G$ and $\pi\colon P \to X$ is $p \mapsto [p]$.
(2C) There exists a trivializing cover that is $G$-equivariant.



Definition 4: A principal $G$-bundle is a fiber bundle $F \to P \xrightarrow{\pi} X$ together with a right action of $G$ on $P$ such that:
(2A) $G$ preserves fibers.
(2C) There exists a trivializing cover that is $G$-equivariant.


Thoughts: It seems to me that Definition 4 is not equivalent to the other three.  More than anything else, I am unclear as to why the existence of a trivializing cover that is $G$-equivariant is equivalent (is it?) to the existence of one that has $G$-valued transition functions.
I've also seen a fifth definition which assumes only condition (1).
Thanks in advance.
 A: For the equivalence of these definitions, I would look here: Local triviality of principal bundles.
The existence of a $G$-equivariant cover is equivalent to the existence of $G$-valued transition functions:
Suppose $(U_\alpha,\Phi_\alpha)$, $\Phi_\alpha : P\vert_{U_\alpha} \to U_\alpha\times F$, is a trivializing cover.  This defines a collection of maps $\phi_\alpha : P\to F$ by
$$
\Phi_\alpha(p) = (\pi(p), \phi_\alpha(p)).
$$
For a right principal $G$-bundle, this covering is $G$-equivariant if $\phi_\alpha(pg) = \phi_\alpha(p)g$.  Now we have 
$$
\Phi_\alpha \circ \Phi_\beta^{-1} : U_\alpha \cap U_\beta \times F \to U_\alpha \cap U_\beta \times F
$$
is an isomorphism of trivial $G$-bundles and so takes the form
$$
(x, f) \mapsto (x, h_{\alpha\beta}(x,f)).
$$
If the covering is $G$-equivariant then so is this map, which means that $h_{\alpha\beta}(x,fg) = h_{\alpha\beta}(x,f)g$.  Since $G$ is acting freely and transitively, fixing a point of $F$ identities $F$ with $G$ and $h_{\alpha\beta}$ is entirely determined by the function $g_{\alpha\beta}: U_\alpha\cap U_\beta \to G, x \mapsto h_{\alpha\beta}(x,e)$.  Thus the transition functions are given by left-multiplication by $g_{\alpha\beta}$.  This is what is meant by the transition functions being $G$-valued.
Conversely, if the transition functions are $G$-valued then the trivializations will be $G$-equivariant.  This is because
$$
P = \sqcup_\alpha U_\alpha \times F/\sim, ~~ (x, f) \sim (x, g_{\alpha\beta}(x)f) \text{ for } x \in U_\alpha\cap U_\beta.
$$
The equivariance then comes from the fact that the transition functions are operating by left-multiplication, while the $G$-action is right multiplication.
A: In fact, these definitions are not equivalent and are not equivalent to the usual notion of a principal $G$-bundle, see e.g. Kobayashi-Nomizu "Foundations of differential geometry", Vol. I, p. 50: 
First of all, you have to assume, say, properness of the $G$-action and local compactness of $F$ in all the definitions. Otherwise, the following will be a counter-example to all four: Start with your favorite connected Lie group  $G$ of dimension $>0$ (say, $U(1)$) and your favorite topological space $X$ (say, a point). Then $P=G\times X$ is a principal $G$-bundle. Now, consider the same group $G$ but equipped with discrete topology $G^\delta$, but keep the original topology on $P$. Take the obvious action $G^\delta\times P\to P$. This action  satisfies (1)---(4) but does not define a $G^\delta$-principal bundle. 
This can be (partly) remedied by assuming that $G$ is (2nd countable!) Lie group and $F$ is a manifold. Then (2) and (3) become equivalent to the standard definition.  
Here is the situation assuming the extra assumption of properness. 
(1) is not equivalent to (2) even if $G$ is a compact metrizable group, see here. Nevertheless, (1) $\iff$ (2) if (in (1)) $G$ is assumed to be a Lie group ($F$ need not be a manifold; this theorem is due to R.Palais). 
(2) is equivalent to (3). 
(3) is equivalent to (4) provided that in (4) the $G$-action on each fiber is transitive.  
