Kerodon

Proof. Let $g: Y \rightarrow X$ be a left homotopy inverse of $f$. Then there exists a homotopy $\alpha : \Delta ^1 \times X \rightarrow X$ from the identity morphism $\operatorname{id}_{X} = \alpha |_{ \{ 0\} \times X }$ to $g \circ f = \alpha |_{ \{ 1\} \times X}$. Then the restriction $\alpha |_{ \Delta ^1 \times \{ x\} }$ determines an edge $e: x \rightarrow g(y)$ of $X$. Since $X$ is a Kan complex, we can use Remark 3.1.5.3 to construct another map $g': Y \rightarrow X$ and a homotopy $\beta : \Delta ^1 \times Y \rightarrow X$ from $g' = \beta |_{ \{ 0\} \times Y }$ to $g = \beta |_{ \{ 1\} \times Y}$, such that $\beta |_{ \{ y\} \times \Delta ^1 }$ is the edge $e$. Precomposing $\beta $ with $\operatorname{id}_{ \Delta ^1 } \times f$, we obtain a homotopy $\beta _{f}$ from $g' \circ f$ to $g \circ f$. Let $\sigma = s^{1}_{0}(e)$ denote the degenerate $2$-simplex of $X$ depicted in the diagram

Corollary 3.1.3.3 guarantees that the evaluation map $\operatorname{ev}_{x}: \operatorname{Fun}( X, X ) \rightarrow \operatorname{Fun}( \{ x\} , X ) \simeq X$ is a Kan fibration, so we can lift $\sigma $ to a $2$-simplex of $\operatorname{Fun}(X,X)$ depicted in the diagram

By construction, $\gamma $ is a pointed homotopy from $\operatorname{id}_{X}$ to the composition $g' \circ f$, so that the homotopy class $[g']$ is a left inverse to $[f]$ in the pointed homotopy category $\mathrm{h} \mathit{\operatorname{Kan}}_{\ast }$. $\square$