Kerodon

Proof. We first prove $(a)$. Fix an edge $e: C_0 \rightarrow C_1$ of $\operatorname{\mathcal{C}}$, let $\operatorname{\mathcal{E}}_{0}$ denote the fiber $\{ C_0 \} \times _{ \operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$, and define $\operatorname{\mathcal{E}}_{1}$ similarly. Fix an object $Y \in \operatorname{\mathcal{E}}_0$, so that we can identify the pair $(Y,e)$ with a vertex of the fiber product $\operatorname{\mathcal{E}}^{\operatorname{op}} \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}})$. Then $T(Y,e)$ can be regarded as a functor $F: \operatorname{\mathcal{E}}_{1} \rightarrow \operatorname{\mathcal{S}}^{< \kappa }$, and we wish to show that $F$ is corepresentable. Replacing $U$ by the projection map $\Delta ^1 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\rightarrow \Delta ^1$, we can reduce to the special case where $\operatorname{\mathcal{C}}= \Delta ^1$ is the standard $1$-simplex (with $C_0 = 0$ and $C_1 = 1$). Our assumption that $U$ is a cocartesian fibration guarantees that there exists a $U$-cocartesian morphism $f: Y \rightarrow X$ with $X \in \operatorname{\mathcal{E}}_1$. Let $\mathscr {H}: \operatorname{\mathcal{E}}^{\operatorname{op}} \times \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{S}}^{< \kappa }$ be a $\operatorname{Hom}$-functor for $\operatorname{\mathcal{E}}$. Using Example 8.6.6.11, we can identify $F$ with the functor

so that $f$ can be identified with a vertex of $\eta \in F(X)$. Since $f$ is $U$-cocartesian, the vertex $\eta $ exhibits $F$ as corepresented by the object $X$ (see Lemma 8.6.5.14).

We now prove $(b)$. For each vertex $C \in \operatorname{\mathcal{C}}$, the restriction of $T$ to the fiber $\operatorname{\mathcal{E}}^{\operatorname{op}} \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \{ \operatorname{id}_{C} \} $ determines a functor $T_{C}: \operatorname{\mathcal{E}}^{\operatorname{op}}_{C} \rightarrow \operatorname{Fun}^{\operatorname{corep}}( \operatorname{\mathcal{E}}_{C}, \operatorname{\mathcal{S}}^{< \kappa } )$ which is a contravariant Yoneda embedding for the $\infty $-category $\operatorname{\mathcal{E}}_{C}$ (Remark 8.6.6.14), and is therefore an equivalence of $\infty $-categories (Theorem 8.3.3.13). We will complete the proof by showing that $T$ satisfies conditions $(2')$ and $(2'')$ of Proposition 8.6.1.13. Both of these conditions make an assertion about an arbitrary edge $e: C_0 \rightarrow C_1$ of the simplicial set $\operatorname{\mathcal{C}}$; let us denote these assertions by $(2'_ e)$ and $(2''_ e)$, respectively. To verify them, we can replace $U$ by the projection map $\Delta ^1 \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\rightarrow \Delta ^1$ as above, and thereby reduce to the special case where $\operatorname{\mathcal{C}}= \Delta ^1$ is the standard $1$-simplex and $e$ is the nondegenerate edge of $\operatorname{\mathcal{C}}$. Let $\mathscr {H}: \operatorname{\mathcal{E}}^{\operatorname{op}} \times \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{S}}^{< \kappa }$ be a $\operatorname{Hom}$-functor for $\operatorname{\mathcal{E}}$. Using Example 8.6.6.11 again and Variant 8.6.5.11, we can formulate the hypotheses of Proposition 8.6.1.13 more concretely as follows:

$(2'_ e)$

For every object $Y \in \operatorname{\mathcal{E}}_0$, the functor $\mathscr {H}(Y, -): \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{S}}^{< \kappa }$ is left Kan extended from $\operatorname{\mathcal{E}}_0$.

$(2''_{e})$

For every object $Y \in \operatorname{\mathcal{E}}_0$ and every $U$-cocartesian morphism $f: Y \rightarrow X$ with $X \in \operatorname{\mathcal{E}}_1$, the induced natural transformation $\mathscr {H}(X, -) \rightarrow \mathscr {H}(Y,-)$ is an isomorphism when restricted to the subcategory $\operatorname{\mathcal{E}}_1$. In other words, for every object $W \in \operatorname{\mathcal{E}}_1$, precomposition with $f$ induces a homotopy equivalence $\mathscr {H}(X,W) \rightarrow \mathscr {H}(Y,W)$.

Assertion $(2'_ e)$ now follows from Lemma 8.6.5.13, and assertion $(2''_{e})$ from Corollary 5.1.2.3. $\square$