Proof.
Using Proposition 3.1.7.1, we can choose a functor $\overline{ \mathscr {G} }: \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{Kan}$ and a natural transformation $\beta : \overline{ \mathscr {F}} \rightarrow \overline{\mathscr {G} }$ which carries each object $C \in \operatorname{\mathcal{C}}^{\triangleleft }$ to an anodyne morphism of simplicial sets $\beta _{C}: \overline{ \mathscr {F} }(C) \rightarrow \overline{ \mathscr {G} }(C)$. We will show that $(1)$ and $(2)$ are equivalent to the following:
- $(3)$
The functor $\overline{ \mathscr {G} }$ is a homotopy limit diagram.
The implications $(2) \Rightarrow (3) \Rightarrow (1)$ are immediate. To prove the reverse implications, suppose we are given another functor $\overline{\mathscr {F} }': \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{Kan}$ and a levelwise weak homotopy equivalence $\alpha : \overline{ \mathscr {F} } \rightarrow \overline{ \mathscr {F} }'$. We will show that $\overline{ \mathscr {F} }'$ is a homotopy limit diagram if and only if $\overline{ \mathscr {G} }$ is a homotopy limit diagram.
Applying Proposition 3.1.7.1 again, we can choose a functor $\overline{ \mathscr {G} }': \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{Kan}$ and a commutative diagram
\[ \xymatrix@R =50pt@C=50pt{ \overline{ \mathscr {F} } \ar [r]^-{\alpha } \ar [d]^{\beta } & \overline{ \mathscr {F} }' \ar [d]^{\beta '} \\ \overline{ \mathscr {G} } \ar [r]^-{\alpha '} & \overline{ \mathscr {G} }' } \]
with the property that, for every object $C \in \operatorname{\mathcal{C}}^{\triangleleft }$, the induced map
\[ \overline{\mathscr {F} }'(C) {\coprod }_{ \overline{\mathscr {F} }(C)} \overline{ \mathscr {G} }(C) \rightarrow \overline{ \mathscr {G} }'(C) \]
is anodyne (and, in particular, a weak homotopy equivalence). Applying Proposition 3.4.2.11, we see that the diagram of simplicial sets
\[ \xymatrix@R =50pt@C=50pt{ \overline{ \mathscr {F} }(C) \ar [r]^-{ \alpha _ C } \ar [d]^{ \beta _{C} } & \overline{ \mathscr {F} }'(C) \ar [d]^{ \beta '_{C} } \\ \overline{ \mathscr {G} }(C) \ar [r]^-{ \alpha '_{C} } & \overline{ \mathscr {G} }'(C) } \]
is a homotopy pushout square. Since $\alpha _ C$ and $\beta _ C$ are weak homotopy equivalences, it follows that $\alpha '_ C$ and $\beta '_{C}$ are also weak homotopy equivalences (Proposition 3.4.2.10). Applying Proposition 7.5.4.4, we see that $\overline{ \mathscr {F} }'$ and $\overline{ \mathscr {G} }$ are homotopy limit diagrams if and only if $\overline{ \mathscr {G} }'$ is a homotopy limit diagram.
$\square$