Kerodon

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

Remark 7.1.7.8. Let $U: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be a functor of $\infty $-categories, let $\overline{f}: K^{\triangleleft } \rightarrow \operatorname{\mathcal{C}}$ be a morphism, and set $f = \overline{f}|_{K}$, so that $U$ induces a functor

\[ U': \operatorname{\mathcal{C}}_{ / \overline{f} } \rightarrow \operatorname{\mathcal{C}}_{/f} \times _{ \operatorname{\mathcal{D}}_{/(U \circ f)}} \operatorname{\mathcal{D}}_{ / (U \circ \overline{f} ) }. \]

By virtue of Proposition 7.1.6.12, the following conditions are equivalent:

$(1)$

The morphism $\overline{f}$ is a $U$-limit diagram.

$(2)$

The functor $U'$ is an equivalence of $\infty $-categories.

If $U$ is an inner fibration of $\infty $-categories, then the functor $U'$ is automatically a right fibration (Proposition 4.3.6.8). In this case, we can replace $(1)$ and $(2)$ by either of the following conditions: to the following:

$(3)$

The functor $U'$ is a trivial Kan fibration.

$(4)$

Each fiber of $U'$ is a contractible Kan complex.

The equivalence of $(2) \Leftrightarrow (3)$ follows from Proposition 4.5.7.16, and the equivalence $(3) \Leftrightarrow (4)$ from Proposition 4.4.2.14.