Homotopy coherent generalization of classifying space theory 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"?
 A: I think it is worth expliciting skd's answer.
There is a chain of equivalences $$\mathcal S_{/BG} \simeq Fun(BG, \mathcal S) \simeq Mod_G(\mathcal S)$$ each of which is, at an informal level, easy to define.
The first one takes your space $p: X\to BG$ to the functor $BG\to \mathcal S$ that sends the basepoint $*\to BG$ to the fiber $*\times_{BG} X = p^{-1}(*)$ and the various paths in $BG$ are sent to the equivalences they induce in the fibers, and the higher homotopies are sent to homotopies that witness that these equivalences are all coherent - basically what one would prove at a very truncated level in an AlgTop class about the fibers of a fibration.
The inverse of this functor is also easy to describe, and quite informative : it takes a functor $F : BG\to\mathcal S$, observes that it has a canonical map to the trivial functor $*$ and takes colimits : $colim_{BG} F \to colim_{BG}* \simeq BG$. So the way you can think of $X\to BG$ is as $colim_{BG}Y\to BG$, where $Y$ is the fiber of $X\to BG$ over the point.
The standard picture is : $Y\to Y_{hG}\to BG$. Leaving the world of $\infty$-categories for a second, if you think of $Y$ as a topological space with a strict, free $G$-action (and the usual hypotheses for bundles), then this is exactly the classical picture, because then $Y_{hG}$ is then $Y/G$, and $Y\to Y/G$ becomes $Y/G \times_{BG} EG$ - but $EG$ is just a point ! So back in the homotopy world, this pullback becomes a (homotopy) pullback $Y_{hG}\times_{BG} *$, i.e. exactly the fiber, so we land on our feet.
The second equivalence I wanted to mention because it clarifies that functors $BG\to \mathcal S$ can really be thought of as $G$-bundles, even for non-discrete $G$. If $F$ is a functor $BG\to \mathcal S$, then it induces a map $G\simeq \Omega BG \simeq map_{BG}(*,*) \to map_\mathcal S(F(*), F(*))$, which is a monoid map, and hence corresponds to a $G$-action on $F(*)$. Conversely, this action is all you need to define such a functor.
So all in all, the composite equivalence sends $X\to BG$ to the fiber $Y$ with its $G$-action induced from that, and conversely given a $G$-action on $Y$, you get the homotopy orbits $Y_{hG}$ with their canonical map to $BG$. So somehow the whole thing goes through.
I guess you could ask for what happens if you want to focus on $X$, so view $X$ as fixed. Then, you can view $X$ as a trivial $G$-module, and then by adjunction a map of $G$-modules $Y\to X$ is the same as a map of spaces $Y_{hG}\to X$. The former has a canonical map to $BG$ so if this map is an equivalence, $X$ gets a map to $BG$.
Making that precise (e.g. by using un/straightening, this time over $X$; or comparing the fiber of $\mathcal S_{/BG}\to \mathcal S$ over $X$ to that of $Mod_G(\mathcal S)\to \mathcal S$; or observing some colimit-preservation thing), you obtain an equivalence between "$Bun_G(X)$", by which I mean the full suhspace/sub-$\infty$-groupoid of $(Mod_G(\mathcal S)_{/X})^\simeq$ spanned by those $Y\to X$ that induce an equivalence $Y_{hG}\to X$ and the mapping space $map(X, BG)$.
If you want more detail, I can sketch a proof of that last equivalence !
A: $\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$.)
