These days, I am making my way towards the classification result about homotopy classes of maps from a CW-complex $Y$ to $BG$ and isomorphism classes of principal $G$-bundles over $Y$, where $G$ is a topological group. It states that taking the pullback $f^*EG$ of a map $f:Y \rightarrow BG$ specifies a bijection between these two sets.
A first step towards this theorem is to be assured that this association is well-defined, i.e that homotopic maps yield isomorphic principal $G$-bundles. To get there, the sources I found combine the following lemmas:
Let $f : P \rightarrow Q$ be a morphism of principal $G$-bundles over the same base space $B$ such that $f$ covers the identity map on $B$. Then, $f$ is an isomorphism.
Let $P \rightarrow B$ be a principal $G$-bundle and $X$ a right $G$-space. Then, the $G$-maps $Hom_G(P, X)$ are in bijection with the sections of the associated bundle $\Gamma(P \times_G X \rightarrow B)$.
The way these results are combined is as follows: to get an isomorphism between $f^*EG$ and $g^*EG$ with an homotopy $H : Y \times I \rightarrow BG$ from $f$ to $g$, one builds the bundle $H^*EG$ over $Y \times I$, and proves that it is isomorphic to $(f^*EG) \times I$. To do so, the first lemma reduces the problem to finding a morphism between $f^*EG\times I$ and $H^*EG$ that covers the identity on $Y \times I$. But now, the sources I find seem to get this desired morphism through the second lemma, by extending a map $s: Y \rightarrow (f^*EG \times I) \times_G H^*EG$ thanks to a Serre fibration. This method produces a section $ \overline{s} : Y \times I \rightarrow (f^*EG \times I) \times_G H^* EG$, which gets turned into a $G$-map between $f^*EG \times I$ and $H^*EG$. But, I do not know how to verify that this map coincides with the identity on the base space $Y \times I$. This prevents me from using the first lemma to conclude. To be more precise, the map $s$ that gets extended is the one associated through the second lemma to the inclusion $f^*EG \times \{0\} = H^*EG|_{Y \times \{0\}} \subset H^*EG$. The lifting can happen in the following diagram (with a Serre fibration on the right):
$\begin{array}{ccc} Y \times \{0\} &\rightarrow &(f^*EG \times I) \times_G H^*EG \\ \downarrow & & \downarrow p \\ Y \times I &\rightarrow & Y \times I, \end{array}$
where $p$ can be chosen to be $p_{f^*EG \times I}$ or $p_{H^*EG}$. In the former case, the second lemma translates the extended $\overline{s}$ into a $G$-map $f^*EG \times I \rightarrow H^*EG$, and in the latter case into a $G$-map $H^*EG \rightarrow f^*EG \times I$. But, as I said, in either case can I manage to show that this $G$-map preserves the projection on $Y \times I$.
I tried to fix this by replacing $p$ in the diagram by both $p_{f^*EG \times I}$ and $p_{H^*EG}$, i.e by the map $(p_{f^*EG \times I}, p_{H^*EG}) : (f^*EG \times I) \times_G H^*EG \rightarrow Y \times I \times Y \times I$. The bottom map becomes the diagonal. A lift in this new diagram would be good, but I am unsure whether it exists: is $(p_{f^*EG \times I}, p_{H^*EG})$ is a Serre fibration? It even looks like a principal $G$-bundle.
Is my fix correct? Am I using the two preliminary results wrong? Any insight is welcome, cheers !