Kerodon

Definition 3.1.6.1. Let $f: X_{} \rightarrow Y_{}$ be a morphism of simplicial sets. We will say that a morphism $g: Y_{} \rightarrow X_{}$ is a simplicial homotopy inverse of $f$ if the compositions $g \circ f$ and $f \circ g$ are homotopic to the identity morphisms $\operatorname{id}_{X_{}}$ and $\operatorname{id}_{ Y_{} }$, respectively (in the sense of Definition 3.1.5.1). In the case where $X$ and $Y$ are Kan complexes, we will say that $g$ is a homotopy inverse of $f$ if it is a simplicial homotopy inverse to $f$. We say that $f: X_{} \rightarrow Y_{}$ is a homotopy equivalence if it admits a simplicial homotopy inverse $g$.