Principal bundle as homotopy fiber universally self-trivializes In this MO answer, I was told the definition of principal bundle as a homotopy fiber of its classifying map precisely says that it's the universal bundle which trivializes itself.
However, I'm having a hard time actually making this explicit, i.e how exactly to move from "it is the universal map to $B$ such that the composition with $f$ is equipped with a nullhomotopy", to "$E$ is the universal space over $B$ equipped with a trivialization of the pullback of the principal bundle to $E$"?
Where to use homotopy invariance?
 A: You trivialize $E\times_B E\to E$ using exactly the nullhomotopy of $f\circ p:E\to BG$. For this you need to know that principal $G$-bundles over $X$, up to isomorphism, are in bijection with maps $X\to BG$, up to homotopy, and that given $f:X\to BG$ classifying $q:Z\to X$ and a map $g:Y\to X,f\circ g$ classifies $Z\times_X Y\to Y$. The first fact is proven wherever principal $G$-bundles are defined. The second fact follows from the cancellation lemma for pullbacks and the construction of the bundle classified by a map into $BG$ as the pullback with $EG$ over $BG$: in the earlier notation, $q$ is the projection $X\times_{BG} EG\to X$, $f\circ g$ classifies
$Y\times_{BG}EG\to Y$, and by pullback cancellation $Y\times_{BG}EG= Y\times_X X\times_{BG} EG$. Now returning to $E$ and $B$, since the nullhomotopy of $f\circ p$ was universal, so is the trivialization of $E\times_B E\to E$.
A: It might be amusing to see how this works in the context of covering spaces. If $G$ is discrete, a $G$-bundle is specified by a representation $\rho: \pi_1(B) \to G$; this representation is determined by picking a basepoint in the total space $x \in E$, and sending a loop to the unique $g$ such that if you lift the loop to start at $x$, it ends at $gx$. This is called the monodromy of the bundle.
Now pull the bundle back under a map $f: X \to B$. If you pick a basepoint in $f^*E$ so that on total spaces this is a based map, I claim the bundle has mondronomy given by the composition $\pi_1(X) \to \pi_1(B) \to G$. This is straightforward to verify. Then if $X = E$ and $f$ is the covering projection, since we know $\pi_1(E)$ is the kernel of the representation $\rho$, we see that the bundle pulls back to a trivial bundle. 
