Origin of double cosets and Mackey formula as Beck-Chevalley condition I recently met the Mackey double coset formula for the first time. After asking around I was told that the origin of double cosets is the following fact.
Fact. Let $G_1,G_2\leq G$ be subgroups. Consider the 2-pullback of the diagram $\mathbf BG_1 \rightarrow \mathbf BG\leftarrow \mathbf BG_2$.


*

*The 2-pullback is a groupoid;

*Its connected components are in natural bijection with the double cosets $G_1\!\!\setminus \!G /G_2 $.


Question 1. Where can I find a reference for this? (Also, is the 2-pullback meant to be strict? Perhaps it does not matter...)
Snooping around the nlab page on double cosets I read that the Mackey double coset "amounts to the Beck-Chevalley condition for the homotopy pullback square."
Question 2. What is a maximally readable reference for this viewpoint? I have only seen the Beck-Chevalley condition in the context of 1-categorical (bi)fibrations, and only for the purpose of monadic descent. I don't know any $\infty$-category theory.
 A: 1. You need, equivalently, the pseudo-pullback, iso-comma, or homotopy pullback, which in the language of the nLab and of $\infty$-categorists more inspired by homotopy theory than category theory is often called a 2-pullback, though older-fashioned 2-category theorists use this terminology for the strict limit. Indeed, the strict pullback of your diagram is simply $\mathbf{B}(G_1\cap G_2)$, and strict pullbacks of categories are also 2-pullbacks.
Regarding the pseudo-pullback, this is a straightforward exercise to check directly. By definition an object of the pseudopullback $P$ is given by an element of $G$: that is, more pedantically, an object of $\mathbf{B}G_1$, an object of $\mathbf{B} G_2$, and an isomorphism between their images in $\mathbf{B} G$. A morphism between $g$ and $g'$ in $P$ is given by a morphism $g_1\in G_1$ and another morphism $g_2\in G_2$ such that $g_2g=g'g_1$, or in other words $g_2gg_1^{-1}=g'$. Any such morphism admits $(g_1^{-1},g_2^{-1})$ as an inverse, and so $P$ is a groupoid. And in any groupoid, two objects are in the same connected component if and only if they're directly connected by a morphism. So $g$ and $g'$ are identified in $\pi_0 P$ if and only if there exist $g_2$ and $g_1$ such that $g_2 gg_1^{-1}=g'$. But this is exactly the condition that $g,g'$ lie in the same $(G_2,G_1)$-double coset. 
2. The term "Beck-Chevalley" can certainly arise in a mysteriously wide range of situations. This is actually a more fundamental use than the one you mentioned, I think, and certainly doesn't require any $\infty$-category theory. In particular, we will do better here to view $P$ as living with $\mathbf{B}G,\mathbf{B}G_1,$ and $\mathbf{B}G_2$ in a comma square (which is equivalent to an iso-comma square, since $\mathbf{B}G$ is a groupoid) than in a homotopy pullback square. What's being used here is the very classical base change formula for pointwise Kan extensions. 
Given any cospan $u:B\to A\leftarrow C:v$ of categories, we have the comma category $v/u$ with its projections $p:v/u\to C$ and $q:v/u\to B$, as well as the canonical natural transformation $\alpha:vp\to uq$. Given any cocomplete category $E$, this induces a natural comparison map $q_!p^*\to u^*v_!$, where $u^*:E^A\to E^B$ and $p^*:E^C\to E^{v/u}$ are precomposition functors while $q_!: E^{v/u}\to E^B$ and $v_!:E^C\to E^A$ are left Kan extensions. (The comparison is given, concretely, by $q_!p^*F\to q_!p^*v^*v_!\to q_!q^*u^*v_!\to u^*v_!$, where the three maps are a unit, induced by $\alpha$, and a counit, respectively.) 
Kan's formula for a pointwise Kan extension, slightly generalized, says that this comparison is always an isomorphism. You can see the case when $B$ is a point discussed on the nLab page for Kan extensions. For a general study, the best references I know are actually set in the more general context of derivators. You might start with Moritz Groth's expository paper "Derivators, pointed derivators, and stable derivators." In the context of that subject, the isomorphism I just claimed encodes the fact that every comma square is "exact." But you should also be able to prove my particular claim from the pointwise Kan extension formula.
The relevance of all this for your question appears when we set $E$ to be some category in which we're doing representation theory, such as complex vector spaces, while $u:B\to A\leftarrow C:v$ is instantiated to your cospan $\mathbf{B}G_1\to \mathbf{B}G\leftarrow \mathbf{B}G_2$. Then my $P$ from earlier is identified with $v/u$. When we exponentiate the resulting square over $E$, yielding the categories of $G,G_1,$ and $G_2$-representations in $E$, I claim that a closer examination of $E^P$ will identify Mackey's formula with Kan's. 
What remains is to observe that induction of a representation is left Kan extension, while restriction is simply precomposition. Then Kan's formula tells us how to induce a representation from $G_2$ to $G$ and then restrict to $G_1$ by first restricting to $P$, then inducing to $G_1$. Finally, we recover Mackey's formula upon identifying $P$ (up to equivalence) with $$\bigsqcup_{[g]\in G_1\backslash G/G_2}\mathbf{B}\left(G_2\cap gG_1g^{-1}\right)$$
This identification amounts to calculating the automorphism group of $g\in P$: it's $\{(g_1,g_2):g_2=gg_1g^{-1}\}\cong G_2\cap gG_1g^{-1}$, as desired. Then the left Kan extension of a representation from $P$ to $\mathbf{B}G_1$ is simplify the coproduct of the left Kan extensions of its restrictions to the connected components $\mathbf{B}\left(G_2\cap gG_1g^{-1}\right)$, and this gives the other side of Mackey's formula.
