Kerodon

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

Proposition 8.6.4.16. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a left fibration of simplicial sets, and set $\widetilde{\operatorname{\mathcal{E}}} = \operatorname{\mathcal{C}}\times _{ \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{E}}) } \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{E}})$. Then the evaluation maps $\operatorname{ev}_0, \operatorname{ev}_1: \widetilde{\operatorname{\mathcal{E}}} \rightarrow \operatorname{\mathcal{E}}$ determine a left fibration $\lambda : \widetilde{\operatorname{\mathcal{E}}} \rightarrow \operatorname{\mathcal{E}}\times _{ \operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$ which exhibits $U$ as a cocartesian dual of itself.

Proof. The morphism $\lambda $ is a pullback of the restriction map

\[ \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{E}}) \rightarrow \operatorname{Fun}( \operatorname{\partial \Delta }^1, \operatorname{\mathcal{E}}) \times _{ \operatorname{Fun}( \operatorname{\partial \Delta }^1, \operatorname{\mathcal{C}}) } \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}}), \]

and is therefore a left fibration by virtue of Proposition 4.2.5.1. For every vertex $C \in \operatorname{\mathcal{C}}$, we can identify $\lambda _{C}$ with the coupling

\[ \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{E}}_{C} ) \rightarrow \operatorname{Fun}( \{ 0\} , \operatorname{\mathcal{E}}_{C} ) \times \operatorname{Fun}( \{ 1\} , \operatorname{\mathcal{E}}_{C} ). \]

It follows from Example 8.2.6.3 that each $\lambda _{C}$ is a balanced coupling, so that $\lambda $ satisfies condition $(a)$ of Definition 8.6.4.1. Moreover, every object of $\operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{E}}_{C} )$ is universal for the coupling $\lambda _{C}$, so that condition $(b)$ of Definition 8.6.4.1 is vacuous. $\square$