# Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$

Proposition 5.1.2.1. Let $q: X \rightarrow S$ be a Kan fibration of simplicial sets and let $e: s \rightarrow s'$ be an edge of $S$. Then the morphisms $e_{!}: X_{s} \rightarrow X_{s'}$ and $e^{\ast }: X_{s'} \rightarrow X_{s}$ are homotopy inverse to one another.

Proof. We will show that the composition $e^{\ast } \circ e_{!}$ is homotopic to the identity map $\operatorname{id}_{ X_ s }$; a similar argument will show that $e_{!} \circ e^{\ast }$ is homotopic to the identity map $\operatorname{id}_{ X_{s'} }$. As in the proof of Proposition 5.1.1.4, we let $\underline{e}$ denote the image of $e$ along the diagonal map $S \rightarrow \operatorname{Fun}( X_ s, S)$, and let $Q: \operatorname{Fun}( X_ s, X) \rightarrow \operatorname{Fun}(X_ s, S)$ be the morphism given by postcomposition with $q$. Let $h: \Delta ^1 \times X_ s \rightarrow X$ be a morphism of simplicial sets which exhibits $e_{!}$ as given by covariant transport along $e$, so that $h$ can be identified with an edge $\overline{e}: \operatorname{id}_{X_ s} \rightarrow e_{!}$ of the simplicial set $\operatorname{Fun}(X_ s, X)$ satisfying $Q( \overline{e} ) = \underline{e}$. Let $h': \Delta ^1 \times X_{s'} \rightarrow X$ be a morphism of simplicial sets which exhibits $e^{\ast }$ as given by contravariant transport along $e$. Then the composite map

$\Delta ^{1} \times X_{s} \xrightarrow { \operatorname{id}\times e_{!} } \Delta ^1 \times X_{s'} \xrightarrow {h'} X$

can be identified with an edge $\overline{e}': (e^{\ast } \circ e_{!}) \rightarrow e_{!}$ of $\operatorname{Fun}( X_ s, X)$ satisfying $Q(\overline{e}' ) = \underline{e}$. Since $Q$ is a Kan fibration (Corollary 3.1.3.2), the lifting problem

$\xymatrix@C =50pt@R=50pt{ \Lambda ^{2}_{2} \ar [r]^-{(\overline{e}', \overline{e}, \bullet )} \ar [d] & \operatorname{Fun}( X_ s, X) \ar [d]^{Q} \\ \Delta ^{2} \ar@ {-->}[ur]^-{\sigma } \ar [r]^-{ s_0( \underline{e} )} & \operatorname{Fun}(X_ s, S) }$

admits a solution. Here $\sigma$ is a $2$-simplex of the simplicial set $\operatorname{Fun}(X_ s, X)$ which we can display as a diagram

$\xymatrix@R =50pt@C=50pt{ & e^{\ast } \circ e_{!} \ar [dr]^{ \overline{e}' } & \\ \operatorname{id}_{ X_ s } \ar [ur]^{h''} \ar [rr]^{ \overline{e} } & & e_{!}. }$

By construction, the edge $h''$ can be regarded as a homotopy from $\operatorname{id}_{X_ s}$ to the composite map $e^{\ast } \circ e_{!}$. $\square$