Kerodon

Proof. Let $H: \mathrm{h} \mathit{( \operatorname{\mathcal{C}}^{\operatorname{op}})} \times \mathrm{h} \mathit{\operatorname{\mathcal{C}}} \rightarrow \mathrm{h} \mathit{\operatorname{Kan}}$ denote the homotopy transport representation for the left fibration $(\lambda _{-}, \lambda _{+})$, given on objects by the formula $H(X,Y) = \{ X\} \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}) \times _{\operatorname{\mathcal{C}}} \{ Y\} $. For every pair of objects $X,Y \in \operatorname{\mathcal{C}}$, Notation 8.1.2.14 determines an isomorphism

in the homotopy category $\mathrm{h} \mathit{\operatorname{Kan}}$. We wish to show that $\alpha _{X,Y}$ depends functorially on $X$ and $Y$.

We first establish a strong form of functoriality in $Y$. Fix an object $X \in \operatorname{\mathcal{C}}$, and let $h^{X}: \mathrm{h} \mathit{\operatorname{\mathcal{C}}} \rightarrow \mathrm{h} \mathit{\operatorname{Kan}}$ denote the $\mathrm{h} \mathit{\operatorname{Kan}}$-enriched functor corepresented by $X$, given concretely by the formula $h^{X}(Y) = \underline{\operatorname{Hom}}_{\mathrm{h} \mathit{\operatorname{\mathcal{C}}}}(X,Y) = \operatorname{Hom}_{\operatorname{\mathcal{C}}}(X,Y)$. Let $H^{X}: \mathrm{h} \mathit{\operatorname{\mathcal{C}}} \rightarrow \mathrm{h} \mathit{\operatorname{Kan}}$ denote the restriction $H|_{ \{ X\} \times \mathrm{h} \mathit{\operatorname{\mathcal{C}}} }$, which we also regard as an $\mathrm{h} \mathit{\operatorname{Kan}}$-enriched functor (using Variant 5.2.8.11). Note that $h^{X}$ can be identified with the (enriched) homotopy transport representation of the left fibration $\{ X\} \operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}$ (see Example 5.2.8.13). Corollary 4.6.4.18 and Proposition 8.1.2.9 supply equivalences

of left fibrations over $\operatorname{\mathcal{C}}$, which induce an isomorphism of $\mathrm{h} \mathit{\operatorname{Kan}}$-enriched functors $\alpha _{X,-}: h^{X} \xrightarrow {\sim } H^{X}$. By construction, this isomorphism carries each object $Y \in \mathrm{h} \mathit{\operatorname{\mathcal{C}}}$ to the isomorphism $\alpha _{X,Y}: \underline{\operatorname{Hom}}(X,Y) \xrightarrow {\sim } H(X,Y)$ of Notation 8.1.2.14, which proves that $\alpha _{X,Y}$ depends functorially on $Y$.

We now show that $\alpha _{X,Y}$ depends functorially on $X$. Fix a morphism $f: W \rightarrow X$ in the $\infty $-category $\operatorname{\mathcal{C}}$. We then have a diagram of $\mathrm{h} \mathit{\operatorname{Kan}}$-enriched functors

where the vertical maps are induced by the homotopy class $[f] \in \operatorname{Hom}_{\mathrm{h} \mathit{\operatorname{\mathcal{C}}}^{\operatorname{op}} }(X,W)$. To complete the proof, it will suffice to show that this diagram commutes. Using the corepresentability of the $\mathrm{h} \mathit{\operatorname{Kan}}$-enriched functor $h^{X}$, we are reduced to showing that clockwise and counterclockwise composition around the diagram (8.4) carry $[ \operatorname{id}_{X} ] \in \pi _0( h^{X}(X) ) = \operatorname{Hom}_{\mathrm{h} \mathit{\operatorname{\mathcal{C}}}}(X,X)$ to the same element of $\pi _0( H^{W}(X) )$. We conclude by observing that under the identification $\pi _0( H^ W(X) ) \simeq \operatorname{Hom}_{\mathrm{h} \mathit{\operatorname{\mathcal{C}}}}(W,X)$ supplied by Corollary 8.1.2.11, both constructions carry $[ \operatorname{id}_{X} ]$ to $[f]$ (Exercise 8.1.2.13). $\square$