Kerodon

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

Remark 10.3.3.18 (Functoriality of Images). Let $\operatorname{\mathcal{C}}$ be an $\infty $-category and let $\operatorname{Fun}'( \Delta ^2, \operatorname{\mathcal{C}}) \subseteq \operatorname{Fun}( \Delta ^2, \operatorname{\mathcal{C}})$ be the full subcategory described in Proposition 10.3.3.14. Then $\operatorname{\mathcal{C}}$ has images if and only if the restriction functor

\[ D: \operatorname{Fun}'( \Delta ^2, \operatorname{\mathcal{C}}) \rightarrow \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}}) \quad \quad \sigma \mapsto d^{2}_{1}( \sigma ) \]

is a trivial Kan fibration. If this condition is satisfied, then $D$ admits a section which carries each morphism $f: X \rightarrow Y$ of $\operatorname{\mathcal{C}}$ to a $2$-simplex

\[ \xymatrix@R =50pt@C=50pt{ & \operatorname{im}(f) \ar [dr] & \\ X \ar [ur] \ar [rr]^{f} & & Y } \]

which exhibits $\operatorname{im}(f)$ as an image of $f$. In particular, we can promote the construction $f \mapsto \operatorname{im}(f)$ as a functor of $\infty $-categories $\operatorname{Fun}(\Delta ^1,\operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{C}}$.