Principal fibration
= Principal fibration
A principal fibration, in the homotopy-theoretic sense, is a homotopy pullback of a <path-space fibration> $PC\to C$ along a map $k:B\to C$. Its fibre is $\Omega C$ and acts on the fibre paths by concatenation, freely and transitively up to the relevant homotopies. Principal bundles for a topological group give this construction through its classifying space. When $C=K(A,n+1)$, the fibre is $K(A,n)$ and the principal fibration is classified by $H^{n+1}(B;A)$, yielding a <principal Eilenberg–MacLane fibration>.