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.14). 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
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.