Proposition 5.2.2.18. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a Kan fibration of simplicial sets and let $f: C \rightarrow D$ be an edge of $\operatorname{\mathcal{C}}$. Then the covariant and contravariant transport morphisms $[f_{!}] \in \operatorname{Hom}_{ \mathrm{h} \mathit{\operatorname{Kan}}}( \operatorname{\mathcal{E}}_{C}, \operatorname{\mathcal{E}}_{D} )$ and $[ f^{\ast } ] \in \operatorname{Hom}_{ \mathrm{h} \mathit{\operatorname{Kan}} }( \operatorname{\mathcal{E}}_{D}, \operatorname{\mathcal{E}}_{C} )$ are inverse to one another (as morphisms in the homotopy category $\mathrm{h} \mathit{\operatorname{Kan}}$).
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Proof. Choose morphisms of Kan complexes $f_{!}: \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{D}$ and $f^{\ast }: \operatorname{\mathcal{E}}_{D} \rightarrow \operatorname{\mathcal{E}}_{C}$ representing the homotopy classes $[f_{!}]$ and $[ f^{\ast } ]$, respectively. We will show that $f^{\ast } \circ f_{!}$ is homotopic to the identity morphism $\operatorname{id}_{\operatorname{\mathcal{E}}_{C} }$; a similar argument will show that $f_{!} \circ f^{\ast }$ is homotopic to $\operatorname{id}_{ \operatorname{\mathcal{E}}_{D} }$. Let $\operatorname{\mathcal{D}}$ denote the fiber product $\operatorname{Fun}( \operatorname{\mathcal{E}}_{C}, \operatorname{\mathcal{E}}) \times _{ \operatorname{Fun}( \operatorname{\mathcal{E}}_{C}, \operatorname{\mathcal{C}}) } \operatorname{\mathcal{C}}$, and let $\pi : \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}$ be the projection map onto the second factor. Since $U$ is a Kan fibration, it follows from Corollary 3.1.3.2 that $\pi $ is also a Kan fibration. Let $\widetilde{f}: \Delta ^{1} \times \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}$ be a morphism witnessing $f_{!}$ as given by covariant transport along $f$. Then $\widetilde{f}$ determines an edge $h$ of the simplicial set $\operatorname{\mathcal{D}}$ satisfying $\pi ( h ) = f$. Let $\widetilde{f}': \Delta ^1 \times \operatorname{\mathcal{E}}_{D} \rightarrow \operatorname{\mathcal{E}}$ be a morphism which witnesses $f^{\ast }$ as given by contravariant transport along $f$, so that the composite morphism
\[ \Delta ^{1} \times \operatorname{\mathcal{E}}_{C} \xrightarrow { \operatorname{id}\times f_{!} } \Delta ^1 \times \operatorname{\mathcal{E}}_{D} \xrightarrow { \widetilde{f}' } \operatorname{\mathcal{E}} \]
determines an edge $h'$ of the simplicial set $\operatorname{\mathcal{D}}$ satisfying $\pi (h') = f$. The edges $h$ and $h'$ have the same target (the vertex of $\operatorname{\mathcal{D}}$ corresponding to the morphism $f_{!}$). Invoking our assumption that $\pi $ is a Kan fibration, we deduce that there exists a $2$-simplex $\sigma $ of $\operatorname{\mathcal{D}}$ satisfying $d^{2}_0(\sigma ) = h'$, $d^{2}_1(\sigma ) = h$, and $\pi (\sigma ) = s^{1}_0(f)$; we can represent $\sigma $ as a diagram
\[ \xymatrix@R =50pt@C=50pt{ & f^{\ast } \circ f_{!} \ar [dr]^{h' } & \\ \operatorname{id}_{\operatorname{\mathcal{E}}_{C}} \ar@ {-->}[ur]^{v} \ar [rr]^-{ h } & & f_{!}. } \]
We now observe that the edge $v = d^{2}_2(\sigma )$ of $\operatorname{\mathcal{D}}$ can be identified with a map of simplicial sets $V: \Delta ^1 \times \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{C}$ which is a homotopy from $\operatorname{id}_{\operatorname{\mathcal{E}}_{C}} = V|_{ \{ 0\} \times \operatorname{\mathcal{E}}_{C} }$ to $f^{\ast } \circ f_! = V|_{ \{ 1\} \times \operatorname{\mathcal{E}}_{C} }$. $\square$