Kerodon

Remark 7.7.1.12 (Cartesian Transformations as Cartesian Sections). Let $\operatorname{\mathcal{C}}$ be an $\infty $-category, let $\mathscr {G}: K \rightarrow \operatorname{\mathcal{C}}$ be a diagram, and let $\operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} K$ denote the oriented fiber product of Definition 4.6.4.1. Then projection onto the second factor determines a cocartesian fibration of simplicial sets $U: \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} K \rightarrow \operatorname{\mathcal{C}}$. By construction, sections of $U$ can be identified with pairs $(\mathscr {F}, \gamma )$, where $\mathscr {F}: K \rightarrow \operatorname{\mathcal{C}}$ is a diagram and $\gamma : \mathscr {F} \rightarrow \mathscr {G}$ is a natural transformation. In this case, the natural transformation $\gamma $ is cartesian (in the sense of Definition 7.7.1.1) if and only if the corresponding section of $U$ is cartesian: that is, it carries each edge of $K$ to a $U$-cartesian edge of $\operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} K$. This is a reformulation of Proposition 7.6.2.20.