Kerodon

Proof of Theorem 9.1.2.5. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category and suppose that the homotopy category $\mathrm{h} \mathit{\operatorname{\mathcal{C}}}$ is homotopy filtered; we wish to show that $\operatorname{\mathcal{C}}$ is filtered (the reverse implication follows from Lemma 9.1.2.11). By virtue of Lemma 9.1.2.12, it will suffice to show that for every integer $n \geq 0$, every morphism of simplicial sets $f: \operatorname{\partial \Delta }^ n \rightarrow \operatorname{\mathcal{C}}$ can be extended to a morphism $\overline{f}: (\operatorname{\partial \Delta }^ n)^{\triangleright } \rightarrow \operatorname{\mathcal{C}}$. For $n = 0$, this follows from our assumption that $\mathrm{h} \mathit{\operatorname{\mathcal{C}}}$ is nonempty. We will therefore assume that $n > 0$. By virtue of Lemma 9.1.2.14, we may assume without loss of generality that the restriction $f_{-} = f|_{ \Delta ^{n-1} }$ is the constant map taking the value $X$ for some object $X \in \operatorname{\mathcal{C}}$. Set $Y = f(n)$ and let $\operatorname{Hom}_{\operatorname{\mathcal{C}}}^{\mathrm{R}}(X,Y) = \{ X\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{/Y}$ denote the right-pinched morphism space of Construction 4.6.5.1, so that we can identify $f|_{ \Lambda ^{n}_{n} }$ with a morphism of simplicial sets $g: \operatorname{\partial \Delta }^{n-1} \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{C}}}^{\mathrm{R}}(X,Y)$. Invoking assumption $(\ast _ n)$ of Definition 9.1.2.1, we deduce that there exists a morphism $v: Y \rightarrow Z$ in $\operatorname{\mathcal{C}}$ for which the composite map

is nullhomotopic. Since the projection map $\operatorname{\mathcal{C}}_{/f} \rightarrow \operatorname{\mathcal{C}}_{/Y}$ is a trivial Kan fibration (Corollary 4.3.6.14), we can lift $g$ to a morphism $\widetilde{g}: \operatorname{\partial \Delta }^{n-1} \rightarrow \{ X\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{/f}$. Combining Propositions 5.2.8.7 and 4.6.9.16, we deduce that the diagram of Kan complexes

commutes up to homotopy, where $\iota _{X,Y}^{\mathrm{R}}$ and $\iota _{X,Z}^{\mathrm{R}}$ are the right-pinch inclusion morphisms of Construction 4.6.5.7. Since $\iota ^{\mathrm{R}}_{X,Z}$ is a homotopy equivalence (Proposition 4.6.5.10), it follows that the composite map $\operatorname{\partial \Delta }^{n-1} \xrightarrow {\widetilde{g}} \{ X\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{/f} \rightarrow \{ X\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{/Z}$ is nullhomotopic, and can therefore be extended to an $(n-1)$-simplex $g': \Delta ^{n-1} \rightarrow \{ X\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{/Z}$ (Variant 3.2.4.12). Unwinding the definitions, we can identify $\widetilde{g}$ and $g'$ with morphisms $(\Lambda ^{n}_{n})^{\triangleright } \rightarrow \operatorname{\mathcal{C}}$ and $( \Delta ^{n-1 })^{\triangleright } \rightarrow \operatorname{\mathcal{C}}$, which can be amalgamated to a single morphism $\overline{f}: ( \operatorname{\partial \Delta }^{n} )^{\triangleright } \rightarrow \operatorname{\mathcal{C}}$ extending $f$. $\square$