Kerodon

Notation 7.7.2.1. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cartesian fibration of simplicial sets. For every morphism of simplicial sets $F: K \rightarrow \operatorname{\mathcal{C}}$, recall that the simplicial set $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}(K, \operatorname{\mathcal{E}})$ is an $\infty $-category (Corollary 4.1.4.8), whose objects are given by morphisms $\widetilde{F}: K \rightarrow \operatorname{\mathcal{E}}$ satisfying $U \circ \widetilde{F} = F$. We let $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{ACart}}(K, \operatorname{\mathcal{E}})$ denote the full subcategory spanned by those objects where $\widetilde{F}$ carries every edge of $K$ to a $U$-cartesian edge of $\operatorname{\mathcal{E}}$.