Proposition 7.6.2.24. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category and let $f: X \rightarrow Y$ be a morphism of $\operatorname{\mathcal{C}}$. The following conditions are equivalent:
- $(1)$
There exists a functor $f^{\ast }: \operatorname{\mathcal{C}}_{/Y} \rightarrow \operatorname{\mathcal{C}}_{/X}$ given by pullback along $f$ (in the sense of Definition 7.6.2.22).
- $(2)$
There exists a functor $f^{\ast }: \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \{ Y\} \rightarrow \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \{ X\} $ given by pullback along $f$ (in the sense of Variant 7.6.2.23).
- $(3)$
The left vertical map of the pullback square
\[ \xymatrix { \Delta ^1 \times _{\operatorname{\mathcal{C}}} \Delta ^1 \ar [r] \ar [d] & \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}}) \ar [d]^{ \operatorname{ev}_1 } \\ \Delta ^{1} \ar [r]^{f} & \operatorname{\mathcal{C}}} \]is a cartesian fibration of $\infty $-categories.
- $(4)$
For every morphism $u: Y' \rightarrow Y$, there exists a pullback diagram
\[ \xymatrix { X' \ar [r] \ar [d] & Y' \ar [d]^{u} \\ X \ar [r]^{f} & Y } \]in the $\infty $-category $\operatorname{\mathcal{C}}$.
Moreover, if these conditions are satisfied, then both pullback functors are given on objects by the construction $Y' \mapsto X \times _{Y} Y'$.