Kerodon

Proof. Let $S$ be a one-element set, and let $\operatorname{Fun}'_{\ast }(\operatorname{Lin}^{\operatorname{op}},\operatorname{Set})$ denote the full subcategory of $\operatorname{Fun}( \operatorname{Lin}^{\operatorname{op}}, \operatorname{Set})$ spanned by those functors $X: \operatorname{Lin}^{\operatorname{op}} \rightarrow \operatorname{Set}$ satisfying $X(\emptyset ) = S$. Since the inclusion functor $\operatorname{Fun}'_{\ast }( \operatorname{Lin}^{\operatorname{op}}, \operatorname{Set}) \hookrightarrow \operatorname{Fun}_{\ast }( \operatorname{Lin}^{\operatorname{op}}, \operatorname{Set})$ is an equivalence of categories, it will suffice to show that the restriction functor

is an equivalence of categories. Let $\operatorname{Lin}_{\neq \emptyset }$ denote the full subcategory of $\operatorname{Lin}$ spanned by the nonempty finite linearly ordered sets, so that the category $\operatorname{Lin}$ can be identified with the left cone $\operatorname{Lin}_{\neq \emptyset }^{\triangleleft }$ of Example 4.3.2.5. Using Proposition 4.3.2.13 (and the fact that the forgetful functor $\operatorname{Set}_{/\ast } \rightarrow \operatorname{Set}$ is an isomorphism), we deduce that the restriction functor $\operatorname{\mathcal{C}}\rightarrow \operatorname{Fun}( \operatorname{Lin}_{\neq \emptyset }^{\operatorname{op}}, \operatorname{Set})$ is an isomorphism of categories. We are therefore reduced to showing that the restriction functor $\operatorname{Fun}( \operatorname{Lin}_{\neq \emptyset }^{\operatorname{op}}, \operatorname{Set}) \rightarrow \operatorname{Fun}( \operatorname{{\bf \Delta }}^{\operatorname{op}}, \operatorname{Set}) = \operatorname{Set_{\Delta }}$ is an equivalence of categories. This is clear, since the inclusion $\operatorname{{\bf \Delta }}\hookrightarrow \operatorname{Lin}_{\neq \emptyset }$ is an equivalence (Remark 1.1.0.3). $\square$