Proposition 4.6.2.8 (05P5)

Proposition 4.6.2.8. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be an inner fibraton of $\infty $-categories. Then, for every functor of $\infty $-categories $F: \operatorname{\mathcal{C}}' \rightarrow \operatorname{\mathcal{C}}$, the inclusion map

\[ \operatorname{\mathcal{C}}' \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\hookrightarrow \operatorname{\mathcal{C}}' \times _{\operatorname{\mathcal{C}}}^{\mathrm{h}} \operatorname{\mathcal{E}} \]

is fully faithful.

Proof. For every pair of objects $X,Y \in \operatorname{\mathcal{E}}$, the functor $U$ induces a Kan fibration of morphism spaces $\operatorname{Hom}_{\operatorname{\mathcal{E}}}(X,Y) \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{C}}}( U(X), U(Y) )$ (Proposition 4.6.1.21). The desired result now follows from the criterion of Remark 4.6.2.6 (together with Example 3.4.1.3). $\square$