The Stacks project

Lemma 14.28.5. Let $f : X \to Y$ be a morphism of a category $\mathcal{C}$ with pushouts. Assume there is a morphism $s : Y \to X$ with $s \circ f = \text{id}_ X$. Consider the cosimplicial object $U$ constructed in Example 14.5.5 starting with $f$. The morphism $U \to U$ which in each degree is the self map of $Y \amalg _ X \ldots \amalg _ X Y$ given by $f \circ s$ on each factor is homotopic to the identity on $U$. In particular, $U$ is homotopy equivalent to the constant cosimplicial object $X$.