Proposition 7.6.2.20. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category, let $\operatorname{ev}_{1}: \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{C}}$ be the functor given by evaluation at the vertex $1 \in \Delta ^1$, and let $\sigma : \Delta ^1 \times \Delta ^1 \rightarrow \operatorname{\mathcal{C}}$ be a diagram, which we display informally as
\[ \xymatrix { X' \ar [r]^{g'} \ar [d]^{f'} & X \ar [d]^{f} \\ Y' \ar [r]^{g} & Y } \]
be a diagram in $\operatorname{\mathcal{C}}$. The following conditions are equivalent:
- $(1)$
The diagram $\sigma $ is a pullback square (Definition 7.6.2.1).
- $(2)$
Let $u: f' \rightarrow f$ be the morphism in $\operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{C}})$ determined by $\sigma $. Then $u$ is $\operatorname{ev}_{1}$-cartesian.
- $(3)$
The morphism $u: f' \rightarrow f$ is locally $\operatorname{ev}_{1}$-cartesian.
Proof of Proposition 7.6.2.20.
Since the evaluation functor $\operatorname{ev}_{1}: \operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{C}}$ is a cocartesian fibration (Example 5.3.7.5), the equivalence $(2) \Leftrightarrow (3)$ is a special case of Lemma 6.2.3.5. We will prove that $(1) \Leftrightarrow (2)$. Let $K$ denote the nerve of the partially ordered set $\{ (0,1) < (1,1) > (1,0) \} $, which we regard as a full subcategory of $\Delta ^1 \times \Delta ^1$, and let $U: \operatorname{Fun}( \Delta ^1 \times \Delta ^1, \operatorname{\mathcal{C}}) \rightarrow \operatorname{Fun}(K, \operatorname{\mathcal{C}})$ be the restriction map. Then $\sigma $ is a pullback diagram in $\operatorname{\mathcal{C}}$ if and only if it is $U$-final when viewed as an object of the $\infty $-category $\operatorname{Fun}( \Delta ^1 \times \Delta ^1, \operatorname{\mathcal{C}})$ (Proposition 7.1.7.4). Unwinding the definitions, we have a pullback diagram of simplicial sets
\[ \xymatrix { \operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{C}}) \operatorname{\vec{\times }}_{ \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}}) } \{ f \} \ar [r] \ar [d]^{U_0} & \operatorname{Fun}( \Delta ^1 \times \Delta ^1, \operatorname{\mathcal{C}}) \ar [d]^{U} \\ \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{ \operatorname{\mathcal{C}}} \{ Y\} & \operatorname{Fun}(K, \operatorname{\mathcal{C}}), } \]
and the morphism $u$ is $\operatorname{ev}_{1}$-cartesian if and only if it is $U_0$-final when viewed as an object of the $\infty $-category $\operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{C}}) \operatorname{\vec{\times }}_{ \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}}) } \{ f \} $ (Example 7.1.6.9). The equivalence $(1) \Leftrightarrow (2)$ now follows from the criterion of Corollary 7.1.5.21, since $U$ is a cocartesian fibration (Corollary 5.3.7.4).
$\square$