Proposition 7.6.3.8. Suppose we are given a commutative diagram
7.66
\begin{equation} \begin{gathered}\label{equation:all-squares-in-QCat} \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{C}}_{01} \ar [r] \ar [d] & \operatorname{\mathcal{C}}_{0} \ar [d]^-{ F_0 } \\ \operatorname{\mathcal{C}}_1 \ar [r]^-{ F_1 } & \operatorname{\mathcal{C}}} \end{gathered} \end{equation}
in the $\infty $-category $\operatorname{\mathcal{QC}}$, corresponding to a functor
\[ G: \operatorname{\mathcal{C}}_{01} \rightarrow \operatorname{\mathcal{C}}_{0} \times ^{\mathrm{h}}_{ \operatorname{\mathcal{C}}} ( \operatorname{\mathcal{C}}_1 \times ^{\mathrm{h}}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}). \]
Then (7.66) is a pullback square in $\operatorname{\mathcal{QC}}$ if and only if the functor $G$ is an equivalence of $\infty $-categories.
Proof.
Let us identify the diagram (7.66) with a functor of simplicial categories $\mathscr {F}: \operatorname{Path}[ [1] \times [1] ]_{\bullet } \rightarrow \operatorname{QCat}$. Using Corollary 4.5.2.23, we can factor the functor $F_0$ as a composition $\operatorname{\mathcal{C}}_0 \xrightarrow { T } \operatorname{\mathcal{C}}'_{0} \xrightarrow { F'_{0} } \operatorname{\mathcal{C}}$, where $T$ is an equivalence of $\infty $-categories and $F'_{0}$ is an isofibration. Let $\operatorname{\mathcal{C}}'_{01}$ denote the iterated homotopy fiber product $\operatorname{\mathcal{C}}'_{0} \times ^{\mathrm{h}}_{ \operatorname{\mathcal{C}}} ( \operatorname{\mathcal{C}}_1 \times ^{\mathrm{h}}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}})$. Then Example 7.6.3.7 supplies a commutative diagram
7.67
\begin{equation} \begin{gathered}\label{equation:all-squares-in-QCat2} \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{C}}'_{01} \ar [r] \ar [d] & \operatorname{\mathcal{C}}'_{0} \ar [d]^-{F'_{0}} \\ \operatorname{\mathcal{C}}_{1} \ar [r]^-{F_1} & \operatorname{\mathcal{C}}} \end{gathered} \end{equation}
in the $\infty $-category $\operatorname{\mathcal{QC}}$, which we view as a functor of simplicial categories $\mathscr {F}': \operatorname{Path}[ [1] \times [1] ]_{\bullet } \rightarrow \operatorname{QCat}$. The morphisms $G$ and $T$ determine a natural transformation of simplicial functors $\mathscr {F} \rightarrow \mathscr {F}'$, which induces a natural transformation from the diagram (7.66) to the diagram (7.67) in the $\infty $-category $\operatorname{Fun}( \Delta ^1 \times \Delta ^1, \operatorname{\mathcal{QC}})$. By virtue of Corollary 4.5.2.20, this natural transformation is an isomorphism of diagrams if and only if the functor $G$ is an equivalence of $\infty $-categories. Consequently, Proposition 7.6.3.8 is equivalent to the assertion that (7.67) is a pullback square in the $\infty $-category $\operatorname{\mathcal{QC}}$ (see Proposition 7.1.3.13).
Note that we have a (strictly) commutative diagram of simplicial sets
7.68
\begin{equation} \begin{gathered}\label{equation:all-squares-in-QCat3} \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{C}}'_{0} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{1} \ar [r] \ar [d] & \operatorname{\mathcal{C}}'_{0} \ar [d]^-{F'_{0}} \\ \operatorname{\mathcal{C}}_{1} \ar [r]^-{F'_1} & \operatorname{\mathcal{C}}, } \end{gathered} \end{equation}
which determines a subfunctor $\mathscr {F}'' \subseteq \mathscr {F}'$. Since $F'_0$ is an isofibration, it follows from Corollaries 4.5.2.28, 4.5.2.22, and 4.5.2.29 that the inclusion maps
\begin{eqnarray*} \operatorname{\mathcal{C}}'_0 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_1 & \hookrightarrow & \operatorname{\mathcal{C}}'_{0} \times _{\operatorname{\mathcal{C}}}^{\mathrm{h}} \operatorname{\mathcal{C}}_1 \\ & \hookrightarrow & \operatorname{\mathcal{C}}'_0 \times _{\operatorname{\mathcal{C}}}^{\mathrm{h}} ( \operatorname{\mathcal{C}}_1 \times ^{\mathrm{h}}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}) \end{eqnarray*}
are equivalences of $\infty $-categories. Consequently, the inclusion $\mathscr {F}'' \hookrightarrow \mathscr {F}'$ is a levelwise categorical equivalence of simplicial functors and therefore induces an isomorphism from the diagram ( 7.68 ) to the diagram ( 7.67 ) in the $\infty $-category $\operatorname{Fun}( \Delta ^1 \times \Delta ^1, \operatorname{\mathcal{C}})$. By virtue of Proposition 7.1.3.13, it will suffice to show that the diagram (7.68) is a pullback square in the $\infty $-category $\operatorname{\mathcal{QC}}$. This is a special case of Example 7.6.3.4, since (7.68) is a categorical pullback square (see Corollary 4.5.2.27).
$\square$