Iterated homotopy pullbacks I would like a reference for the following fact, which I believe to be true.
Consider the simplicial model category of Kan complexes with the Quillen model structure, and suppose given a commutative 3x3 square as below:
$\require{AMScd}$
\begin{CD}
X_1 @>>> X_{12} @<<< X_2\\
@VVV @VVV @VVV\\
Y_1 @>>> Y_{12} @<<< Y_2\\
@AAA @AAA @AAA\\
Z_1 @>>> Z_{12} @<<< Z_2
\end{CD}
Denote by $\operatorname{holim}(X)$, $\operatorname{holim}(Y)$, and $\operatorname{holim}(Z)$ the homotopy limits of the three rows, and by $\operatorname{holim}(C_1)$, $\operatorname{holim}(C_{12})$, and $\operatorname{holim}(C_2)$ the homotopy limits of the three columns. Then the claim is that
$$\operatorname{holim}(\operatorname{holim}(X)\to \operatorname{holim}(Y)\leftarrow \operatorname{holim}(Z))$$
is weakly equivalent to
$$\operatorname{holim}(\operatorname{holim}(C_1)\to \operatorname{holim}(C_{12})\leftarrow \operatorname{holim}(C_2)).$$
In the category of topological spaces this is Theorem 3.3.15 in the book ‘Cubical Homotopy Theory’ by Munson & Volic. It’s a general case of the idea ‘homotopy limits commute with homotopy limits.’ Others refer to it as a ‘Fubini theorem.’ I’ve been able to find surprisingly little documentation of this sort of thing, and I would like to know of a treatment of this kind of thing in any simplicial model category. Thanks.
 A: It seems to me you have found an acceptable concrete argument for yourself, so let me discuss the general principle of "homotopy limits commute with homotopy limits".
Your question can be considered to be a special case of the following question:

Given a diagram $X : \mathcal{I} \times \mathcal{J} \to \mathcal{M}$, what is the relationship between the following (iterated) homotopy limits?
$$\textstyle \mathop{\textrm{ho}{\varprojlim}}_{i : \mathcal{I}} \mathop{\textrm{ho}{\varprojlim}}_{j : \mathcal{J}} X (i, j)$$
$$\textstyle \mathop{\textrm{ho}{\varprojlim}}_{j : \mathcal{J}} \mathop{\textrm{ho}{\varprojlim}}_{i : \mathcal{I}} X (i, j)$$
$$\textstyle \mathop{\textrm{ho}{\varprojlim}}_{(i, j) : \mathcal{I} \times \mathcal{J}} X (i, j)$$

