# Kerodon

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

Proposition 3.1.6.6. Let $\operatorname{\mathcal{C}}$ be a category and let $F: \operatorname{Kan}\rightarrow \operatorname{\mathcal{C}}$ be a functor. The following conditions are equivalent:

$(\ast )$

If $X$ and $Y$ are Kan complexes and $u_0, u_1: X \rightarrow Y$ are homotopic morphisms, then $F(u_0) = F(u_1)$ in $\operatorname{Hom}_{\operatorname{\mathcal{C}}}( F(X), F(Y) )$.

$(\ast ')$

For every homotopy equivalence of Kan complexes $u: X \rightarrow Y$, the induced map $F(u): F(X) \rightarrow F(Y)$ is an isomorphism in the category $\operatorname{\mathcal{C}}$.

Proof. The implication $(\ast ) \Rightarrow (\ast ')$ is immediate (note that a morphism of Kan complexes $u: X \rightarrow Y$ is a homotopy equivalence if and only if its homotopy class $[u]$ is an isomorphism in the homotopy category $\mathrm{h} \mathit{\operatorname{Kan}}$). For the converse, assume that $(\ast ')$ is satisfied, let $X$ and $Y$ be Kan complexes, and let $u_0, u_1: X \rightarrow Y$ be a pair of homotopic morphisms. Let us regard $u_0$ and $u_1$ as vertices of the Kan complex $\operatorname{Fun}(X,Y)$. Since $u_0$ and $u_1$ are homotopic, there exists an edge $e: \Delta ^1 \rightarrow \operatorname{Fun}(X,Y)$ satisfying $e(0) = u_0$ and $e(1) = u_1$. By virtue of Proposition 3.1.6.1, this morphism factors as a composition $\Delta ^1 \xrightarrow {e'} Q \xrightarrow {e''} \operatorname{Fun}(X,Y)$, where $e'$ is anodyne and $e''$ is a Kan fibration. Since $\operatorname{Fun}(X,Y)$ is a Kan complex (Corollary 3.1.3.4), it follows that $Q$ is also a Kan complex. Let us identify $e''$ with a morphism of Kan complexes $h: Q \times X \rightarrow Y$. Let $i_0: X \hookrightarrow Q \times X$ be the product of the identity map $\operatorname{id}_{X}$ with the inclusion $\{ e'(0) \} \hookrightarrow Q$, and define $i_1: X \hookrightarrow Q \times X$ similarly. Since $e'$ is anodyne, the restrictions $e'|_{\{ 0\} }$ and $e'|_{\{ 1\} }$ are anodyne. In particular, they are weak homotopy equivalences (Proposition 3.1.5.13) and therefore homotopy equivalences (Proposition 3.1.5.12), since $Q$ is a Kan complex. It follows that $i_0$ and $i_1$ are also homotopy equivalences, so that $F(i_0)$ and $F(i_1)$ are isomorphisms (by virtue of assumption $(\ast ')$). Using the fact that $i_0$ and $i_1$ are left inverse to the projection map $\pi : Q \times X \rightarrow X$, we see that $F(\pi )$ is an isomorphism in $\operatorname{\mathcal{C}}$ and that we have

$F(u_0) = F(h) \circ F(i_0) = F(h) \circ F(\pi )^{-1} = F(h) \circ F(i_1) = F(u_1),$

as desired. $\square$