If one has a normal Lie group inclusion $H\to G$, with quotient $G/H$, and a $G$-manifold $X$, one can take the quotient $X/H$. Then the $G$-action on $X/H$ factors thru a $G/H$-action, so one can take the quotient again to obtain $(X/H)/(G/H)$. It is known classically that $(X/H)/(G/H)\cong X/G$ (see, e.g. Bourbaki's book on Lie Groups and Lie Algebras, Section 1.6 of Chapter III).

In a less structured setting, say, May's "Classifying Spaces and Fibrations" where the $H$ and $G$ are not Lie groups, but only topological monoids, and $X$ is just an object of the category of compactly generated Hausdorff spaces, we can still produce the quotient group $G/H$ and quotient space $X/H$ by a bar construction.

One could take this one step further and work just with a spectrum $X$ with an action of a topological monoid $G$. One can still take the quotient by $H$, and can still try to then take the quotient again by $G/H$. This all seems like it should be some purely formal bar construction thing.

My question is: where (if anywhere) can I find a proof that for a general model or quasi- category $C$, and a $G$-action on an object $X\in C$, the iterated quotient $(X/H)/(G/H)$ is equivalent to $X/G$?

It'd also be nice to see a general proof for spaces or spectra.

If one has a normal Lie group inclusion $H\to G$, with quotient $G/H$, and a $G$-manifold $X$, one can take the quotient $X/H$. Then the $G$-action on $X/H$ factors thru a $G/H$-action, so one can take the quotient again to obtain $(X/H)/(G/H)$. It is known classically that $(X/H)/(G/H)\cong X/G$ (see, e.g. Bourbaki's book on Lie Groups and Lie Algebras, Section 1.6 of Chapter III).

In a less structured setting, say, May's "Classifying Spaces and Fibrations" where the $H$ and $G$ are not Lie groups, but only topological monoids, and $X$ is just an object of the category of compactly generated Hausdorff spaces, we can still produce the quotient monoid $G/H$ and quotient space $X/H$ by a bar construction.

One could take this one step further and work just with a spectrum $X$ with an action of a topological monoid $G$. One can still take the quotient by $H$, and can still try to then take the quotient again by $G/H$. This all seems like it should be some purely formal bar construction thing.

My question is: where (if anywhere) can I find a proof that for a general model or quasi- category $C$, and a $G$-action on an object $X\in C$, the iterated quotient $(X/H)/(G/H)$ is equivalent to $X/G$?

It'd also be nice to see a general proof for spaces or spectra.

If one has a normal Lie group inclusion $H\to G$, with quotient $G/H$, and a $G$-manifold $X$, one can take the quotient $X/H$. Then the $G$-action on $X/H$ factors thru a $G/H$-action, so one can take the quotient again to obtain $(X/H)/(G/H)$. It is known classically that $(X/H)/(G/H)\cong X/G$ (see, e.g. Bourbaki's book on Lie Groups and Lie Algebras, Section 1.6 of Chapter III).

In a less structured setting, say, May's "Classifying Spaces and Fibrations" where the $H$ and $G$ are not Lie groups, but only topological monoids, and $X$ is just an object of the category of compactly generated Hausdorff spaces, we can still produce the quotient group $G/H$ and quotient space $X/H$ by a bar construction.

One could take this one step further and work just with a spectrum $X$ with an action of a topological monoid $G$. One can still take the quotient by $H$, and can still try to then take the quotient again by $G/H$. This all seems like it should some purely formal bar construction thing.

My question is: where (if anywhere) can I find a proof that for a general model or quasi- category $C$, and a $G$-action on an object $X\in C$, the iterated quotient $(X/H)/(G/H)$ is equivalent to $X/G$?

It'd also be nice to see a general proof for spaces or spectra.

If one has a normal Lie group inclusion $H\to G$, with quotient $G/H$, and a $G$-manifold $X$, one can take the quotient $X/H$. Then the $G$-action on $X/H$ factors thru a $G/H$-action, so one can take the quotient again to obtain $(X/H)/(G/H)$. It is known classically that $(X/H)/(G/H)\cong X/G$ (see, e.g. Bourbaki's book on Lie Groups and Lie Algebras, Section 1.6 of Chapter III).

In a less structured setting, say, May's "Classifying Spaces and Fibrations" where the $H$ and $G$ are not Lie groups, but only topological monoids, and $X$ is just an object of the category of compactly generated Hausdorff spaces, we can still produce the quotient group $G/H$ and quotient space $X/H$ by a bar construction.

One could take this one step further and work just with a spectrum $X$ with an action of a topological monoid $G$. One can still take the quotient by $H$, and can still try to then take the quotient again by $G/H$. This all seems like it should be some purely formal bar construction thing.

My question is: where (if anywhere) can I find a proof that for a general model or quasi- category $C$, and a $G$-action on an object $X\in C$, the iterated quotient $(X/H)/(G/H)$ is equivalent to $X/G$?

It'd also be nice to see a general proof for spaces or spectra.