ScalingStacks

Proof. One only has to observe that the map $\tilde{f}\colon U_{\mathcal{P}}F_{\mathcal{P}}\left(X\right)\to U_{\mathcal{P}}\left(A\right)$ is a map of cones on $\mathcal{P}_{\mathbf{SSeq}}\left(X\right)$. Let $u_{X}\colon X\to U_{\mathcal{P}}F_{\mathcal{P}}\left(X\right)$ be the unit map of the free-forgetful adjunction at $X$. The adjunct map $F_{\mathcal{P}}\left(X\right)\to A$ induces a map $\tilde{f}^{\triangleright}\colon\left(\mathcal{\mathcal{C}}_{\operatorname{\scriptsize{act}}}^{\otimes}\right)_{/U_{\mathcal{P}}F_{\mathcal{P}}\left(X\right)}\to\left(\mathcal{\mathcal{C}}_{\operatorname{\scriptsize{act}}}^{\otimes}\right)_{/U_{\mathcal{P}}\left(A\right)}$. Inspecting Construction A.3.1.3.1, it can be seen that the cone diagram $\mathcal{P}_{\mathbf{SSeq}}\left(f\right)$ is equivalent to the composition of the universal cone diagram $\mathcal{P}_{\mathbf{SSeq}}\left(u_{X}\right)$ and $\tilde{f}^{\triangleright}$. ∎