The answer is that there are natural weak equivalences:
$$\textstyle \mathop{\textrm{ho}{\varprojlim}}_{i : \mathcal{I}} \mathop{\textrm{ho}{\varprojlim}}_{j : \mathcal{J}} X (i, j) \longrightarrow \mathop{\textrm{ho}{\varprojlim}}_{(i, j) : \mathcal{I} \times \mathcal{J}} X (i, j)$$
$$\textstyle \mathop{\textrm{ho}{\varprojlim}}_{j : \mathcal{J}} \mathop{\textrm{ho}{\varprojlim}}_{i : \mathcal{I}} X (i, j) \longrightarrow \mathop{\textrm{ho}{\varprojlim}}_{(i, j) : \mathcal{I} \times \mathcal{J}} X (i, j)$$
(The reason why this is sometimes referred to as a "Fubini theorem" is that there is an even more general result concerning homotopy ends, and the corresponding result about ordinary ends is (for better or worse) called a "Fubini theorem" because ends are written with an $\int$ sign.)
In fact, when $\mathcal{M}$ is a simplicial model category and each $X (i, j)$ is a fibrant object in $\mathcal{M}$, there is a very satisfactory theory of homotopy limits in which the comparison morphisms mentioned above are isomorphisms.
Specifically, if $\mathcal{M}$ is the category of simplicial sets with the Kan–Quillen model structure, then the Bousfield–Kan theory of homotopy limits has this property, and it is straightforward to generalise the Bousfield–Kan theory to other simplicial model categories.
Since there is not yet a consensus regarding terminology in this subject, let me make some definitions.
Definition.
Given a category $\mathcal{I}$ and functors $G : \mathcal{I}^\textrm{op} \to \textbf{sSet}$ and $F : \mathcal{I} \to \textbf{sSet}$, the bar construction $\mathrm{B} (G, \mathcal{I}, F)$ is the simplicial set where
$$\mathrm{B} (G, \mathcal{I}, F)_n = \coprod_{(i_0, \ldots, i_n)} G (i_n)_n \times \mathcal{I} (i_{n-1}, i_n) \times \cdots \times \mathcal{I} (i_0, i_1) \times F (i_0)_n$$
with face operators defined by composition in $\mathcal{I}$ and the actions of $G$ and $F$, and degeneracy operators defined by inserting identity morphisms in $\mathcal{I}$.
For brevity, we write $\mathrm{B} (G, \mathcal{I}, \mathcal{I})$ for the functor $\mathcal{I}^\textrm{op} \to \textbf{sSet}$ defined by $i' \mapsto \mathrm{B} (G, \mathcal{I}, \mathcal{I}^{i'})$, where $\mathcal{I}^{i'} = \mathcal{I} (i', -)$.
Definition.
Given a category $\mathcal{I}$, a functor $G : \mathcal{I} \to \textbf{sSet}$, and a functor $F : \mathcal{I} \to \mathcal{M}$, the cobar construction $\mathrm{C} (G, \mathcal{I}, F)$ is an object in $\mathcal{M}$ equipped with isomorphisms
$$\mathcal{M} (T, \mathrm{C} (G, \mathcal{I}, F)) \cong [\mathcal{I}, \textbf{sSet}] (\mathrm{B} (G, \mathcal{I}^\textrm{op}, \mathcal{I}^\textrm{op}), \mathcal{M} (T, F))$$
simplicially natural in $T$, where $[\mathcal{I}, \textbf{sSet}]$ is the simplicially enriched category of functors $\mathcal{I} \to \textbf{sSet}$.
Proposition / Definition.
Let $F : \mathcal{I} \to \mathcal{M}$ be a functor where each $F (i)$ is fibrant and let $G : \mathcal{I} \to \textbf{sSet}$ be any functor.
Then the cobar construction $\mathrm{C} (G, \mathcal{I}, F)$ computes the homotopy limit of $F$ weighted by $G$.
In particular, if $G (i)$ is (weakly) contractible for all $i$, then $\mathrm{C} (G, \mathcal{I}, F)$ computes $\mathop{\textrm{ho}{\varprojlim}}_\mathcal{I} F$.
To be very concrete, let us define $\mathop{\textrm{ho}{\varprojlim}}_\mathcal{I} F$ to mean the cobar construction $\mathrm{C} (G, \mathcal{I}, F)$ where $G (i) = \Delta^0$ for all $i$, bearing in mind that every $F (i)$ must be fibrant for this definition to work well.
Then the claim that "homotopy limits commute with homotopy limits" comes down to the following straightforward calculation:
Lemma.
Let $F : \mathcal{I} \times \mathcal{J} \to \mathcal{M}$, $G : \mathcal{I} \to \textbf{sSet}$, and $H : \mathcal{J} \to \textbf{sSet}$ be functors.
Then we have a natural isomorphism:
$$\mathrm{C} (G, \mathcal{I}, \mathrm{C} (H, \mathcal{J}, F)) \cong \mathrm{C} (G \boxtimes H, \mathcal{I} \times \mathcal{J}, F)$$
Here, $G \boxtimes H : \mathcal{I} \times \mathcal{J} \to \textbf{sSet}$ is defined by $(G \boxtimes H) (i, j) = G (i) \times H (j)$.
Proof.
By definition,
$$\mathcal{M} (T, \mathrm{C} (G, \mathcal{I}, \mathrm{C} (H, \mathcal{J}, F))) \cong [\mathcal{I}, \textbf{sSet}] (\mathrm{B} (G, \mathcal{I}^\textrm{op}, \mathcal{I}^\textrm{op}), [\mathcal{J}, \textbf{sSet}] (\mathrm{B} (H, \mathcal{J}^\textrm{op}, \mathcal{J}^\textrm{op}), \mathcal{M} (T, F)))$$
and it can be shown (using the so-called Fubini theorem, but from ordinary category theory) that
\begin{multline}
[\mathcal{I}, \textbf{sSet}] (\mathrm{B} (G, \mathcal{I}^\textrm{op}, \mathcal{I}^\textrm{op}), [\mathcal{J}, \textbf{sSet}] (\mathrm{B} (H, \mathcal{J}^\textrm{op}, \mathcal{J}^\textrm{op}), \mathcal{M} (T, F))) \\
\cong [\mathcal{I} \times \mathcal{J}, \textbf{sSet}] (\mathrm{B} (G, \mathcal{I}^\textrm{op}, \mathcal{I}^\textrm{op}) \times \mathrm{B} (H, \mathcal{J}^\textrm{op}, \mathcal{J}^\textrm{op}), \mathcal{M} (T, F))
\end{multline}
but it is clear that
$$\mathrm{B} (G, \mathcal{I}^\textrm{op}, \mathcal{I}^\textrm{op}) \times \mathrm{B} (H, \mathcal{J}^\textrm{op}, \mathcal{J}^\textrm{op}) \cong \mathrm{B} (G \boxtimes H, (\mathcal{I} \times \mathcal{J})^\textrm{op}, (\mathcal{I} \times \mathcal{J})^\textrm{op})$$
so we are done.　◼
A: Here is a proof of the claimed statement in simplicial sets with the Joyal model structure. I don’t know why this sort of fact isn’t easier to find and why my question didn’t get any responses: it’s a useful fact with a simple proof and I’m sure it’s well-known. I’m sure the below proof generalizes to other model categories.
I use the fact that any map between fibrant objects (quasi-categories) factors as a weak equivalence (Joyal equivalence) followed by an isofibration (fibration). All objects that appear below are fibrant.
We wish to compute the homotopy limit of the above diagram in two different ways.

