Kerodon

Proof of Theorem 5.6.6.13. Let $\operatorname{\mathcal{C}}$ be a locally small $\infty $-category and let $X$ be an object of $\operatorname{\mathcal{C}}$. We wish to show that there exists a functor $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{S}}$ which is corepresentable by $X$, and that $\mathscr {F}$ is uniquely determined up to isomorphism (as an object of the $\infty $-category $\operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{S}})$). By virtue of Proposition 5.6.6.21 and Corollary 5.6.0.6, this is equivalent to the assertion that there exists a left fibration $U: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{C}}$ together with an initial object $\widetilde{X} \in \operatorname{\mathcal{D}}$ satisfying $U( \widetilde{X}) = X$, and that the left fibration $U$ is uniquely determined up to equivalence (in the sense of Definition 5.1.7.1). To prove existence, we can take $\operatorname{\mathcal{D}}= \operatorname{\mathcal{C}}_{X/}$ and $\widetilde{X}$ to be the identity morphism $\operatorname{id}_{X}$ (Proposition 4.6.7.22). The uniqueness assertion follows from Proposition 5.6.6.19. $\square$