Corollary 6.2.4.8. Let $F_0: \operatorname{\mathcal{C}}_0 \rightarrow \operatorname{\mathcal{C}}$ and $F_1: \operatorname{\mathcal{C}}_1 \rightarrow \operatorname{\mathcal{C}}$ be functors of $\infty $-categories and let $\operatorname{\mathcal{E}}$ denote the oriented fiber product $\operatorname{\mathcal{C}}_0 \operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_1$ (see Definition 4.6.4.1). Assume that $F_0$ is a left fibration. Then the homotopy fiber product $\operatorname{\mathcal{E}}' = \operatorname{\mathcal{C}}_0 \times _{\operatorname{\mathcal{C}}}^{\mathrm{h}} \operatorname{\mathcal{C}}_1$ is a reflective subcategory of $\operatorname{\mathcal{E}}$. Moreover, if $w$ is a morphism in $\operatorname{\mathcal{E}}$, the following conditions are equivalent:
- $(1)$
The morphism $w$ is a $\operatorname{\mathcal{E}}'$-local equivalence (Definition 6.2.2.1).
- $(2)$
The projection functor $\operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}_1$ carries $w$ to an isomorphism in the $\infty $-category $\operatorname{\mathcal{C}}_1$.
- $(3)$
The morphism $w$ is $U$-cartesian, where $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}_0$ is given by projection onto the first factor.