Kerodon

Proof. Let $\operatorname{\mathcal{K}}$ denote the simplicial set given by the product $( \bullet \rightrightarrows \bullet )^{\triangleleft } \times \Delta ^1$. Then $\operatorname{\mathcal{K}}$ is an $\infty $-category, which we depict informally by the diagram

We now proceed in several steps.

• Let $\operatorname{\mathcal{K}}_{0}$ denote the full subcategory of $\operatorname{\mathcal{K}}$ spanned by the objects $x$ and $y$. Then $\operatorname{\mathcal{K}}_0$ is isomorphic to the simplicial set $( \bullet \rightrightarrows \bullet )$. In particular, the pair of morphisms $f_0, f_1: Y \rightarrow X$ can be identified with a functor $\sigma _0: \operatorname{\mathcal{K}}_0 \rightarrow \operatorname{\mathcal{C}}$, satisfying $\sigma _0( x ) = X$ and $\sigma _0( y ) = Y$. By definition, an object of $\operatorname{\mathcal{C}}$ is an equalizer of the pair $(f_0, f_1)$ if and only if it is a limit of the diagram $\sigma _0$.

• Let $\operatorname{\mathcal{K}}_1$ denote the full subcategory of $\operatorname{\mathcal{K}}$ spanned by the objects $x$, $x'$, and $y$. Note that the identity map $\operatorname{id}_{ \operatorname{\mathcal{K}}_0 }$ extends uniquely to a retraction $r: \operatorname{\mathcal{K}}_1 \rightarrow \operatorname{\mathcal{K}}_0$, carrying the object $x' \in \operatorname{\mathcal{K}}_1$ to $x \in \operatorname{\mathcal{K}}_0$. Let $\sigma _1: \operatorname{\mathcal{K}}_1 \rightarrow \operatorname{\mathcal{C}}$ be the composition $\sigma _0 \circ r$. Note that that the inclusion map $\operatorname{\mathcal{K}}_0 \hookrightarrow \operatorname{\mathcal{K}}_1$ admits a right adjoint (given by the retraction $r$), and is therefore left cofinal (Corollary 7.2.3.7). It follows that an object of $\operatorname{\mathcal{C}}$ is a limit of the diagram $\sigma _0$ if and only if it is a limit of the diagram $\sigma _1$ (Corollary 7.2.2.11).

• Choose a pair of morphisms $\pi _0, \pi _1: X \times X \rightarrow X$ in the $\infty $-category $\operatorname{\mathcal{C}}$ which exhibit $X \times X$ as a product of $X$ with itself. The morphism $(f_0, f_1): Y \rightarrow X$ is characterized (up to homotopy) by the requirement that there exist $2$-simplices $\sigma _0$ and $\sigma _1$ of $\operatorname{\mathcal{C}}$, where $\sigma _ i$ exhibits $f_ i$ as a composition of $\pi _ i$ with $(f_0, f_1)$. Let $\operatorname{\mathcal{K}}_2$ denote the full subcategory of $\operatorname{\mathcal{K}}$ spanned by the objects $x$, $x'$, $y$, and $y'$. Then the pair $(\sigma _0, \sigma _1)$ determines an extension of $\sigma _1$ to a functor $\sigma _2: \operatorname{\mathcal{K}}_2 \rightarrow \operatorname{\mathcal{C}}$ satisfying $\sigma _2(y') = X \times X$.

• The diagonal morphism $\delta _{X}: X \rightarrow X \times X$ is characterized (up to homotopy) by the requirement that there exist $2$-simplices $\tau _0$ and $\tau _ i$ of $\operatorname{\mathcal{C}}$, where $\tau _ i$ exhibits $\operatorname{id}_{X}$ as a composition of $\pi _ i$ with $\delta _{X}$. Let $\operatorname{\mathcal{K}}_3$ denote the full subcategory of $\operatorname{\mathcal{K}}$ spanned by the objects $x$, $x'$, $y$, and $y'$, and $z'$. Then the pair $(\tau _0, \tau _1)$ determines an extension of $\sigma _2$ to a functor $\sigma _3: \operatorname{\mathcal{K}}_3 \rightarrow \operatorname{\mathcal{C}}$ satisfying $\sigma _3(z') = X$. The diagram $\sigma _3$ can be represented informally by the diagram

  \[ \xymatrix@R =50pt@C=50pt{ \bullet \ar@ {-->}[r] \ar@ {-->}[d] & Y \ar@ <.4ex>[r]^{f_0} \ar@ <-.4ex>[r]_{f_1} \ar [d]^-{ (f_0, f_1) } & X \ar [d]^-{\operatorname{id}_ X} \\ X \ar [r]^-{\delta _ X} & X \times X \ar@ <.4ex>[r]^{\pi _0} \ar@ <-.4ex>[r]_{\pi _1} & X. } \]

  Note that $\sigma _3$ is right Kan extended from the full subcategory $\operatorname{\mathcal{K}}_1 \subseteq \operatorname{\mathcal{K}}_3$. Consequently, an object of $\operatorname{\mathcal{C}}$ is a limit of the diagram $\sigma _1$ if and only if it is a limit of the diagram $\sigma _3$ (Remark 7.3.8.15).

• Let $\operatorname{\mathcal{K}}_{4}$ denote the full subcategory of $\operatorname{\mathcal{K}}$ spanned by the objects $x'$, $y$, $y'$, and $z'$. Note that the functor $\sigma _3$ is right Kan extended from $\operatorname{\mathcal{K}}_4$. It follows that an object of $\operatorname{\mathcal{C}}$ is a limit of the functor $\sigma _3$ if and only if it is a limit of the functor $\sigma _4 = \sigma _3 |_{\operatorname{\mathcal{K}}_4}$.

• Let $\operatorname{\mathcal{K}}_5$ denote the full subcategory of $\operatorname{\mathcal{K}}$ spanned by the objects $y$, $y'$, and $z'$. Using the criterion of Theorem 7.2.3.1, we see that the inclusion $\operatorname{\mathcal{K}}_{5} \hookrightarrow \operatorname{\mathcal{K}}_4$ is left cofinal. It follows that an object of $\operatorname{\mathcal{C}}$ is a limit of the diagram $\sigma _4$ if and only if it is a limit of the diagram $\sigma _5 = \sigma _4 |_{ \operatorname{\mathcal{K}}_5}$ (Corollary 7.2.2.11).

Combining these steps, we deduce that an object of $\operatorname{\mathcal{C}}$ is an equalizer of $f_0$ and $f_1$ if and only if it is a limit of the diagram $\sigma _5$: that is, if and only if it is a fiber product of $Y$ with $X$ over $X \times X$ (along the morphisms $(f_0, f_1)$ and $\delta _ X$). $\square$