Kerodon

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

Proposition 4.4.4.9. Let $q: X \rightarrow S$ be an inner fibration of simplicial sets, let $\overline{F}: B \rightarrow S$ be a morphism of simplicial sets, and let $u: F \rightarrow F'$ be a morphism in the $\infty $-category $\operatorname{Fun}_{/S}(B, X)$. The following conditions are equivalent:

$(1)$

The morphism $u$ is an isomorphism in the $\infty $-category $\operatorname{Fun}_{/S}(B,X)$.

$(2)$

For every vertex $b \in B$, the morphism $u_ b: F(b) \rightarrow F'(b)$ is an isomorphism in the $\infty $-category $X_{b} = \{ \overline{F}(b) \} \times _{S} X$.

Proof. For each vertex $b \in B$, evaluation at $b$ determines a functor of $\infty $-categories $\operatorname{Fun}_{/S}(B,X) \rightarrow X_{b}$. Consequently, the implication $(1) \Rightarrow (2)$ follows from Remark 1.5.1.6. The converse implication follows by combining Lemma 4.4.4.8 (in the special case $A = \emptyset $) with the criterion of Theorem 4.4.2.6. $\square$