Kerodon

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

Construction 8.6.2.2. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of simplicial sets, and let $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{Tw}(\operatorname{\mathcal{C}}) / \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{E}})$ be the simplicial set given in Notation 8.6.2.1. Unwinding the definitions, we see that vertices of $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{Tw}(\operatorname{\mathcal{C}}) / \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{E}})$ can be identified with pairs $(C, f_{C} )$, where $C$ is an object of $\operatorname{\mathcal{C}}$ and $f_{C}$ is a morphism which fits into a commutative diagram

\[ \xymatrix@R =50pt@C=50pt{ \{ C\} \times _{\operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}) \ar [dr] \ar [rr]^{f_{C}} & & \operatorname{\mathcal{E}}\ar [dl]^{U} \\ & \operatorname{\mathcal{C}}. & } \]

We let $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{Tw}(\operatorname{\mathcal{C}}) / \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{E}})$ denote the full simplicial subset of $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( \operatorname{Tw}(\operatorname{\mathcal{C}}) / \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{E}})$, spanned by those pairs $(C, f_{C} )$ where the morphism $f_{C}$ carries each edge of $\{ C\} \times _{\operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}})$ to a $U$-cocartesian edge of $\operatorname{\mathcal{E}}$. By construction, the simplicial set $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{Tw}(\operatorname{\mathcal{C}}) / \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{E}})$ is equipped with a projection map $V: \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{Tw}(\operatorname{\mathcal{C}}) / \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{E}}) \rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}}$ and an evaluation map $\operatorname{ev}: \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}^{\operatorname{CCart}}( \operatorname{Tw}(\operatorname{\mathcal{C}}) / \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{E}}) \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{E}}$, given on vertices by the construction $(C, f_{C}, u: C \rightarrow C') \mapsto f_{C}(u)$.