2 added 453 characters in body

To answer your first set of questions in order (I'm going to use the word "space" for "$\infty$-groupoid"):

Yes, this is all correct.

You seem to be familiar with how to construct $BG$ as a simplicial space via a bar construction. To turn this into an actual space, you just have to form the geometric realization of this simplicial space. This is just like the geometric realization of a simplicial set: if $X_*$ is a simplicial space, its realization is the quotient of $\bigsqcup X_n \times \Delta^n$ given by gluing together simplices according to the face (and degeneracy) maps. More succinctly, it is the coend of the functor $X:\Delta^{op}\to Spaces$ along the functor $\Delta \to Spaces$ sending $[n]$ to the standard $n$-simplex. More abstractly, it is the (homotopy) colimit of the diagram $X:\Delta^{op}\to Spaces$ in the $(\infty,1)$-category of spaces. If you model spaces as simplicial sets, it can also be described as the pullback of your bisimplicial set along the diagonal functor $\Delta\to\Delta^2$ (to show this, you need to only verify it for single "bisimplices" (ie, representable functors on $\Delta^2$), which amounts to the fact that the product of two representable functors on a category $C$ is the pullback of the associated representable functor on $C^2$ along the diagonal $C\to C^2$).

I don't know the best way of precisely formulating and proving this, but one way is to construct an explicit Quillen equivalence between the categories of simplicial groups and the category of reduced simplicial sets (simplicial groups can be used instead of $A_\infty$-groups because $A_\infty$-spaces can be rigidified). For this, the delooping functor is exactly just taking the geometric realization of the bar construction. The looping functor is subtler--one has to be careful to get a functor which actually lands in simplicial groups. Even if you were happy to land in $A_\infty$-groups, just taking the simplicial mapping space $Maps(S^1,X)$ would not work because for non-fibrant objects $X$ this does not have a multiplication. The classical solution to this is called the "Kan loop group", the exact details of which I don't remember but are described on nlab in the generalized setting of a not-necessarily-reduced simplicial set (in which case you get a simplicial groupoid, rather than a simplicial group). In any case, this is just a specific simplicial model for the loopspace of a reduced simplicial set which happens to actually be a group.

As for a reference, I learned the Kan loop group and the Quillen equivalence it gives from Goerss-Jardine's book Simplicial Homotopy Theory, but they say essentially nothing about thinking about this from an $\infty$-categorical perspective.

1

To answer your first set of questions in order (I'm going to use the word "space" for "$\infty$-groupoid"):

Yes, this is all correct.

You seem to be familiar with how to construct $BG$ as a simplicial space via a bar construction. To turn this into an actual space, you just have to form the geometric realization of this simplicial space. This is just like the geometric realization of a simplicial set: if $X_*$ is a simplicial space, its realization is the quotient of $\bigsqcup X_n \times \Delta^n$ given by gluing together simplices according to the face (and degeneracy) maps. More succinctly, it is the coend of the functor $X:\Delta^{op}\to Spaces$ along the functor $\Delta \to Spaces$ sending $[n]$ to the standard $n$-simplex. More abstractly, it is the (homotopy) colimit of the diagram $X:\Delta^{op}\to Spaces$ in the $(\infty,1)$-category of spaces.

I don't know the best way of precisely formulating and proving this, but one way is to construct an explicit Quillen equivalence between the categories of simplicial groups and the category of reduced simplicial sets (simplicial groups can be used instead of $A_\infty$-groups because $A_\infty$-spaces can be rigidified). For this, the delooping functor is exactly just taking the geometric realization of the bar construction. The looping functor is subtler--one has to be careful to get a functor which actually lands in simplicial groups. Even if you were happy to land in $A_\infty$-groups, just taking the simplicial mapping space $Maps(S^1,X)$ would not work because for non-fibrant objects $X$ this does not have a multiplication. The classical solution to this is called the "Kan loop group", the exact details of which I don't remember but are described on nlab in the generalized setting of a not-necessarily-reduced simplicial set (in which case you get a simplicial groupoid, rather than a simplicial group). In any case, this is just a specific simplicial model for the loopspace of a reduced simplicial set which happens to actually be a group.

As for a reference, I learned the Kan loop group and the Quillen equivalence it gives from Goerss-Jardine's book Simplicial Homotopy Theory, but they say essentially nothing about thinking about this from an $\infty$-categorical perspective.