# Kerodon

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

Proof. We first prove $(1)$. Let $\underline{s}$, $\underline{s}'$, and $\underline{e}$ denote the images of $s$, $s'$, and $e$ under the diagonal map $S \rightarrow \operatorname{Fun}( X_{s}, S)$. Let $\overline{s}$ denote the vertex of the simplicial set $\operatorname{Fun}(X_ s, X)$ corresponding to the inclusion map $X_ s \hookrightarrow X$. Applying Corollary 4.2.3.2, we see that postcomposition with $q$ induces a left fibration $Q: \operatorname{Fun}( X_ s, X) \rightarrow \operatorname{Fun}( X_ s, S)$ satisfying $Q( \overline{s} ) = \underline{s}$. It follows that $\underline{e}$ can be lifted to an edge $\overline{e}: \overline{s} \rightarrow \overline{s}'$ of the simplicial set $\operatorname{Fun}(X_ s, X)$. Unwinding the definitions, we see that $\overline{s}'$ can be identified with a morphism of Kan complexes $f: X_{s} \rightarrow X_{s'}$ and that $\overline{e}$ can be identified with a morphism $h: \Delta ^1 \times X_{s} \rightarrow X$ which witnesses $f$ as given by covariant transport along the edge $e$.

We now prove $(2)$. Let $g: X_{s} \rightarrow X_{s'}$ be a morphism of Kan complexes. Then $g$ can be identified with a vertex $\overline{s}''$ of the simplicial set $\operatorname{Fun}( X_{s}, X)$ satisfying $Q( \overline{s}'' ) = \underline{s}'$. Unwinding the definitions, we see that $f$ is homotopic to $g$ if and only if the following condition is satisfied:

• There exists an edge $\overline{e}': \overline{s}' \rightarrow \overline{s}''$ of the simplicial set $\operatorname{Fun}( X_ s, X)$ satisfying $Q( \overline{e}' ) = \operatorname{id}_{ \underline{s}' }$.

Similarly, $g$ is given by covariant transport along $e$ if and only if the following alternative condition is satisfied:

$(\ast ')$

There exists an edge $\overline{e}'': \overline{s} \rightarrow \overline{s}''$ of the simplicial set $\operatorname{Fun}( X_ s, X)$ satisfying $Q( \overline{e}'' ) = \underline{e}$.

To complete the proof, it suffices to show that conditions $(\ast )$ and $(\ast ')$ are equivalent to one another. The implication $(\ast ) \Rightarrow (\ast ')$ follows from the observation that the left fibration $Q: \operatorname{Fun}( X_ s, X) \rightarrow \operatorname{Fun}(X_ s, S)$ has the right lifting property with respect to the horn inclusion $\Lambda ^{2}_{0} \hookrightarrow \Delta ^2$, and the implication $(\ast ') \Rightarrow (\ast )$ follows from the observation that $Q$ has the right lifting property with respect to the horn inclusion $\Lambda ^{2}_{1} \hookrightarrow \Delta ^2$. $\square$