Kerodon

Proof. By virtue of Theorem 7.2.3.1, it will suffice to show that for every integer $n \geq 0$, the category $\operatorname{\mathcal{C}}= \operatorname{{\bf \Delta }}_{\operatorname{inj}} \times _{\operatorname{{\bf \Delta }}} \operatorname{{\bf \Delta }}_{ / [n] }$ has weakly contractible nerve. Let $C_0 \in \operatorname{\mathcal{C}}$ denote the object corresponding to the inclusion map $[0] \simeq \{ n\} \hookrightarrow [n]$. For every object $C \in \operatorname{\mathcal{C}}$, given by a nondecreasing function $\alpha : [m] \rightarrow [n]$, we let $F(C) \in \operatorname{\mathcal{C}}$ denote the object given by the nondecreasing function $\alpha ^{+}: [m+1] \rightarrow [n]$ given by the formula

Note that we have canonical maps $C \xrightarrow {\beta _{-}} F(C) \xleftarrow {\beta _+} C_0$, given by the inclusions

These morphisms depend functorially on $C$, and therefore furnish natural transformations of functors ${\operatorname{id}}_{\operatorname{\mathcal{C}}} \rightarrow F \leftarrow \underline{C}_0$, where $\underline{C}_0: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}$ denotes the constant functor taking the value $C_0$. It follows that the identity morphism of the simplicial set $\operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$ is homotopic to the constant morphism $\operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}) \twoheadrightarrow \{ C_0 \} \hookrightarrow \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$, so that the simplicial set $\operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$ is contractible (and, in particular, it is weakly contractible). $\square$