Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$ $\newcommand\empty{}$
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$

Construction 7.6.5.19 (The Homotopy Equalizer). Let $F_0, F_1: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}$ be functors of $\infty $-categories, and form a pullback diagram of simplicial sets

\[ \xymatrix@R =50pt@C=50pt{ \operatorname{hEq}(F_0, F_1) \ar [r] \ar [d]^-{G} & \operatorname{Isom}(\operatorname{\mathcal{C}}) \ar [d] \\ \operatorname{\mathcal{D}}\ar [r]^-{ (F_0, F_1) } & \operatorname{\mathcal{C}}\times \operatorname{\mathcal{C}}. } \]

Note that the right vertical map is an isofibration (Corollary 4.4.5.5), so the left vertical map is also an isofibration; in particular, $\operatorname{hEq}(F_0, F_1)$ is an $\infty $-category. We will refer to $\operatorname{hEq}( F_0, F_1 )$ as the homotopy equalizer of the functors $F_0$ and $F_1$. By construction, objects of $\operatorname{hEq}(F_0, F_1)$ can be identified with pairs $(X, u)$, where $X$ is an object of $\operatorname{\mathcal{D}}$ and $u: F_0(X) \rightarrow F_1(X)$ is an isomorphism in the $\infty $-category $\operatorname{\mathcal{C}}$.

Set $H = G \circ F_1$, so that the construction $(X,u) \mapsto u$ determines an isomorphism $\alpha _0: G \circ F_0 \xrightarrow {\sim } H$ in the $\infty $-category $\operatorname{Fun}( \operatorname{Eq}(F_0, F_1), \operatorname{\mathcal{C}})$. Taking $\alpha _1$ to be the identity morphism $\operatorname{id}: G \circ F_1 \xrightarrow {\sim } H$, we see that the quadruple $(G,H, \alpha _0, \alpha _1 )$ determines a diagram $\overline{\sigma }: ( \bullet \rightrightarrows \bullet )^{\triangleleft } \rightarrow \operatorname{\mathcal{QC}}$, carrying the cone point to the homotopy equalizer $\operatorname{hEq}(F_0, F_1)$ (see Remark 7.6.5.17).