# Kerodon

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

Construction 4.5.2.1 (The Homotopy Fiber Product of $\infty$-Categories). Let $\operatorname{\mathcal{C}}$ be an $\infty$-category, and let $\operatorname{Isom}(\operatorname{\mathcal{C}}) \subseteq \operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{C}})$ denote the full subcategory spanned by the isomorphisms in $\operatorname{\mathcal{C}}$ (Example 4.4.1.13). If $\operatorname{\mathcal{C}}_0$ and $\operatorname{\mathcal{C}}_1$ are $\infty$-categories equipped with functors $F_0: \operatorname{\mathcal{C}}_0 \rightarrow \operatorname{\mathcal{C}}$ and $F_1: \operatorname{\mathcal{C}}_1 \rightarrow \operatorname{\mathcal{C}}$, we let $\operatorname{\mathcal{C}}_0 \times ^{\mathrm{h}}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_1$ denote the iterated pullback

$\operatorname{\mathcal{C}}_0 \times _{ \operatorname{Fun}( \{ 0\} , \operatorname{\mathcal{C}}) } \operatorname{Isom}(\operatorname{\mathcal{C}}) \times _{ \operatorname{Fun}( \{ 1\} , \operatorname{\mathcal{C}}) } \operatorname{\mathcal{C}}_1.$

We will refer to $\operatorname{\mathcal{C}}_{0} \times ^{\mathrm{h}}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_1$ as the homotopy fiber product of $\operatorname{\mathcal{C}}_0$ with $\operatorname{\mathcal{C}}_1$ over $\operatorname{\mathcal{C}}$. Note that the diagonal map $\operatorname{\mathcal{C}}\rightarrow \operatorname{Isom}(\operatorname{\mathcal{C}}) \subseteq \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}})$ induces a comparison map $\operatorname{\mathcal{C}}_{0} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{1} \hookrightarrow \operatorname{\mathcal{C}}_{0} \times ^{\mathrm{h}}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{1}$, which is a monomorphism of simplicial sets.