*

*First, by factoring each map to $Y_{12}$ as above, we may assume each of the four maps with target $Y_{12}$ are isofibrations.

*Second, factoring $X_1\to Y_1\times X_{12}$ as above, we can assume it is an isofibration. As the projections are isofibrations (all objects are assumed quasi-categories), this implies $X_1\to Y_1$ and $X_1\to X_{12}$ are also isofibrations. We can do the same for the other three corners of the diagram.

Now we are in a situation where the ordinary fiber product of any row or column computes the relevant homotopy pullback, as every arrow in the diagram is an isofibration. Moreover, I claim that the maps $X_1\times_{X_{12}}X_2\to Y_1\times_{Y_{12}}Y_2$ are isofibrations, and similarly for the other row and both maps between pullbacks of the columns. Then our result will follow simply from the fact that ordinary limits commute with limits.
To check the claim, we consider the lifting problem defining an isofibration:
$\require{AMScd}$
\begin{CD}
\{0\} @>>> X_1\times_{X_{12}}X_2\\
@VVV @VVV\\
J @>>> Y_1\times_{Y_{12}}Y_2.
\end{CD}
($J$ is the nerve of the category with two objects and precisely one isomorphism between them.)
We wish to find a map $J\to X_1\times_{X_{12}}X_2$ that makes the diagram commute. We can solve the lifting problem
\begin{CD}
\{0\} @>>> X_1\\
@VVV @VVV\\
J @>>> Y_1,
\end{CD}
so we only need solve the lifting problem
\begin{CD}
\{0\} @>>>X_2\\
@VVV @VVV\\
J @>>> X_{12}\times_{Y_{12}}Y_2,
\end{CD}
which I can solve since $X_2\to X_{12}\times Y_2$ is an isofibration by construction.
