Primero vamos a demostrar que si $ W \simeq BG$ a través de $\phi$ la función $[X,W] \rightarrow P$ dado por $[f] \rightarrow f^*(\phi^*(EG))$ es biyectiva y natural, donde $P$ es el conjunto de todos los paquetes G principales.
Esto debería ser un hecho categórico general:
Imaginemos que tenemos una categoría $C$ y encima de cada objeto $c \in C$ hay un conjunto $P_C$ (piénsese en las clases de isomorfismo de los haces principales sobre un espacio). Además, un mapa $c \rightarrow c'$ induce un mapa $P_{c'} \rightarrow P_c$ . Hay un functor obvio $F$ tomando $c \rightarrow P(c)$ . Por último, tenemos que un objeto $s$ representa $F$ mediante la retirada de un elemento distinguido $\gamma$ de $P(s)$ .
Queremos decir que dado un isomorfismo $\Phi:s' \rightarrow s$ , $\Phi^*(\gamma)$ es un elemento distinguido de $P(s')$ que retrocediendo por da lugar a un functor naturalmente isomorfo a $F$ .
La subjetividad es fácil: supongamos que $x \in P(c)$ . Sea $f: c \rightarrow s$ sea el mapa que da lugar a $x$ . La composición $\Phi^{-1} f$ es el mapa que buscamos.
La inyectividad también es fácil: supongamos $g^*(s')=h^*(s')$ luego escribiendo lo que esto significa vemos $g^*(\Phi^*(s))=h^*(\Phi^*(s))$ lo que implica $\Phi g = \Phi h$ lo que implica la $g=h$ .
La naturalidad también sale con facilidad. Obsérvese que esto no es más que el lema de Yoneda cuando se reconoce que el haz universal es el pullback de la identidad en $BG$ .
Ahora note que el tipo de isomorfismo del haz principal depende sólo del tipo de homotopía del mapa por el que se retrocede. Esto significa que podemos utilizar el hecho anterior para mostrar que cualquier espacio homotópico equivalente a un espacio clasificador es otro espacio clasificador con haz clasificador el pull back.
Lo único que queda por comprobar es que, dado un cuadrado conmutativo de haces principales en el que los mapas superiores son equivariantes, el pullback del mapa entre espacios orbitales es isomorfo al haz con el que se empezó. Si el mapa entre haces principales es $L$ un isomorfismo viene dado por $x \rightarrow ([x],L(x))$ Esto no depende de que el mapa sea una equivalencia homotópica.
