Corollary 7.6.4.20. Let $F_0, F_1: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}$ and $F_1: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}$ be functors of $\infty $-categories. Then the morphism $\overline{\sigma }: ( \bullet \rightrightarrows \bullet )^{\triangleleft } \rightarrow \operatorname{\mathcal{QC}}$ of Construction 7.6.4.19 is an equalizer diagram. In particular, the homotopy equalizer $\operatorname{hEq}( F_0, F_1)$ is an equalizer of $F_0$ and $F_1$ in the $\infty $-category $\operatorname{\mathcal{QC}}$.
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Proof. The diagram $\overline{\sigma }$ can be identified with a functor $U: \operatorname{hEq}( F_0, F_1 ) \rightarrow \operatorname{\mathcal{D}}\times ^{\mathrm{h}}_{ (\operatorname{\mathcal{C}}\times \operatorname{\mathcal{C}}) } \operatorname{\mathcal{C}}$. By virtue of Proposition 7.6.4.18, it will suffice to show that $U$ is an equivalence of $\infty $-categories. Unwinding the definitions, we see that $U$ fits into a commutative diagram
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{hEq}( F_0, F_1) \ar [r]^-{U} \ar [d] & \operatorname{\mathcal{D}}\times ^{\mathrm{h}}_{(\operatorname{\mathcal{C}}\times \operatorname{\mathcal{C}}) } \operatorname{\mathcal{C}}\ar [r] \ar [d] & \operatorname{\mathcal{D}}\times ^{\mathrm{h}}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}\ar [d] \\ \operatorname{\mathcal{D}}\ar [r] & \operatorname{\mathcal{D}}\times ^{\mathrm{h}}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}\ar [r] & \operatorname{\mathcal{D}}\times \operatorname{\mathcal{C}}, } \]
where the homotopy fiber product on the upper right is formed using the functor $F_0$, and the homotopy fiber product on the lower middle is formed using the functor $F_1$. Each of the squares in this diagram is a pullback, and the right vertical map is an isofibration (Remark 4.5.2.2). It follows that the left side of the diagram is a categorical pullback square (Corollary 4.5.2.27). Since the functor on the lower left is an equivalence of $\infty $-categories (Corollary 4.5.2.22), it follows that $U$ is an equivalence of $\infty $-categories. $\square$