In section 19.2.6 of Lurie's "Spectral Algebraic Geometry," he constructs the smooth projective space, which represents the derived version of the usual functor of points interpretation of projective space. The functorial construction is as follows for convenience:
Construction 19.2.6.1: Fix a nonnegative integer $n\geq 0.$ For every connective $\mathbb{E}_\infty$-ring $A,$ let $X(A)$ denote the subcategory of $(\mathsf{Mod}_A)_{/A^{n+1}}$ whose morphisms are equivalences and whose objects are maps $f : L\to A^{n+1}$ with the following property:
- The map $f$ admits a left homotopy inverse (that is, exhibits $L$ as a direct summand of $A^{n+1}$).
- The $A$-module $L$ is projective of rank $1.$
We will regard the construction $A\mapsto X(A)$ as a functor $X : \mathsf{CAlg}^{\textrm{cn}}\to\mathcal{S}.$
My question is about the last sentence: regarding this construction as a functor. Only assigning an $\infty$-groupoid is not enough to describe a functor, and as I understand, even if we describe how $X$ acts on morphisms of $\mathbb{E}_\infty$-rings this is not enough to construct $X$ as a functor.
This is probably standard, but how do we actually confirm that $X$ is a functor of $\infty$-categories? Specifically, I want to understand what needs to be specified in order to define $X$ as a functor, as well as how those details can be verified in this instance.