Classically, given a compact Lie group $G$, there is a topological space $BG$ which classifies principal $G$-bundles. This means that there is an equality of sets {principal $G$-bundles up to isomorphism} = {maps $X \to BG$ up to homotopy}.


**Question:** is there a "infinity categorical" refinement of this statement? (And if so, what are good references?)


For example, is there a statement along the lines of " every principal $G$-bundle over a space $X$ is "coherently isomorphic" (whatever this means...) to the pullback of the universal bundle over $BG$ under some map $X \to BG$ which is unique "up to coherent homotopy"?



Homotopy coherent generalization of classifying space theory
$\newcommand{\cS}{\mathcal{S}}\newcommand{\Fun}{\mathrm{Fun}}\newcommand{\LMod}{\mathrm{LMod}}\newcommand{\Sp}{\mathrm{Sp}}$Hey Laurent :) Let $X$ be a space (which I'll view as a Kan complex), and let $\cS$ denote the $\infty$-category of spaces. You could think of the homotopy-coherent categorification of "maps $X \to BG$ up to homotopy" as $\cS\_{/BG}$. Then Theorem 2.2.1.2 of Higher Topos Theory (see Section 2.2 of <https://arxiv.org/pdf/1403.4325.pdf> for a bite-sized summary) says that there's an equivalence $\Fun(X, \cS) \simeq \cS\_{/X}$. So, taking $X = BG$ (i.e., the nerve of the one-object topological category whose morphism space is $G$), we see that $\Fun(BG, \cS) \simeq \cS\_{/BG}$. But a functor from $BG \to \cS$ is exactly the data of a homotopy-coherent $G$-action on a space, as desired. (One other useful fact is that if $X$ is assumed to be connected, and $\Sp$ denotes the $\infty$-category of spectra, then there's a Koszul duality equivalence $\Fun(X, \Sp) \simeq \LMod\_{\Sigma^\infty\_+ \Omega X}(\Sp)$, where $\Sigma^\infty\_+ \Omega X$ is viewed as an $\mathbf{E}\_1$-algebra in $\Sp$. Taking $X = BG$, we see that $\Fun(BG, \Sp) \simeq \LMod\_{\Sigma^\infty\_+ G}(\Sp)$; you can interpret this as saying that the $\mathbf{E}\_1$-algebra $\Sigma^\infty\_+ G$ plays the role of a spherical group ring of $G$.)


